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)
proof
set A = cod (@ f);
reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by ;
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 ;
then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by ;
then A11: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;
{x1,x2} c= B by ;
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
.= cod (@ f) by ;
then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by ;
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 ;
A16: g1 . x = x1 by ;
reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by ;
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 ;
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 ) )
thus A24: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) ) by ; :: 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 ;
( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by ;
hence (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by ; :: thesis: verum
end;
then A27: ((@ (@ m1)) `2) * ((@ f) `2) = ((@ (@ m2)) `2) * ((@ f) `2) ;
cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by ;
then A28: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by ;
cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by ;
then A29: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by ;
A30: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by ;
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 ;
then A34: @ m1 in Hom (b,B) by ;
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
.= f2 (*) f by A30, A23, A32, A13, Th27
.= f2 * f by ;
then f1 = f2 by ;
hence contradiction by A5, A16, A15, XTUPLE_0:1; :: thesis: verum
end;
rng ((@ f) `2) c= cod (@ f) by Lm3;
hence rng ((@ f) `2) = cod (@ f) by ; :: according to ENS_1:def 8 :: thesis: verum