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

now

let d be Object of C; :: thesis: for h1, h2 being Morphism of c,d st Hom (c,d) <> {} & h1 * g = h2 * g holds
h1 = h2
let h1, h2 be Morphism of c,d; :: thesis: ( Hom (c,d) <> {} & h1 * g = h2 * g implies h1 = h2 )
A4: Hom (a,c) <> {} by A1, A2, Th51;
assume A5: Hom (c,d) <> {} ; :: thesis: ( h1 * g = h2 * g implies h1 = h2 )
then ( h1 * (g * f) = (h1 * g) * f & h2 * (g * f) = (h2 * g) * f ) by A1, A2, Th54;
hence ( h1 * g = h2 * g implies h1 = h2 ) by A3, A5, A4, Th65; :: thesis: verum

end;

hence g is epi by A2, Th65; :: thesis: verum