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:10
.= the Sorts of (MSAlg A) . (homsym a,a) by Def5
.= Hom a,a by Def15 ; :: thesis: verum