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 :: thesis: F is onto

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

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

then F = {} ;
hence F is onto by A4, FUNCT_2:def 3, RELAT_1:38; :: thesis: verum

end;

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

A6: o1 is Element of X by ALTCAT_1:def 14;
then o1 is trivial by A3;
then consider z being object such that
A7: o1 = {z} by A6, ZFMISC_1:131;
dom F = {z} by A5, A7, FUNCT_2:def 1;
then A8: rng F <> {} by RELAT_1:42;
o2 is Element of X by ALTCAT_1:def 14;
then o2 is trivial by A3;
then consider y being object such that
A9: o2 = {y} by A5, ZFMISC_1:131;
rng F c= {y} by A9, RELAT_1:def 19;
then rng F = {y} by A8, ZFMISC_1:33;
hence F is onto by A9, 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
then A12: <^o1,o^> <> {} by A1, ALTCAT_1:def 2;
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
A13: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def 14;
then consider B1 being Function such that
A14: B1 = B and
A15: dom B1 = o2 and
rng B1 c= o by A11, FUNCT_2:def 2;
consider C1 being Function such that
A16: C1 = C and
A17: dom C1 = o2 and
rng C1 c= o by A11, A13, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
then A18: B1 * F = C * A by A1, A2, A11, A14, A12, ALTCAT_1:16
.= C1 * F by A1, A2, A11, A16, A12, ALTCAT_1:16 ;

now :: thesis: not B1 <> C1

assume B1 <> C1 ; :: thesis: contradiction
then consider z being object such that
A19: z in o2 and
A20: B1 . z <> C1 . z by A15, A17, FUNCT_1:2;
z in rng F by A10, A19, FUNCT_2:def 3;
then consider x being object such that
A21: x in dom F and
A22: F . x = z by FUNCT_1:def 3;
B1 . (F . x) = (B1 * F) . x by A21, FUNCT_1:13;
hence contradiction by A18, A20, A21, A22, FUNCT_1:13; :: thesis: verum

end;

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

end;

end;

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

now :: thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )

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

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

consider o being set such that
A25: o in X and
A26: not o is trivial by A23;
reconsider o = o as Object of (EnsCat X) by A25, ALTCAT_1:def 14;
A27: dom F = o1 by A24, FUNCT_2:def 1;
thus ( A is epi implies F is onto ) :: thesis: ( F is onto implies A is epi )

proof

set k = the Element of o;
A28: rng F c= o2 by RELAT_1:def 19;
reconsider ok = o \ { the Element of o} as non empty set by A26, ZFMISC_1:139;
assume that
A29: A is epi and
A30: not F is onto ; :: thesis: contradiction
rng F <> o2 by A30, FUNCT_2:def 3;
then not o2 c= rng F by A28, XBOOLE_0:def 10;
then consider y being object such that
A31: y in o2 and
A32: not y in rng F ;
set C = o2 --> the Element of o;
A33: dom (o2 --> the Element of o) = o2 by FUNCOP_1:13;
A34: o <> {} by A25;
then A35: the Element of o in o ;
rng (o2 --> the Element of o) c= o

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o2 --> the Element of o) or y in o )
assume y in rng (o2 --> the Element of o) ; :: thesis: y in o
then ex x being object st
( x in dom (o2 --> the Element of o) & (o2 --> the Element of o) . x = y ) by FUNCT_1:def 3;
hence y in o by A35, A33, FUNCOP_1:7; :: thesis: verum

end;

then o2 --> the Element of o in Funcs (o2,o) by A33, FUNCT_2:def 2;
then reconsider C1 = o2 --> the Element of o as Morphism of o2,o by ALTCAT_1:def 14;
set l = the Element of ok;
A36: not the Element of ok in { the Element of o} by XBOOLE_0:def 5;
reconsider l = the Element of ok as Element of o by XBOOLE_0:def 5;
A37: the Element of o <> l by A36, TARSKI:def 1;
deffunc H₁( object ) -> Element of o = IFEQ ($1,y,l, the Element of o);
consider B being Function such that
A38: dom B = o2 and
A39: for x being object st x in o2 holds
B . x = H₁(x) from FUNCT_1:sch 3();
A40: dom (B * F) = o1 by A27, A28, A38, RELAT_1:27;
A41: rng B c= o

proof

let y1 be object ; :: 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 object such that
A42: ( x in dom B & B . x = y1 ) by FUNCT_1:def 3;

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

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

y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42
.= l by A43, FUNCOP_1:def 8 ;
hence y1 in o by A34; :: thesis: verum

end;

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

y1 = IFEQ (x,y,l, the Element of o) by A38, A39, A42
.= the Element of o by A44, FUNCOP_1:def 8 ;
hence y1 in o by A34; :: thesis: verum

end;

end;

end;

then A45: B in Funcs (o2,o) by A38, FUNCT_2:def 2;
then A46: B in <^o2,o^> by ALTCAT_1:def 14;
reconsider B1 = B as Morphism of o2,o by A45, ALTCAT_1:def 14;
for z being object st z in rng (B * F) holds
z in rng B by FUNCT_1:14;
then rng (B * F) c= rng B ;
then rng (B * F) c= o by A41;
then B * F in Funcs (o1,o) by A40, FUNCT_2:def 2;
then A47: B * F in <^o1,o^> by ALTCAT_1:def 14;
B . y = IFEQ (y,y,l, the Element of o) by A31, A39
.= l by FUNCOP_1:def 8 ;
then A48: not B = o2 --> the Element of o by A31, A37, FUNCOP_1:7;
A49: dom ((o2 --> the Element of o) * F) = o1 by A27, A28, A33, RELAT_1:27;

now :: thesis: for z being object st z in o1 holds
(B * F) . z = ((o2 --> the Element of o) * F) . z

let z be object ; :: thesis: ( z in o1 implies (B * F) . z = ((o2 --> the Element of o) * F) . z )
assume A50: z in o1 ; :: thesis: (B * F) . z = ((o2 --> the Element of o) * F) . z
then A51: F . z in rng F by A27, FUNCT_1:def 3;
then A52: B . (F . z) = IFEQ ((F . z),y,l, the Element of o) by A28, A39
.= the Element of o by A32, A51, FUNCOP_1:def 8 ;
thus (B * F) . z = B . (F . z) by A40, A50, FUNCT_1:12
.= (o2 --> the Element of o) . (F . z) by A28, A51, A52, FUNCOP_1:7
.= ((o2 --> the Element of o) * F) . z by A49, A50, FUNCT_1:12 ; :: thesis: verum

end;

then B * F = (o2 --> the Element of o) * F by A40, A49, FUNCT_1:2;
then B1 * A = (o2 --> the Element of o) * F by A1, A2, A46, A47, ALTCAT_1:16
.= C1 * A by A1, A2, A46, A47, ALTCAT_1:16 ;
hence contradiction by A29, A48, A46; :: thesis: verum

end;

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

proof

assume A53: 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 A54: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
then A55: <^o1,o^> <> {} by A1, ALTCAT_1:def 2;
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
A56: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def 14;
then consider B1 being Function such that
A57: B1 = B and
A58: dom B1 = o2 and
rng B1 c= o by A54, FUNCT_2:def 2;
consider C1 being Function such that
A59: C1 = C and
A60: dom C1 = o2 and
rng C1 c= o by A54, A56, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
then A61: B1 * F = C * A by A1, A2, A54, A57, A55, ALTCAT_1:16
.= C1 * F by A1, A2, A54, A59, A55, ALTCAT_1:16 ;

now :: thesis: not B1 <> C1

assume B1 <> C1 ; :: thesis: contradiction
then consider z being object such that
A62: z in o2 and
A63: B1 . z <> C1 . z by A58, A60, FUNCT_1:2;
z in rng F by A53, A62, FUNCT_2:def 3;
then consider x being object such that
A64: x in dom F and
A65: F . x = z by FUNCT_1:def 3;
B1 . (F . x) = (B1 * F) . x by A64, FUNCT_1:13;
hence contradiction by A61, A63, A64, A65, FUNCT_1:13; :: thesis: verum

end;

hence B = C by A57, A59; :: thesis: verum

end;

end;

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

then F = {} ;
hence ( A is epi implies F is onto ) by A66, FUNCT_2:def 3, RELAT_1:38; :: 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 A67: <^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 )
A68: <^o2,o^> = Funcs (o2,o) by ALTCAT_1:def 14;
then consider B1 being Function such that
A69: B1 = B and
A70: dom B1 = o2 and
rng B1 c= o by A67, FUNCT_2:def 2;
A71: ex C1 being Function st
( C1 = C & dom C1 = o2 & rng C1 c= o ) by A67, A68, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
B1 = {} by A66, A70, RELAT_1:41;
hence B = C by A66, A69, A71, RELAT_1:41; :: thesis: verum

end;

end;

end;

end;

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

end;

end;