let V be non empty set ; :: thesis: for f being Morphism of (Ens V) holds
( f is monic iff (@ f) `2 is one-to-one )
let f be Morphism of (Ens V); :: thesis: ( f is monic iff (@ f) `2 is one-to-one )
set m = @ f;
A1: dom (@ f) = dom f by Def10;
then A2: 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 A3: f is monic ; :: thesis: (@ f) `2 is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: 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
A4: x1 in dom ((@ f) `2) and
A5: x2 in dom ((@ f) `2) and
A6: ((@ f) `2) . x1 = ((@ f) `2) . x2 ; :: thesis: x1 = x2
A7: dom ((@ f) `2) = dom (@ f) by Lm3;
then reconsider A = dom ((@ f) `2) as Element of V ;
A8: dom f = A by A7, Def10;
reconsider fx1 = A --> x1, fx2 = A --> x2 as Function of A,A by A4, A5, FUNCOP_1:57;
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));
A9: m2 = [[(dom m2),(cod m2)],(m2 `2)] by Th8;
then A10: dom m2 = A by Lm1;
A11: cod m2 = A by A9, Lm1;
then A12: ( ((@ f) * (@ (@ m2))) `2 = ((@ f) `2) * ((@ (@ m2)) `2) & dom ((@ f) * (@ (@ m2))) = dom (@ (@ m2)) ) by A7, Th12;
cod ((@ f) * (@ (@ m2))) = cod (@ f) by A7, A11, Th12;
then A13: (@ f) * (@ (@ m2)) = [[(dom (@ (@ m2))),(cod (@ f))],(((@ f) `2) * ((@ (@ m2)) `2))] by A12, Th8;
dom (@ (@ m2)) = A by A9, Lm1;
then A14: dom (@ m2) = A by Def10;
cod (@ (@ m2)) = A by A9, Lm1;
then A15: cod (@ m2) = A by Def11;
then A16: f * (@ m2) = (@ f) * (@ (@ m2)) by A8, Th28;
A17: m1 = [[(dom m1),(cod m1)],(m1 `2)] by Th8;
then A18: cod m1 = A by Lm1;
then A19: ( ((@ f) * (@ (@ m1))) `2 = ((@ f) `2) * ((@ (@ m1)) `2) & dom ((@ f) * (@ (@ m1))) = dom (@ (@ m1)) ) by A7, Th12;
A20: dom m1 = A by A17, Lm1;

now

thus A21: ( dom (((@ f) `2) * ((@ (@ m1)) `2)) = A & dom (((@ f) `2) * ((@ (@ m2)) `2)) = A ) by A20, A10, A19, A12, 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 A22: x in A ; :: thesis: (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x
fx1 = m1 `2 by A17, ZFMISC_1:33;
then ((@ (@ m1)) `2) . x = x1 by A22, FUNCOP_1:13;
then A23: (((@ f) `2) * ((@ (@ m1)) `2)) . x = ((@ f) `2) . x1 by A21, A22, FUNCT_1:22;
fx2 = m2 `2 by A9, ZFMISC_1:33;
then ((@ (@ m2)) `2) . x = x2 by A22, FUNCOP_1:13;
hence (((@ f) `2) * ((@ (@ m1)) `2)) . x = (((@ f) `2) * ((@ (@ m2)) `2)) . x by A6, A21, A22, A23, FUNCT_1:22; :: thesis: verum

end;

then A24: ((@ f) `2) * ((@ (@ m1)) `2) = ((@ f) `2) * ((@ (@ m2)) `2) by FUNCT_1:9;
cod ((@ f) * (@ (@ m1))) = cod (@ f) by A7, A18, Th12;
then A25: (@ f) * (@ (@ m1)) = [[(dom (@ (@ m1))),(cod (@ f))],(((@ f) `2) * ((@ (@ m1)) `2))] by A19, Th8;
dom (@ (@ m1)) = A by A17, Lm1;
then A26: dom (@ m1) = A by Def10;
cod (@ (@ m1)) = A by A17, Lm1;
then A27: cod (@ m1) = A by Def11;
then f * (@ m1) = (@ f) * (@ (@ m1)) by A8, Th28;
then @ m1 = @ m2 by A3, A20, A10, A26, A14, A27, A15, A8, A25, A13, A24, A16, CAT_1:def 10;
then fx1 = fx2 by ZFMISC_1:33;
hence x1 = fx2 . x1 by A4, FUNCOP_1:13
.= x2 by A4, FUNCOP_1:13 ;
:: thesis: verum

end;

assume A28: (@ f) `2 is one-to-one ; :: thesis: f is monic
let f1 be Morphism of (Ens V); :: according to CAT_1:def 10 :: thesis: for b<sub>1</sub> being Element of the carrier' of (Ens V) holds
( not dom f1 = dom b<sub>1</sub> or not cod f1 = dom f or not cod b<sub>1</sub> = dom f or not f * f1 = f * b<sub>1</sub> or f1 = b<sub>1</sub> )
let f2 be Morphism of (Ens V); :: thesis: ( not dom f1 = dom f2 or not cod f1 = dom f or not cod f2 = dom f or not f * f1 = f * f2 or f1 = f2 )
assume that
A29: dom f1 = dom f2 and
A30: cod f1 = dom f and
A31: cod f2 = dom f and
A32: f * f1 = f * f2 ; :: thesis: f1 = f2
set m1 = @ f1;
set m2 = @ f2;
A33: ( (@ f) * (@ f1) = f * f1 & (@ f) * (@ f2) = f * f2 ) by A30, A31, Th28;
A34: @ f1 = [[(dom (@ f1)),(cod (@ f1))],((@ f1) `2)] by Th8;
A35: dom (@ f2) = dom f2 by Def10;
then A36: dom ((@ f2) `2) = dom f2 by Lm3;
A37: cod (@ f1) = cod f1 by Def11;
then A38: rng ((@ f1) `2) c= cod f1 by Lm3;
A39: cod (@ f2) = cod f2 by Def11;
then A40: rng ((@ f2) `2) c= cod f2 by Lm3;
A41: (@ f) * (@ f2) = [[(dom (@ f2)),(cod (@ f))],(((@ f) `2) * ((@ f2) `2))] by A31, A39, A1, Def7;
(@ f) * (@ f1) = [[(dom (@ f1)),(cod (@ f))],(((@ f) `2) * ((@ f1) `2))] by A30, A37, A1, Def7;
then A42: ((@ f) `2) * ((@ f1) `2) = ((@ f) `2) * ((@ f2) `2) by A32, A33, A41, ZFMISC_1:33;
A43: dom (@ f1) = dom f1 by Def10;
then dom ((@ f1) `2) = dom f1 by Lm3;
then (@ f1) `2 = (@ f2) `2 by A28, A29, A30, A31, A36, A2, A38, A40, A42, FUNCT_1:49;
hence f1 = f2 by A29, A30, A31, A43, A35, A37, A39, A34, Th8; :: thesis: verum