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 :: thesis: for c being Object of C
for g1, g2 being Morphism of b,c st Hom (b,c) <> {} & g1 * (id b) = g2 * (id b) holds
g1 = g2
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 Th24;
hence ( g1 * (id b) = g2 * (id b) implies g1 = g2 ) by A2, Th24; :: thesis: verum
end;
thus id b is epi by A1; :: thesis: verum