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

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