let C be Category; :: thesis: for b being Object of C holds id b is epi
let b be Object of C; :: thesis: id b is epi

A1: now

let c be Object of C; :: thesis: for g1, g2 being Morphism of b,c st Hom b,c <> {} & g1 * (id b) = g2 * (id b) holds
g1 = g2
let g1, g2 be Morphism of b,c; :: thesis: ( Hom b,c <> {} & g1 * (id b) = g2 * (id b) implies g1 = g2 )
assume A2: Hom b,c <> {} ; :: thesis: ( g1 * (id b) = g2 * (id b) implies g1 = g2 )
then g1 * (id b) = g1 by Th58;
hence ( g1 * (id b) = g2 * (id b) implies g1 = g2 ) by A2, Th58; :: thesis: verum

end;

Hom b,b <> {} by Th55;
hence id b is epi by A1, Th65; :: thesis: verum