let V be non empty set ; :: thesis: for f being Morphism of (Ens V) st 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 (Ens V); :: thesis: ( 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: 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 A2: x1 in B and
A3: x2 in B and
A4: x1 <> x2 ; :: thesis: @ f is surjective
A5: cod (@ f) c= rng ((@ f) `2)

proof

set A = cod (@ f);
reconsider g1 = (cod (@ f)) --> x1 as Function of (cod (@ f)),B by A2, FUNCOP_1:45;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in cod (@ f) or x in rng ((@ f) `2) )
assume that
A6: x in cod (@ f) and
A7: not x in rng ((@ f) `2) ; :: thesis: contradiction
set h = {x} --> x2;
set g2 = g1 +* ({x} --> x2);
A8: dom ({x} --> x2) = {x} by FUNCOP_1:13;
A9: rng ({x} --> x2) = {x2} by FUNCOP_1:8;
rng g1 = {x1} by A6, FUNCOP_1:8;
then rng (g1 +* ({x} --> x2)) c= {x1} \/ {x2} by A9, FUNCT_4:17;
then A10: rng (g1 +* ({x} --> x2)) c= {x1,x2} by ENUMSET1:1;
{x1,x2} c= B by A2, A3, ZFMISC_1:32;
then A11: rng (g1 +* ({x} --> x2)) c= B by A10, XBOOLE_1:1;
dom g1 = cod (@ f) by FUNCOP_1:13;
then dom (g1 +* ({x} --> x2)) = (cod (@ f)) \/ {x} by A8, FUNCT_4:def 1
.= cod (@ f) by A6, ZFMISC_1:40 ;
then reconsider g2 = g1 +* ({x} --> x2) as Function of (cod (@ f)),B by A2, A11, FUNCT_2:def 1, RELSET_1:4;
A12: cod f = cod (@ f) by Def11;
A13: x in {x} by TARSKI:def 1;
then ({x} --> x2) . x = x2 by FUNCOP_1:7;
then A14: g2 . x = x2 by A13, A8, FUNCT_4:13;
A15: g1 . x = x1 by A6, FUNCOP_1:7;
reconsider m1 = [[(cod (@ f)),B],g1], m2 = [[(cod (@ f)),B],g2] as Element of Maps V by A2, 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);
A16: m1 = [[(dom m1),(cod m1)],(m1 `2)] by Th8;
then A17: g1 = m1 `2 by ZFMISC_1:27;
A18: dom m1 = cod (@ f) by A16, Lm1;
then A19: ( ((@ (@ m1)) * (@ f)) `2 = ((@ (@ m1)) `2) * ((@ f) `2) & dom ((@ (@ m1)) * (@ f)) = dom (@ f) ) by Th12;
A20: m2 = [[(dom m2),(cod m2)],(m2 `2)] by Th8;
then A21: dom m2 = cod (@ f) by Lm1;
then A22: ( ((@ (@ m2)) * (@ f)) `2 = ((@ (@ m2)) `2) * ((@ f) `2) & dom ((@ (@ m2)) * (@ f)) = dom (@ f) ) by Th12;
cod (@ (@ m2)) = B by A20, Lm1;
then A23: cod (@ m2) = B by Def11;
dom (@ (@ m2)) = cod (@ f) by A20, Lm1;
then A24: dom (@ m2) = cod (@ f) by Def10;
then A25: (@ m2) * f = (@ (@ m2)) * (@ f) by A12, Th28;
A26: g2 = m2 `2 by A20, ZFMISC_1:27;

now

thus A27: ( dom (((@ (@ m1)) `2) * ((@ f) `2)) = dom (@ f) & dom (((@ (@ m2)) `2) * ((@ f) `2)) = dom (@ f) ) by A19, A22, Lm3; :: thesis: for z being set st z in dom (@ f) holds
(((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z
let z be set ; :: thesis: ( z in dom (@ f) implies (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z )
set y = ((@ f) `2) . z;
assume A28: 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 A29: not ((@ f) `2) . z in {x} by A7, TARSKI:def 1;
( (((@ (@ m1)) `2) * ((@ f) `2)) . z = g1 . (((@ f) `2) . z) & (((@ (@ m2)) `2) * ((@ f) `2)) . z = g2 . (((@ f) `2) . z) ) by A17, A26, A27, A28, FUNCT_1:12;
hence (((@ (@ m1)) `2) * ((@ f) `2)) . z = (((@ (@ m2)) `2) * ((@ f) `2)) . z by A8, A29, FUNCT_4:11; :: thesis: verum

end;

then A30: ((@ (@ m1)) `2) * ((@ f) `2) = ((@ (@ m2)) `2) * ((@ f) `2) by FUNCT_1:2;
cod ((@ (@ m1)) * (@ f)) = cod (@ (@ m1)) by A18, Th12;
then A31: (@ (@ m1)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m1)))],(((@ (@ m1)) `2) * ((@ f) `2))] by A19, Th8;
cod ((@ (@ m2)) * (@ f)) = cod (@ (@ m2)) by A21, Th12;
then A32: (@ (@ m2)) * (@ f) = [[(dom (@ f)),(cod (@ (@ m2)))],(((@ (@ m2)) `2) * ((@ f) `2))] by A22, Th8;
cod m1 = B by A16, Lm1;
then A33: (@ (@ m1)) * (@ f) = (@ (@ m2)) * (@ f) by A20, A31, A32, A30, Lm1;
cod (@ (@ m1)) = B by A16, Lm1;
then A34: cod (@ m1) = B by Def11;
dom (@ (@ m1)) = cod (@ f) by A16, Lm1;
then A35: dom (@ m1) = cod (@ f) by Def10;
then (@ m1) * f = (@ (@ m1)) * (@ f) by A12, Th28;
then @ m1 = @ m2 by A1, A35, A24, A34, A23, A12, A33, A25, CAT_1:def 8;
hence contradiction by A4, A15, A14, ZFMISC_1:27; :: thesis: verum

end;

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