let A be Category; :: thesis: for a being Object of A holds Result ((idsym a),(MSAlg A)) = Hom (a,a)
let a be Object of A; :: thesis: Result ((idsym a),(MSAlg A)) = Hom (a,a)
thus Result ((idsym a),(MSAlg A)) = the Sorts of (MSAlg A) . (the_result_sort_of (idsym a)) by PRALG_2:3
.= the Sorts of (MSAlg A) . (homsym (a,a)) by Def3
.= Hom (a,a) by Def13 ; :: thesis: verum