Proof 01. 1 ⊢ fn_on f A, hypo. 02. 1 ⊢ relation f, lsubj_conj_eliml fn_on_equi 1. relation_from_fn_on. ⊢ fn_on f A → relation f, subj_intro 2.