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