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

A5: now :: thesis: for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (h * g) * f1 = (h * g) * f2 holds
f1 = f2

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, Th23;
( h * (g * f1) = (h * g) * f1 & (h * g) * f2 = h * (g * f2) ) by A1, A2, A6, Th25;
then g * f1 = g * f2 by Defm, A4, A7, A8;
hence f1 = f2 by Defm, A3, A6; :: thesis: verum

end;

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