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 )
assume A1: id a = id b ; :: thesis: a = b
thus a = dom (id a)
.= b by Th53, A1 ; :: thesis: verum