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 )

proof

set A = dom ((@ f) `2);
assume A4: f is monic ; :: thesis: (@ f) `2 is one-to-one
let x1, x2 be set ; :: 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: m2 = [[(dom m2),(cod m2)],(m2 `2)] by Th8;
then A11: dom m2 = A by Lm1;
A12: cod m2 = A by A10, Lm1;
then A13: ( ((@ f) * (@ (@ m2))) `2 = ((@ f) `2) * ((@ (@ m2)) `2) & dom ((@ f) * (@ (@ m2))) = dom (@ (@ m2)) ) by A8, Th12;
cod ((@ f) * (@ (@ m2))) = cod (@ f) by A8, A12, Th12;
then A14: (@ f) * (@ (@ m2)) = [[(dom (@ (@ m2))),(cod (@ f))],(((@ f) `2) * ((@ (@ m2)) `2))] by A13, Th8;
dom (@ (@ m2)) = A by A10, Lm1;
then A15: dom (@ m2) = A by Def9;
cod (@ (@ m2)) = A by A10, Lm1;
then A16: cod (@ m2) = A by Def10;
then A17: f (*) (@ m2) = (@ f) * (@ (@ m2)) by A9, Th28;
A18: m1 = [[(dom m1),(cod m1)],(m1 `2)] by Th8;
then A19: cod m1 = A by Lm1;
then A20: ( ((@ f) * (@ (@ m1))) `2 = ((@ f) `2) * ((@ (@ m1)) `2) & dom ((@ f) * (@ (@ m1))) = dom (@ (@ m1)) ) by A8, Th12;
A21: dom m1 = A by A18, Lm1;

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

thus A22: ( dom (((@ f) `2) * ((@ (@ m1)) `2)) = A & dom (((@ f) `2) * ((@ (@ m2)) `2)) = A ) by A21, A11, A20, A13, Lm3; :: thesis: for x being set st x in A holds
(((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
let x be set ; :: thesis: ( x in A implies (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x )
assume A23: x in A ; :: thesis: (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
fx1 = m1 `2 by A18, XTUPLE_0:1;
then ((@ (@ m1)) `2) . x = x1 by A23, FUNCOP_1:7;
then A24: (((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1 by A22, A23, FUNCT_1:12;
fx2 = m2 `2 by A10, XTUPLE_0:1;
then ((@ (@ m2)) `2) . x = x2 by A23, FUNCOP_1:7;
hence (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x by A7, A22, A23, A24, FUNCT_1:12; :: thesis: verum

end;

then A25: ((@ f) `2) * ((@ (@ m1)) `2) = ((@ f) `2) * ((@ (@ m2)) `2) by FUNCT_1:2;
cod ((@ f) * (@ (@ m1))) = cod (@ f) by A8, A19, Th12;
then A26: (@ f) * (@ (@ m1)) = [[(dom (@ (@ m1))),(cod (@ f))],(((@ f) `2) * ((@ (@ m1)) `2))] by A20, Th8;
dom (@ (@ m1)) = A by A18, Lm1;
then A27: dom (@ m1) = A by Def9;
cod (@ (@ m1)) = A by A18, Lm1;
then A28: cod (@ m1) = A by Def10;
reconsider A = A as Object of (Ens V) ;
A29: dom f = a by A1, CAT_1:5;
then A30: ( @ m1 in Hom (A,a) & @ m2 in Hom (A,a) ) by A27, A9, A28, A15, A16;
then reconsider f1 = @ m1, f2 = @ m2 as Morphism of A,a by CAT_1:def 5;
A31: f * f1 = f (*) f1 by A1, A30, CAT_1:def 13
.= f (*) f2 by A21, A11, A26, A14, A25, A17, A28, A9, Th28
.= f * f2 by A1, A30, CAT_1:def 13 ;
Hom (A,a) <> {} by A29, A9;
then f1 = f2 by A4, A31, CAT_1:def 14;
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 A32: (@ f) `2 is one-to-one ; :: thesis: f is monic
thus Hom (a,b) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b<sub>1</sub> being Element of the carrier of (Ens V) holds
( Hom (b<sub>1</sub>,a) = {} or for b<sub>2</sub>, b<sub>3</sub> being Morphism of b<sub>1</sub>,a holds
( not f * b<sub>2</sub> = f * b<sub>3</sub> or b<sub>2</sub> = b<sub>3</sub> ) )
let c be Object of (Ens V); :: thesis: ( Hom (c,a) = {} or for b<sub>1</sub>, b<sub>2</sub> being Morphism of c,a holds
( not f * b<sub>1</sub> = f * b<sub>2</sub> or b<sub>1</sub> = b<sub>2</sub> ) )
assume A33: Hom (c,a) <> {} ; :: thesis: for b<sub>1</sub>, b<sub>2</sub> being Morphism of c,a holds
( not f * b<sub>1</sub> = f * b<sub>2</sub> or b<sub>1</sub> = b<sub>2</sub> )
let f1, f2 be Morphism of c,a; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )
A34: dom f1 = c by A33, CAT_1:5
.= dom f2 by A33, CAT_1:5 ;
A35: cod f1 = a by A33, CAT_1:5
.= dom f by A1, CAT_1:5 ;
A36: cod f2 = a by A33, CAT_1:5
.= dom f by A1, CAT_1:5 ;
assume A37: f * f1 = f * f2 ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A38: (@ f) * (@ f1) = f (*) f1 by A35, Th28
.= f * f1 by A33, A1, CAT_1:def 13 ;
A39: (@ f) * (@ f2) = f (*) f2 by A36, Th28
.= f * f2 by A33, A1, CAT_1:def 13 ;
A40: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A41: dom (@ f2) = dom f2 by Def9;
then A42: dom ((@ f2) `2) = dom f2 by Lm3;
A43: cod (@ f1) = cod f1 by Def10;
then A44: rng ((@ f1) `2) c= cod f1 by Lm3;
A45: cod (@ f2) = cod f2 by Def10;
then A46: rng ((@ f2) `2) c= cod f2 by Lm3;
A47: (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))] by A36, A45, A2, Def6;
(@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))] by A35, A43, A2, Def6;
then A48: ((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2) by A39, A37, A38, A47, XTUPLE_0:1;
A49: dom (@ f1) = dom f1 by Def9;
then dom ((@ f1) `2) = dom f1 by Lm3;
then (@ f1) `2 = (@ f2) `2 by A32, A34, A35, A36, A42, A3, A44, A46, A48, FUNCT_1:27;
hence f1 = f2 by A34, A35, A36, A49, A41, A43, A45, A40, Th8; :: thesis: verum