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 9 :: thesis: f is epi
let f1 be Morphism of (Ens V); :: according to CAT_1:def 11 :: 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 & dom f2 = cod f & cod f1 = cod f2 ) and
A3: f1 * f = f2 * f ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A4: ( dom (@ f1) = dom f1 & dom (@ f2) = dom f2 & cod (@ f1) = cod f1 & cod (@ f2) = cod f2 & cod (@ f) = cod f ) by Def10, Def11;
then ( (@ f1) * (@ f) = f1 * f & (@ f2) * (@ f) = f2 * f & (@ f1) * (@ f) = [[(dom (@ f)),(cod (@ f1))],(((@ f1) `2 ) * ((@ f) `2 ))] & (@ f2) * (@ f) = [[(dom (@ f)),(cod (@ f2))],(((@ f2) `2 ) * ((@ f) `2 ))] ) by A2, Def7, Th28;
then ( ((@ f1) `2 ) * ((@ f) `2 ) = ((@ f2) `2 ) * ((@ f) `2 ) & dom ((@ f1) `2 ) = dom f1 & dom ((@ f2) `2 ) = dom f2 ) by A3, A4, Lm3, ZFMISC_1:33;
then ( (@ f1) `2 = (@ f2) `2 & @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2 )] & @ f2 = [[(dom (@ f2)),(cod (@ f2))],((@ f2) `2 )] ) by A1, A2, A4, Th8, FUNCT_1:156;
hence f1 = f2 by A2, A4; :: thesis: verum