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