let A be strict Universal_Algebra; :: thesis: A = 1-Alg (MSAlg A)
the carrier of A in { the carrier of A} by TARSKI:def 1;
then the carrier of A in rng the Sorts of (MSAlg A) by FUNCOP_1:8;
hence A = 1-Alg (MSAlg A) by Def12; :: thesis: verum