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 <> {} & f is epi & g is epi holds
g * f 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 <> {} & f is epi & g is epi holds
g * f is epi
let f be Morphism of a,b; :: thesis: for g being Morphism of b,c st Hom a,b <> {} & Hom b,c <> {} & f is epi & g is epi holds
g * f is epi
let g be Morphism of b,c; :: thesis: ( Hom a,b <> {} & Hom b,c <> {} & f is epi & g is epi implies g * f is epi )
assume that
A1: Hom a,b <> {} and
A2: Hom b,c <> {} and
A3: f is epi and
A4: g is epi ; :: thesis: g * f is epi

A5: now

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

end;

Hom a,c <> {} by A1, A2, Th51;
hence g * f is epi by A5, Th65; :: thesis: verum