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 :: 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 A4: 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, Th21;
hence ( g * f1 = g * f2 implies f1 = f2 ) by A3, A4; :: thesis: verum

end;

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