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 ) by Defm; :: 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 )
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
thus Hom (b,c) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2
thus for a being Object of C st Hom (a,b) <> {} holds
for f1, f2 being Morphism of a,b st g * f1 = g * f2 holds
f1 = f2 by A7; :: thesis: verum