let A be non empty set ; :: thesis: for a being Object of (EnsCat A) holds the_carrier_of a = a
let a be Object of (EnsCat A); :: thesis: the_carrier_of a = a
thus the_carrier_of a = proj1 (id a) by Th31
.= a ; :: thesis: verum