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 :: thesis: for c being Object of C
for g1, g2 being Morphism of c,b st Hom (c,b) <> {} & g * g1 = g * g2 holds
g1 = g2

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, Th23
.= h * (g * g2) by A1, A2, A4, A5, Th21
.= (h * g) * g2 by A1, A2, A4, Th21
.= g2 by A3, A4, Th23 ; :: thesis: verum

end;

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