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

A1: now :: thesis: for a being Object of C
for f1, f2 being Morphism of a,b st Hom (a,b) <> {} & (id b) * f1 = (id b) * f2 holds
f1 = f2

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

end;

thus id b is monic by A1; :: thesis: verum