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

now

let c be Object of C; :: thesis: for g1, g2 being Morphism of c,b st Hom c,b <> {} & g * g1 = g * g2 holds
g1 = g2
let g1, g2 be Morphism of c,b; :: thesis: ( Hom c,b <> {} & g * g1 = g * g2 implies g1 = g2 )
assume that
A4: Hom c,b <> {} and
A5: g * g1 = g * g2 ; :: thesis: g1 = g2
thus g1 = (h * g) * g1 by A3, A4, Th57
.= h * (g * g2) by A1, A2, A4, A5, Th54
.= (h * g) * g2 by A1, A2, A4, Th54
.= g2 by A3, A4, Th57 ; :: thesis: verum

end;

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