Theorem fn_on_from_map

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ A ⊆ X, hypo.
03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
04. 1 ⊢ function f, conj_elimll 3.
05. 1 ⊢ dom f = X, conj_elimlr 3.
06. 1, 2 ⊢ A ⊆ dom f, eq_subst_rev 5 2.
07. 1, 2 ⊢ fn_on f A, fn_on_from_function 4 6.
fn_on_from_map. ⊢ map f X Y → A ⊆ X → fn_on f A, subj_intro_ii 7.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.