let C be Category; 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; 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; 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; ( 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
; g is monic
now for c being Object of C
for g1, g2 being Morphism of c,b st Hom (c,b) <> {} & g * g1 = g * g2 holds
g1 = g2let c be
Object of
C;
for g1, g2 being Morphism of c,b st Hom (c,b) <> {} & g * g1 = g * g2 holds
g1 = g2let g1,
g2 be
Morphism of
c,
b;
( Hom (c,b) <> {} & g * g1 = g * g2 implies g1 = g2 )assume that A4:
Hom (
c,
b)
<> {}
and A5:
g * g1 = g * g2
;
g1 = g2thus 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
;
verum end;
hence
g is monic
by A2; verum