Proof 01. 1 ⊢ bij f X Y, hypo. 02. 1 ⊢ inj f X Y, lsubj_conj_eliml bij_equi 1. 03. 1 ⊢ map f X Y, inj_is_map 2. bij_is_map. ⊢ bij f X Y → map f X Y, subj_intro 3.