let C be Category; :: thesis: for b, c, d being Object of C
for g being Morphism of b,c
for h being Morphism of c,d st Hom b,c <> {} & Hom c,d <> {} & h * g is monic holds
g is monic
let b, c, d be Object of C; :: thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom b,c <> {} & Hom c,d <> {} & h * g is monic holds
g is monic
let g be Morphism of b,c; :: thesis: for h being Morphism of c,d st Hom b,c <> {} & Hom c,d <> {} & h * g is monic holds
g is monic
let h be Morphism of c,d; :: thesis: ( Hom b,c <> {} & Hom c,d <> {} & h * g is monic implies g is monic )
assume that
A1: Hom b,c <> {} and
A2: Hom c,d <> {} and
A3: h * g is monic ; :: thesis: g is monic

now

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 )
A4: Hom b,d <> {} by A1, A2, Th51;
assume A5: Hom a,b <> {} ; :: thesis: ( g * f1 = g * f2 implies f1 = f2 )
then ( h * (g * f1) = (h * g) * f1 & h * (g * f2) = (h * g) * f2 ) by A1, A2, Th54;
hence ( g * f1 = g * f2 implies f1 = f2 ) by A3, A5, A4, Th60; :: thesis: verum

end;

hence g is monic by A1, Th60; :: thesis: verum