let X be non empty with_non-empty_elements set ; :: thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let o1, o2 be object of (EnsCat X); :: thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto ) )
assume A1: <^o1,o2^> <> {} ; :: thesis: for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let A be Morphism of o1,o2; :: thesis: for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let F be Function of o1,o2; :: thesis: ( F = A implies ( A is epi iff F is onto ) )
assume A2: F = A ; :: thesis: ( A is epi iff F is onto )

per cases ( for x being set st x in X holds
x is trivial or ex x being set st
( x in X & not x is trivial ) ) ;

suppose A3: for x being set st x in X holds
x is trivial ; :: thesis: ( A is epi iff F is onto )

thus ( A is epi implies F is onto ) :: thesis: ( F is onto implies A is epi )

proof

assume A is epi ; :: thesis: F is onto

now

per cases ( o2 = {} or o2 <> {} ) ;

suppose A4: o2 = {} ; :: thesis: F is onto

now

per cases ( o1 = {} or o1 <> {} ) ;

suppose o1 = {} ; :: thesis: F = {}

hence F = {} ; :: thesis: verum

end;

suppose o1 <> {} ; :: thesis: F = {}

thus F = {} by A4; :: thesis: verum

end;

end;

end;

hence F is onto by A4, FUNCT_2:def 3, RELAT_1:60; :: thesis: verum

end;

suppose A5: o2 <> {} ; :: thesis: F is onto

o2 is Element of X by ALTCAT_1:def 16;
then o2 is trivial by A3;
then consider y being set such that
A6: o2 = {y} by A5, REALSET1:def 4;
A7: rng F c= {y} by A6, RELAT_1:def 19;
A8: o1 is Element of X by ALTCAT_1:def 16;
then o1 is trivial by A3;
then consider z being set such that
A9: o1 = {z} by A8, REALSET1:def 4;
dom F = {z} by A5, A9, FUNCT_2:def 1;
then rng F <> {} by RELAT_1:65;
then rng F = {y} by A7, ZFMISC_1:39;
hence F is onto by A6, FUNCT_2:def 3; :: thesis: verum

end;

end;

end;

hence F is onto ; :: thesis: verum

end;

thus ( F is onto implies A is epi ) :: thesis: verum

proof

assume A10: F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A11: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
assume A12: B * A = C * A ; :: thesis: B = C
A13: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A14: ( B1 = B & dom B1 = o2 & rng B1 c= o ) by A11, FUNCT_2:def 2;
consider C1 being Function such that
A15: ( C1 = C & dom C1 = o2 & rng C1 c= o ) by A11, A13, FUNCT_2:def 2;
A16: <^o1,o^> <> {} by A1, A11, ALTCAT_1:def 4;
then A17: B1 * F = C * A by A1, A2, A11, A12, A14, ALTCAT_1:18
.= C1 * F by A1, A2, A11, A15, A16, ALTCAT_1:18 ;

now

assume B1 <> C1 ; :: thesis: contradiction
then consider z being set such that
A18: ( z in o2 & B1 . z <> C1 . z ) by A14, A15, FUNCT_1:9;
z in rng F by A10, A18, FUNCT_2:def 3;
then consider x being set such that
A19: ( x in dom F & F . x = z ) by FUNCT_1:def 5;
B1 . (F . x) = (B1 * F) . x by A19, FUNCT_1:23;
hence contradiction by A17, A18, A19, FUNCT_1:23; :: thesis: verum

end;

hence B = C by A14, A15; :: thesis: verum

end;

end;

suppose A20: ex x being set st
( x in X & not x is trivial ) ; :: thesis: ( A is epi iff F is onto )

now

per cases ( o2 <> {} or o2 = {} ) ;

suppose o2 <> {} ; :: thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )

then A21: dom F = o1 by FUNCT_2:def 1;
consider o being set such that
A22: o in X and
A23: not o is trivial by A20;
reconsider o = o as object of (EnsCat X) by A22, ALTCAT_1:def 16;
thus ( A is epi implies F is onto ) :: thesis: ( F is onto implies A is epi )

proof

assume that
A24: A is epi and
A25: not F is onto ; :: thesis: contradiction
A26: rng F c= o2 by RELAT_1:def 19;
rng F <> o2 by A25, FUNCT_2:def 3;
then not o2 c= rng F by A26, XBOOLE_0:def 10;
then consider y being set such that
A27: ( y in o2 & not y in rng F ) by TARSKI:def 3;
A28: o <> {} by A22;
consider k being Element of o;
reconsider ok = o \ {k} as non empty set by A23, REALSET1:4;
consider l being Element of ok;
A29: ( l in o & not l in {k} ) by XBOOLE_0:def 5;
reconsider l = l as Element of o by XBOOLE_0:def 5;
A30: k <> l by A29, TARSKI:def 1;
A31: ( k in o & l in o ) by A28;
deffunc H₁( set ) -> Element of o = IFEQ $1,y,l,k;
consider B being Function such that
A32: dom B = o2 and
A33: for x being set st x in o2 holds
B . x = H₁(x) from FUNCT_1:sch 3();
set C = o2 --> k;
A34: dom (o2 --> k) = o2 by FUNCOP_1:19;
B . y = IFEQ y,y,l,k by A27, A33
.= l by FUNCOP_1:def 8 ;
then A35: not B = o2 --> k by A27, A30, FUNCOP_1:13;
A36: rng B c= o

proof

let y1 be set ; :: according to TARSKI:def 3 :: thesis: ( not y1 in rng B or y1 in o )
assume y1 in rng B ; :: thesis: y1 in o
then consider x being set such that
A37: ( x in dom B & B . x = y1 ) by FUNCT_1:def 5;

per cases ( x = y or x <> y ) ;

suppose A38: x = y ; :: thesis: y1 in o

y1 = IFEQ x,y,l,k by A32, A33, A37
.= l by A38, FUNCOP_1:def 8 ;
hence y1 in o by A28; :: thesis: verum

end;

suppose A39: x <> y ; :: thesis: y1 in o

y1 = IFEQ x,y,l,k by A32, A33, A37
.= k by A39, FUNCOP_1:def 8 ;
hence y1 in o by A28; :: thesis: verum

end;

end;

end;

then A40: B in Funcs o2,o by A32, FUNCT_2:def 2;
then A41: B in <^o2,o^> by ALTCAT_1:def 16;
reconsider B1 = B as Morphism of o2,o by A40, ALTCAT_1:def 16;
rng (o2 --> k) c= o

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o2 --> k) or y in o )
assume y in rng (o2 --> k) ; :: thesis: y in o
then consider x being set such that
A42: ( x in dom (o2 --> k) & (o2 --> k) . x = y ) by FUNCT_1:def 5;
thus y in o by A31, A34, A42, FUNCOP_1:13; :: thesis: verum

end;

then o2 --> k in Funcs o2,o by A34, FUNCT_2:def 2;
then reconsider C1 = o2 --> k as Morphism of o2,o by ALTCAT_1:def 16;
A43: dom (B * F) = o1 by A21, A26, A32, RELAT_1:46;
for z being set st z in rng (B * F) holds
z in rng B by FUNCT_1:25;
then rng (B * F) c= rng B by TARSKI:def 3;
then rng (B * F) c= o by A36, XBOOLE_1:1;
then B * F in Funcs o1,o by A43, FUNCT_2:def 2;
then A44: B * F in <^o1,o^> by ALTCAT_1:def 16;
A45: dom ((o2 --> k) * F) = o1 by A21, A26, A34, RELAT_1:46;

now

let z be set ; :: thesis: ( z in o1 implies (B * F) . z = ((o2 --> k) * F) . z )
assume A46: z in o1 ; :: thesis: (B * F) . z = ((o2 --> k) * F) . z
then A47: F . z in rng F by A21, FUNCT_1:def 5;
then A48: B . (F . z) = IFEQ (F . z),y,l,k by A26, A33
.= k by A27, A47, FUNCOP_1:def 8 ;
thus (B * F) . z = B . (F . z) by A43, A46, FUNCT_1:22
.= (o2 --> k) . (F . z) by A26, A47, A48, FUNCOP_1:13
.= ((o2 --> k) * F) . z by A45, A46, FUNCT_1:22 ; :: thesis: verum

end;

then B * F = (o2 --> k) * F by A43, A45, FUNCT_1:9;
then B1 * A = (o2 --> k) * F by A1, A2, A41, A44, ALTCAT_1:18
.= C1 * A by A1, A2, A41, A44, ALTCAT_1:18 ;
hence contradiction by A24, A35, A41, Def8; :: thesis: verum

end;

thus ( F is onto implies A is epi ) :: thesis: verum

proof

assume A49: F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A50: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
assume A51: B * A = C * A ; :: thesis: B = C
A52: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A53: ( B1 = B & dom B1 = o2 & rng B1 c= o ) by A50, FUNCT_2:def 2;
consider C1 being Function such that
A54: ( C1 = C & dom C1 = o2 & rng C1 c= o ) by A50, A52, FUNCT_2:def 2;
A55: <^o1,o^> <> {} by A1, A50, ALTCAT_1:def 4;
then A56: B1 * F = C * A by A1, A2, A50, A51, A53, ALTCAT_1:18
.= C1 * F by A1, A2, A50, A54, A55, ALTCAT_1:18 ;

now

assume B1 <> C1 ; :: thesis: contradiction
then consider z being set such that
A57: ( z in o2 & B1 . z <> C1 . z ) by A53, A54, FUNCT_1:9;
z in rng F by A49, A57, FUNCT_2:def 3;
then consider x being set such that
A58: ( x in dom F & F . x = z ) by FUNCT_1:def 5;
B1 . (F . x) = (B1 * F) . x by A58, FUNCT_1:23;
hence contradiction by A56, A57, A58, FUNCT_1:23; :: thesis: verum

end;

hence B = C by A53, A54; :: thesis: verum

end;

end;

suppose A59: o2 = {} ; :: thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )

now

per cases ( o1 = {} or o1 <> {} ) ;

suppose o1 = {} ; :: thesis: F = {}

hence F = {} ; :: thesis: verum

end;

suppose o1 <> {} ; :: thesis: F = {}

thus F = {} by A59; :: thesis: verum

end;

end;

end;

hence ( A is epi implies F is onto ) by A59, FUNCT_2:def 3, RELAT_1:60; :: thesis: ( F is onto implies A is epi )
thus ( F is onto implies A is epi ) :: thesis: verum

proof

assume F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A60: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
assume B * A = C * A ; :: thesis: B = C
A61: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A62: ( B1 = B & dom B1 = o2 & rng B1 c= o ) by A60, FUNCT_2:def 2;
consider C1 being Function such that
A63: ( C1 = C & dom C1 = o2 & rng C1 c= o ) by A60, A61, FUNCT_2:def 2;
( B1 = {} & C1 = {} ) by A59, A62, A63, RELAT_1:64;
hence B = C by A62, A63; :: thesis: verum

end;

end;

end;

end;

hence ( A is epi iff F is onto ) ; :: thesis: verum

end;

end;