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) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

let a, b be Object of (Ens V); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ( f is monic iff (@ f) `2 is one-to-one ) )

assume A1: Hom (a,b) <> {} ; :: thesis: ( f is monic iff (@ f) `2 is one-to-one )

set m = @ f;

A2: dom (@ f) = dom f by Def9;

then A3: dom ((@ f) `2) = dom f by Lm3;

thus ( f is monic implies (@ f) `2 is one-to-one ) :: thesis: ( (@ f) `2 is one-to-one implies f is monic )

thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b_{1} being Element of the carrier of (Ens V) holds

( Hom (b_{1},a) = {} or for b_{2}, b_{3} being Morphism of b_{1},a holds

( not f * b_{2} = f * b_{3} or b_{2} = b_{3} ) )

let c be Object of (Ens V); :: thesis: ( Hom (c,a) = {} or for b_{1}, b_{2} being Morphism of c,a holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} ) )

assume A29: Hom (c,a) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of c,a holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} )

let f1, f2 be Morphism of c,a; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )

A30: dom f1 = c by A29, CAT_1:5

.= dom f2 by A29, CAT_1:5 ;

A31: cod f1 = a by A29, CAT_1:5

.= dom f by A1, CAT_1:5 ;

A32: cod f2 = a by A29, CAT_1:5

.= dom f by A1, CAT_1:5 ;

assume A33: f * f1 = f * f2 ; :: thesis: f1 = f2

set m1 = @ f1;

set m2 = @ f2;

A34: (@ f) * (@ f1) = f (*) f1 by A31, Th27

.= f * f1 by A29, A1, CAT_1:def 13 ;

A35: (@ f) * (@ f2) = f (*) f2 by A32, Th27

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

A36: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;

A37: dom (@ f2) = dom f2 by Def9;

then A38: dom ((@ f2) `2) = dom f2 by Lm3;

A39: cod (@ f1) = cod f1 by Def10;

then A40: rng ((@ f1) `2) c= cod f1 by Lm3;

A41: cod (@ f2) = cod f2 by Def10;

then A42: rng ((@ f2) `2) c= cod f2 by Lm3;

A43: (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))] by A32, A41, A2, Def6;

(@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))] by A31, A39, A2, Def6;

then A44: ((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2) by A35, A33, A34, A43, XTUPLE_0:1;

A45: dom (@ f1) = dom f1 by Def9;

then dom ((@ f1) `2) = dom f1 by Lm3;

then (@ f1) `2 = (@ f2) `2 by A28, A30, A31, A32, A38, A3, A40, A42, A44, FUNCT_1:27;

hence f1 = f2 by A30, A31, A32, A45, A37, A39, A41, A36, Th8; :: thesis: verum

for f being Morphism of a,b st Hom (a,b) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

let a, b be Object of (Ens V); :: thesis: for f being Morphism of a,b st Hom (a,b) <> {} holds

( f is monic iff (@ f) `2 is one-to-one )

let f be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} implies ( f is monic iff (@ f) `2 is one-to-one ) )

assume A1: Hom (a,b) <> {} ; :: thesis: ( f is monic iff (@ f) `2 is one-to-one )

set m = @ f;

A2: dom (@ f) = dom f by Def9;

then A3: dom ((@ f) `2) = dom f by Lm3;

thus ( f is monic implies (@ f) `2 is one-to-one ) :: thesis: ( (@ f) `2 is one-to-one implies f is monic )

proof

assume A28:
(@ f) `2 is one-to-one
; :: thesis: f is monic
set A = dom ((@ f) `2);

assume A4: f is monic ; :: thesis: (@ f) `2 is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 ((@ f) `2) or not x2 in proj1 ((@ f) `2) or not ((@ f) `2) . x1 = ((@ f) `2) . x2 or x1 = x2 )

assume that

A5: x1 in dom ((@ f) `2) and

A6: x2 in dom ((@ f) `2) and

A7: ((@ f) `2) . x1 = ((@ f) `2) . x2 ; :: thesis: x1 = x2

A8: dom ((@ f) `2) = dom (@ f) by Lm3;

then reconsider A = dom ((@ f) `2) as Element of V ;

A9: dom f = A by A8, Def9;

reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A5, A6, FUNCOP_1:45;

reconsider m1 = [[A,A],fx1], m2 = [[A,A],fx2] as Element of Maps V by Th5;

set f1 = @ m1;

set f2 = @ m2;

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

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

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

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

A10: cod m2 = A ;

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

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

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

dom (@ (@ m2)) = A ;

then A13: dom (@ m2) = A by Def9;

cod (@ (@ m2)) = A ;

then A14: cod (@ m2) = A by Def10;

then A15: f (*) (@ m2) = (@ f) * (@ (@ m2)) by A9, Th27;

A16: cod m1 = A ;

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

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

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

dom (@ (@ m1)) = A ;

then A23: dom (@ m1) = A by Def9;

cod (@ (@ m1)) = A ;

then A24: cod (@ m1) = A by Def10;

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

A25: dom f = a by A1, CAT_1:5;

then A26: ( @ m1 in Hom (A,a) & @ m2 in Hom (A,a) ) by A23, A9, A24, A13, A14;

then reconsider f1 = @ m1, f2 = @ m2 as Morphism of A,a by CAT_1:def 5;

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

.= f (*) f2 by A22, A12, A21, A15, A24, A9, Th27

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

Hom (A,a) <> {} by A25, A9;

then f1 = f2 by A4, A27;

then fx1 = fx2 by XTUPLE_0:1;

hence x1 = fx2 . x1 by A5, FUNCOP_1:7

.= x2 by A5, FUNCOP_1:7 ;

:: thesis: verum

end;assume A4: f is monic ; :: thesis: (@ f) `2 is one-to-one

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 ((@ f) `2) or not x2 in proj1 ((@ f) `2) or not ((@ f) `2) . x1 = ((@ f) `2) . x2 or x1 = x2 )

assume that

A5: x1 in dom ((@ f) `2) and

A6: x2 in dom ((@ f) `2) and

A7: ((@ f) `2) . x1 = ((@ f) `2) . x2 ; :: thesis: x1 = x2

A8: dom ((@ f) `2) = dom (@ f) by Lm3;

then reconsider A = dom ((@ f) `2) as Element of V ;

A9: dom f = A by A8, Def9;

reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A5, A6, FUNCOP_1:45;

reconsider m1 = [[A,A],fx1], m2 = [[A,A],fx2] as Element of Maps V by Th5;

set f1 = @ m1;

set f2 = @ m2;

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

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

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

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

A10: cod m2 = A ;

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

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

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

dom (@ (@ m2)) = A ;

then A13: dom (@ m2) = A by Def9;

cod (@ (@ m2)) = A ;

then A14: cod (@ m2) = A by Def10;

then A15: f (*) (@ m2) = (@ f) * (@ (@ m2)) by A9, Th27;

A16: cod m1 = A ;

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

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

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

then A21:
((@ f) `2) * ((@ (@ m1)) `2) = ((@ f) `2) * ((@ (@ m2)) `2)
;(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x ) )

thus A18:
( dom (((@ f) `2) * ((@ (@ m1)) `2)) = A & dom (((@ f) `2) * ((@ (@ m2)) `2)) = A )
by A17, A11, Lm3; :: thesis: for x being object st x in A holds

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

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

assume A19: x in A ; :: thesis: (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x

((@ (@ m1)) `2) . x = x1 by A19, FUNCOP_1:7;

then A20: (((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1 by A18, A19, FUNCT_1:12;

((@ (@ m2)) `2) . x = x2 by A19, FUNCOP_1:7;

hence (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x by A7, A18, A19, A20, FUNCT_1:12; :: thesis: verum

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

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

assume A19: x in A ; :: thesis: (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x

((@ (@ m1)) `2) . x = x1 by A19, FUNCOP_1:7;

then A20: (((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1 by A18, A19, FUNCT_1:12;

((@ (@ m2)) `2) . x = x2 by A19, FUNCOP_1:7;

hence (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x by A7, A18, A19, A20, FUNCT_1:12; :: thesis: verum

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

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

dom (@ (@ m1)) = A ;

then A23: dom (@ m1) = A by Def9;

cod (@ (@ m1)) = A ;

then A24: cod (@ m1) = A by Def10;

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

A25: dom f = a by A1, CAT_1:5;

then A26: ( @ m1 in Hom (A,a) & @ m2 in Hom (A,a) ) by A23, A9, A24, A13, A14;

then reconsider f1 = @ m1, f2 = @ m2 as Morphism of A,a by CAT_1:def 5;

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

.= f (*) f2 by A22, A12, A21, A15, A24, A9, Th27

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

Hom (A,a) <> {} by A25, A9;

then f1 = f2 by A4, A27;

then fx1 = fx2 by XTUPLE_0:1;

hence x1 = fx2 . x1 by A5, FUNCOP_1:7

.= x2 by A5, FUNCOP_1:7 ;

:: thesis: verum

thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b

( Hom (b

( not f * b

let c be Object of (Ens V); :: thesis: ( Hom (c,a) = {} or for b

( not f * b

assume A29: Hom (c,a) <> {} ; :: thesis: for b

( not f * b

let f1, f2 be Morphism of c,a; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )

A30: dom f1 = c by A29, CAT_1:5

.= dom f2 by A29, CAT_1:5 ;

A31: cod f1 = a by A29, CAT_1:5

.= dom f by A1, CAT_1:5 ;

A32: cod f2 = a by A29, CAT_1:5

.= dom f by A1, CAT_1:5 ;

assume A33: f * f1 = f * f2 ; :: thesis: f1 = f2

set m1 = @ f1;

set m2 = @ f2;

A34: (@ f) * (@ f1) = f (*) f1 by A31, Th27

.= f * f1 by A29, A1, CAT_1:def 13 ;

A35: (@ f) * (@ f2) = f (*) f2 by A32, Th27

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

A36: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;

A37: dom (@ f2) = dom f2 by Def9;

then A38: dom ((@ f2) `2) = dom f2 by Lm3;

A39: cod (@ f1) = cod f1 by Def10;

then A40: rng ((@ f1) `2) c= cod f1 by Lm3;

A41: cod (@ f2) = cod f2 by Def10;

then A42: rng ((@ f2) `2) c= cod f2 by Lm3;

A43: (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))] by A32, A41, A2, Def6;

(@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))] by A31, A39, A2, Def6;

then A44: ((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2) by A35, A33, A34, A43, XTUPLE_0:1;

A45: dom (@ f1) = dom f1 by Def9;

then dom ((@ f1) `2) = dom f1 by Lm3;

then (@ f1) `2 = (@ f2) `2 by A28, A30, A31, A32, A38, A3, A40, A42, A44, FUNCT_1:27;

hence f1 = f2 by A30, A31, A32, A45, A37, A39, A41, A36, Th8; :: thesis: verum