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