let V be non empty set ; :: thesis: for a, b being Object of (Ens V)

for f being Morphism of a,b st Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) holds

@ f is surjective

let a, b be Object of (Ens V); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) holds

@ f is surjective

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) implies @ f is surjective )

assume A1: Hom (a,b) <> {} ; :: thesis: ( not f is epi or for A being Element of V

for x1, x2 being set holds

( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )

assume A2: f is epi ; :: thesis: ( for A being Element of V

for x1, x2 being set holds

( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )

given B being Element of V, x1, x2 being set such that A3: x1 in B and

A4: x2 in B and

A5: x1 <> x2 ; :: thesis: @ f is surjective

A6: cod (@ f) c= rng ((@ f) `2)

hence rng ((@ f) `2) = cod (@ f) by A6, XBOOLE_0:def 10; :: according to ENS_1:def 8 :: thesis: verum

for f being Morphism of a,b st Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) holds

@ f is surjective

let a, b be Object of (Ens V); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) holds

@ f is surjective

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & f is epi & ex A being Element of V ex x1, x2 being set st

( x1 in A & x2 in A & x1 <> x2 ) implies @ f is surjective )

assume A1: Hom (a,b) <> {} ; :: thesis: ( not f is epi or for A being Element of V

for x1, x2 being set holds

( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )

assume A2: f is epi ; :: thesis: ( for A being Element of V

for x1, x2 being set holds

( not x1 in A or not x2 in A or not x1 <> x2 ) or @ f is surjective )

given B being Element of V, x1, x2 being set such that A3: x1 in B and

A4: x2 in B and

A5: x1 <> x2 ; :: thesis: @ f is surjective

A6: cod (@ f) c= rng ((@ f) `2)

proof

rng ((@ f) `2) c= cod (@ f)
by Lm3;
set A = cod (@ f);

reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A3, FUNCOP_1:45;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cod (@ f) or x in rng ((@ f) `2) )

assume that

A7: x in cod (@ f) and

A8: not x in rng ((@ f) `2) ; :: thesis: contradiction

set h = {x} --> x2;

set g2 = g1 +* ({x} --> x2);

A9: dom ({x} --> x2) = {x} by FUNCOP_1:13;

A10: rng ({x} --> x2) = {x2} by FUNCOP_1:8;

rng g1 = {x1} by A7, FUNCOP_1:8;

then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by A10, FUNCT_4:17;

then A11: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;

{x1,x2} c= B by A3, A4, ZFMISC_1:32;

then A12: rng (g1 +* ({x} --> x2)) c= B by A11;

dom g1 = cod (@ f) by FUNCOP_1:13;

then dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by A9, FUNCT_4:def 1

.= cod (@ f) by A7, ZFMISC_1:40 ;

then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A3, A12, FUNCT_2:def 1, RELSET_1:4;

A13: cod f = cod (@ f) by Def10;

A14: x in {x} by TARSKI:def 1;

then ({x} --> x2) . x = x2 by FUNCOP_1:7;

then A15: g2 . x = x2 by A14, A9, FUNCT_4:13;

A16: g1 . x = x1 by A7, FUNCOP_1:7;

reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A3, Th5;

set f1 = @ m1;

set f2 = @ m2;

set h1 = ((@ (@ m1)) `2) * ((@ f) `2);

set h2 = ((@ (@ m2)) `2) * ((@ f) `2);

set f1f = (@ (@ m1)) * (@ f);

set f2f = (@ (@ m2)) * (@ f);

A17: dom m1 = cod (@ f) ;

then A18: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2) * ((@ f) `2) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) ) by Th12;

A19: dom m2 = cod (@ f) ;

then A20: ( ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2) * ((@ f) `2) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) ) by Th12;

cod (@ (@ m2)) = B ;

then A21: cod (@ m2) = B by Def10;

dom (@ (@ m2)) = cod (@ f) ;

then A22: dom (@ m2) = cod (@ f) by Def9;

then A23: (@ m2) (*) f = (@ (@ m2)) * (@ f) by A13, Th27;

cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by A17, Th12;

then A28: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by A18, Th8;

cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by A19, Th12;

then A29: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by A20, Th8;

A30: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by A28, A29, A27;

cod (@ (@ m1)) = B ;

then A31: cod (@ m1) = B by Def10;

dom (@ (@ m1)) = cod (@ f) ;

then A32: dom (@ m1) = cod (@ f) by Def9;

reconsider B = B as Object of (Ens V) ;

A33: cod f = b by A1, CAT_1:5;

then A34: @ m1 in Hom (b,B) by A13, A31, A32;

then reconsider f1 = @ m1 as Morphism of b,B by CAT_1:def 5;

@ m2 in Hom (b,B) by A13, A21, A22, A33;

then reconsider f2 = @ m2 as Morphism of b,B by CAT_1:def 5;

f1 * f = f1 (*) f by A1, A34, CAT_1:def 13

.= f2 (*) f by A30, A23, A32, A13, Th27

.= f2 * f by A1, A34, CAT_1:def 13 ;

then f1 = f2 by A2, A34;

hence contradiction by A5, A16, A15, XTUPLE_0:1; :: thesis: verum

end;reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A3, FUNCOP_1:45;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cod (@ f) or x in rng ((@ f) `2) )

assume that

A7: x in cod (@ f) and

A8: not x in rng ((@ f) `2) ; :: thesis: contradiction

set h = {x} --> x2;

set g2 = g1 +* ({x} --> x2);

A9: dom ({x} --> x2) = {x} by FUNCOP_1:13;

A10: rng ({x} --> x2) = {x2} by FUNCOP_1:8;

rng g1 = {x1} by A7, FUNCOP_1:8;

then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by A10, FUNCT_4:17;

then A11: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;

{x1,x2} c= B by A3, A4, ZFMISC_1:32;

then A12: rng (g1 +* ({x} --> x2)) c= B by A11;

dom g1 = cod (@ f) by FUNCOP_1:13;

then dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by A9, FUNCT_4:def 1

.= cod (@ f) by A7, ZFMISC_1:40 ;

then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A3, A12, FUNCT_2:def 1, RELSET_1:4;

A13: cod f = cod (@ f) by Def10;

A14: x in {x} by TARSKI:def 1;

then ({x} --> x2) . x = x2 by FUNCOP_1:7;

then A15: g2 . x = x2 by A14, A9, FUNCT_4:13;

A16: g1 . x = x1 by A7, FUNCOP_1:7;

reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A3, Th5;

set f1 = @ m1;

set f2 = @ m2;

set h1 = ((@ (@ m1)) `2) * ((@ f) `2);

set h2 = ((@ (@ m2)) `2) * ((@ f) `2);

set f1f = (@ (@ m1)) * (@ f);

set f2f = (@ (@ m2)) * (@ f);

A17: dom m1 = cod (@ f) ;

then A18: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2) * ((@ f) `2) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) ) by Th12;

A19: dom m2 = cod (@ f) ;

then A20: ( ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2) * ((@ f) `2) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) ) by Th12;

cod (@ (@ m2)) = B ;

then A21: cod (@ m2) = B by Def10;

dom (@ (@ m2)) = cod (@ f) ;

then A22: dom (@ m2) = cod (@ f) by Def9;

then A23: (@ m2) (*) f = (@ (@ m2)) * (@ f) by A13, Th27;

now :: thesis: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) & ( for z being object st z in dom (@ f) holds

(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z ) )

then A27:
((@ (@ m1)) `2) * ((@ f) `2) = ((@ (@ m2)) `2) * ((@ f) `2)
;(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z ) )

thus A24:
( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) )
by A18, A20, Lm3; :: thesis: for z being object st z in dom (@ f) holds

(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z

let z be object ; :: thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z )

set y = ((@ f) `2) . z;

assume A25: z in dom (@ f) ; :: thesis: (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z

then z in dom ((@ f) `2) by Lm3;

then ((@ f) `2) . z in rng ((@ f) `2) by FUNCT_1:def 3;

then A26: not ((@ f) `2) . z in {x} by A8, TARSKI:def 1;

( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by A24, A25, FUNCT_1:12;

hence (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by A9, A26, FUNCT_4:11; :: thesis: verum

end;(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z

let z be object ; :: thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z )

set y = ((@ f) `2) . z;

assume A25: z in dom (@ f) ; :: thesis: (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z

then z in dom ((@ f) `2) by Lm3;

then ((@ f) `2) . z in rng ((@ f) `2) by FUNCT_1:def 3;

then A26: not ((@ f) `2) . z in {x} by A8, TARSKI:def 1;

( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by A24, A25, FUNCT_1:12;

hence (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by A9, A26, FUNCT_4:11; :: thesis: verum

cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by A17, Th12;

then A28: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by A18, Th8;

cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by A19, Th12;

then A29: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by A20, Th8;

A30: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by A28, A29, A27;

cod (@ (@ m1)) = B ;

then A31: cod (@ m1) = B by Def10;

dom (@ (@ m1)) = cod (@ f) ;

then A32: dom (@ m1) = cod (@ f) by Def9;

reconsider B = B as Object of (Ens V) ;

A33: cod f = b by A1, CAT_1:5;

then A34: @ m1 in Hom (b,B) by A13, A31, A32;

then reconsider f1 = @ m1 as Morphism of b,B by CAT_1:def 5;

@ m2 in Hom (b,B) by A13, A21, A22, A33;

then reconsider f2 = @ m2 as Morphism of b,B by CAT_1:def 5;

f1 * f = f1 (*) f by A1, A34, CAT_1:def 13

.= f2 (*) f by A30, A23, A32, A13, Th27

.= f2 * f by A1, A34, CAT_1:def 13 ;

then f1 = f2 by A2, A34;

hence contradiction by A5, A16, A15, XTUPLE_0:1; :: thesis: verum

hence rng ((@ f) `2) = cod (@ f) by A6, XBOOLE_0:def 10; :: according to ENS_1:def 8 :: thesis: verum