theorem :: MSUHOM_1:25

for U1 being Universal_Algebra holds MSAlg (id the carrier of U1) = id the Sorts of (MSAlg U1)