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) <> {} & g is monic & h is monic holds
h * 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) <> {} & g is monic & h is monic holds
h * 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) <> {} & g is monic & h is monic holds
h * g is monic
let h be Morphism of c,d; :: thesis: ( Hom (b,c) <> {} & Hom (c,d) <> {} & g is monic & h is monic implies h * g is monic )
assume that
A1: Hom (b,c) <> {} and
A2: Hom (c,d) <> {} and
A3: g is monic and
A4: h is monic ; :: thesis: h * g is monic

A5: now

let a be Object of C; :: thesis: for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 holds
f1 = f2
let f1, f2 be Morphism of a,b; :: thesis: ( Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 implies f1 = f2 )
assume that
A6: Hom (a,b) <> {} and
A7: (h * g) * f1 = (h * g) * f2 ; :: thesis: f1 = f2
A8: Hom (a,c) <> {} by A1, A6, Th51;
( h * (g * f1) = (h * g) * f1 & (h * g) * f2 = h * (g * f2) ) by A1, A2, A6, Th54;
then g * f1 = g * f2 by A2, A4, A7, A8, Th60;
hence f1 = f2 by A1, A3, A6, Th60; :: thesis: verum

end;

Hom (b,d) <> {} by A1, A2, Th51;
hence h * g is monic by A5, Th60; :: thesis: verum