let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) )
assume A1: U1 is SubAlgebra of U2 ; :: thesis: the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)
then A2: the carrier of U1 is Subset of U2 by UNIALG_2:def 8;
MSSign U1 = MSSign U2 by A1, Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra of MSSign U2 ;
A3: MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 16;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 16;
then A4: the Sorts of A = 0 .--> the carrier of U1 by MSUALG_1:def 14;
A5: the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by A3, MSUALG_1:def 14;
set gg1 = (*--> 0 ) * (signature U2);
set gg2 = (dom (signature U2)) --> z;
reconsider gg1 = (*--> 0 ) * (signature U2) as Function of (dom (signature U2)),({0 } * ) by MSUALG_1:7;
A6: MSSign U2 = ManySortedSign(# {0 },(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:16;
A7: 0 in {0 } by TARSKI:def 1;
the Sorts of A is MSSubset of (MSAlg U2)

proof

thus the Sorts of A c= the Sorts of (MSAlg U2) :: according to PBOOLE:def 23 :: thesis: verum

proof

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of (MSSign U2) or the Sorts of A . i c= the Sorts of (MSAlg U2) . i )
assume i in the carrier of (MSSign U2) ; :: thesis: the Sorts of A . i c= the Sorts of (MSAlg U2) . i
then A8: i = 0 by A6, TARSKI:def 1;
A9: the Sorts of A . 0 = the carrier of U1 by A4, A7, FUNCOP_1:13;
the Sorts of (MSAlg U2) . 0 = the carrier of U2 by A5, A7, FUNCOP_1:13;
hence the Sorts of A . i c= the Sorts of (MSAlg U2) . i by A2, A8, A9; :: thesis: verum

end;

end;

hence the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) ; :: thesis: verum