Proof 01. 1 ⊢ map f X Y, hypo. 02. 1 ⊢ function f, map_is_function 1. 03. 1 ⊢ relation f, fn_is_rel 2. map_is_relation. ⊢ map f X Y → relation f, subj_intro 3.