let C be Category; :: thesis: for b, c being Object of C
for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
let b, c be Object of C; :: thesis: for g being Morphism of b,c st Hom (b,c) <> {} holds
( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
let g be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} implies ( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) )
assume A1: Hom (b,c) <> {} ; :: thesis: ( g is monic iff for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 )
thus ( g is monic implies for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) :: thesis: ( ( for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ) implies g is monic )

proof

assume A2: for f1, f2 being Morphism of C st dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g * f1 = g * f2 holds
f1 = f2 ; :: according to CAT_1:def 7 :: thesis: for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2
let a be Object of C; :: thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2
let f1, f2 be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & g * f1 = g * f2 implies f1 = f2 )
assume A3: Hom (a,b) <> {} ; :: thesis: ( not g * f1 = g * f2 or f1 = f2 )
then A4: ( dom f1 = a & dom f2 = a ) by Th23;
A5: dom g = b by A1, Th23;
A6: ( cod f1 = b & cod f2 = b ) by A3, Th23;
( g * f2 = g * f2 & g * f1 = g * f1 ) by A1, A3, Def13;
hence ( not g * f1 = g * f2 or f1 = f2 ) by A2, A4, A6, A5; :: thesis: verum

end;

assume A7: for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & g * f1 = g * f2 holds
f1 = f2 ; :: thesis: g is monic
let f1, f2 be Morphism of C; :: according to CAT_1:def 7 :: thesis: ( dom f1 = dom f2 & cod f1 = dom g & cod f2 = dom g & g * f1 = g * f2 implies f1 = f2 )
assume that
A8: dom f1 = dom f2 and
A9: cod f1 = dom g and
A10: cod f2 = dom g ; :: thesis: ( not g * f1 = g * f2 or f1 = f2 )
set a = dom f1;
A11: dom g = b by A1, Th23;
then reconsider f1 = f1 as Morphism of dom f1,b by A9, Th22;
reconsider f2 = f2 as Morphism of dom f1,b by A8, A10, A11, Th22;
A12: Hom ((dom f1),b) <> {} by A9, A11, Th18;
then ( g * f2 = g * f2 & g * f1 = g * f1 ) by A1, Def13;
hence ( not g * f1 = g * f2 or f1 = f2 ) by A7, A12; :: thesis: verum