let C be Category; :: thesis: for a, b being Object of C st id a = id b holds
a = b
let a, b be Object of C; :: thesis: ( id a = id b implies a = b )
dom (id a) = a by Def8;
hence ( id a = id b implies a = b ) by Def8; :: thesis: verum