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

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

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 A4, A6, Th19;
( h1 * (g * f) = (h1 * g) * f & (h2 * g) * f = h2 * (g * f) ) by A3, A4, A6, Th21;
then h1 * g = h2 * g by A1, A7, A8;
hence h1 = h2 by A2, A6; :: thesis: verum

end;

Hom (a,c) <> {} by A3, A4, Th19;
hence g * f is epi by A5; :: thesis: verum