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:14;
hence A = 1-Alg (MSAlg A) by Def17; :: thesis: verum