map_is_function

Theorem map_is_function

Theorem. map_is_function
map f X Y → function f

Proof
01. 1 ⊢ map f X Y, hypo.
02. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
03. 1 ⊢ function f ∧ dom f = X, conj_eliml 2.
04. 1 ⊢ function f, conj_eliml 3.
map_is_function. ⊢ map f X Y → function f, subj_intro 4.