let C be set-id-inheriting carrier-underlaid category; :: thesis: for a being Object of C holds idm a = id (a as_1-sorted)

let a be Object of C; :: thesis: idm a = id (a as_1-sorted)

ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S ) by Def3;

then the_carrier_of a = the carrier of (a as_1-sorted) by Def1;

hence idm a = id (a as_1-sorted) by YELLOW18:def 10; :: thesis: verum

let a be Object of C; :: thesis: idm a = id (a as_1-sorted)

ex S being 1-sorted st

( a = S & the_carrier_of a = the carrier of S ) by Def3;

then the_carrier_of a = the carrier of (a as_1-sorted) by Def1;

hence idm a = id (a as_1-sorted) by YELLOW18:def 10; :: thesis: verum