let C be carrier-underlaid category; :: thesis: for a being Object of C holds the_carrier_of a = the carrier of (a as_1-sorted)
let a be Object of C; :: thesis: the_carrier_of a = the carrier of (a as_1-sorted)
ex S being 1-sorted st
( a = S & the_carrier_of a = the carrier of S ) by Def3;
hence the_carrier_of a = the carrier of (a as_1-sorted) by Def1; :: thesis: verum