let A be non empty set ; :: thesis: for a being object of holds the_carrier_of a = a
let a be object of ; :: thesis: the_carrier_of a = a
thus the_carrier_of a = proj1 (id a) by Th32
.= dom (id a)
.= a by RELAT_1:71 ; :: thesis: verum