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
h is epi
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
h is epi
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
h is epi
let g be Morphism of b,a; ( Hom (a,b) <> {} & Hom (b,a) <> {} & h * g = id b implies h is epi )
assume that
A1:
Hom (a,b) <> {}
and
A2:
Hom (b,a) <> {}
and
A3:
h * g = id b
; h is epi
now for c being Object of C
for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds
h1 = h2let c be
Object of
C;
for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds
h1 = h2let h1,
h2 be
Morphism of
b,
c;
( Hom (b,c) <> {} & h1 * h = h2 * h implies h1 = h2 )assume that A4:
Hom (
b,
c)
<> {}
and A5:
h1 * h = h2 * h
;
h1 = h2thus h1 =
h1 * (h * g)
by A3, A4, Th24
.=
(h2 * h) * g
by A1, A2, A4, A5, Th21
.=
h2 * (h * g)
by A1, A2, A4, Th21
.=
h2
by A3, A4, Th24
;
verum end;
hence
h is epi
by A1; verum