let V be non empty set ; :: thesis: for f being Morphism of (Ens V) st @ f is surjective holds
f is epi
let f be Morphism of (Ens V); :: thesis: ( @ f is surjective implies f is epi )
set m = @ f;
assume A1: rng ((@ f) `2) = cod (@ f) ; :: according to ENS_1:def 8 :: thesis: f is epi
let f1 be Morphism of (Ens V); :: according to CAT_1:def 8 :: thesis: for b<sub>1</sub> being Element of the carrier' of (Ens V) holds
( not dom f1 = cod f or not dom b<sub>1</sub> = cod f or not cod f1 = cod b<sub>1</sub> or not f1 * f = b<sub>1</sub> * f or f1 = b<sub>1</sub> )
let f2 be Morphism of (Ens V); :: thesis: ( not dom f1 = cod f or not dom f2 = cod f or not cod f1 = cod f2 or not f1 * f = f2 * f or f1 = f2 )
assume that
A2: dom f1 = cod f and
A3: dom f2 = cod f and
A4: cod f1 = cod f2 and
A5: f1 * f = f2 * f ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A6: ( (@ f1) * (@ f) = f1 * f & (@ f2) * (@ f) = f2 * f ) by A2, A3, Th28;
A7: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A8: ( cod (@ f1) = cod f1 & cod (@ f2) = cod f2 ) by Def11;
A9: dom (@ f2) = dom f2 by Def10;
then A10: dom ((@ f2) `2) = dom f2 by Lm3;
A11: cod (@ f) = cod f by Def11;
then A12: (@ f2) * (@ f) = [[(dom (@ f)),(cod (@ f2))],(((@ f2) `2) * ((@ f) `2))] by A3, A9, Def7;
A13: dom (@ f1) = dom f1 by Def10;
then (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2) * ((@ f) `2))] by A2, A11, Def7;
then A14: ((@ f1) `2) * ((@ f) `2) = ((@ f2) `2) * ((@ f) `2) by A5, A6, A12, ZFMISC_1:27;
dom ((@ f1) `2) = dom f1 by A13, Lm3;
then (@ f1) `2 = (@ f2) `2 by A1, A2, A3, A11, A14, A10, FUNCT_1:86;
hence f1 = f2 by A2, A3, A4, A13, A9, A8, A7, Th8; :: thesis: verum