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
h is epi
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
h is epi
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
h is epi
let g be Morphism of b,a; :: thesis: ( 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 ; :: thesis: h is epi

now :: thesis: for c being Object of C
for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds
h1 = h2

let c be Object of C; :: thesis: for h1, h2 being Morphism of b,c st Hom (b,c) <> {} & h1 * h = h2 * h holds
h1 = h2
let h1, h2 be Morphism of b,c; :: thesis: ( Hom (b,c) <> {} & h1 * h = h2 * h implies h1 = h2 )
assume that
A4: Hom (b,c) <> {} and
A5: h1 * h = h2 * h ; :: thesis: h1 = h2
thus 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 ; :: thesis: verum

end;

hence h is epi by A1; :: thesis: verum