Proof 01. 1 ⊢ sur f X Y, hypo. 02. 1 ⊢ map f X Y, lsubj_conj_eliml sur_equi 1. sur_is_map. ⊢ sur f X Y → map f X Y, subj_intro 2.