let U1, U2 be Universal_Algebra; ( MSAlg U1 is MSSubAlgebra of MSAlg U2 implies the carrier of U1 is Subset of U2 )
set MU1 = MSAlg U1;
set MU2 = MSAlg U2;
assume A1:
MSAlg U1 is MSSubAlgebra of MSAlg U2
; the carrier of U1 is Subset of U2
then reconsider MU1 = MSAlg U1 as MSAlgebra over MSSign U2 ;
reconsider C = the Sorts of MU1 as MSSubset of (MSAlg U2) by A1, MSUALG_2:def 9;
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:2;
reconsider C1 = C as ManySortedSet of the carrier of (MSSign U2) ;
A2:
0 in {0}
by TARSKI:def 1;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #)
by MSUALG_1:def 11;
then A3:
C1 c= MSSorts U2
by PBOOLE:def 18;
( MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) & MSSorts U2 = 0 .--> the carrier of U2 )
by MSUALG_1:10, MSUALG_1:def 9;
then
( MU1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) & C1 . 0 c= ({0} --> the carrier of U2) . 0 )
by A3, MSUALG_1:def 11;
then
(MSSorts U1) . 0 c= the carrier of U2
by A2, FUNCOP_1:7;
then
(0 .--> the carrier of U1) . 0 c= the carrier of U2
by MSUALG_1:def 9;
hence
the carrier of U1 is Subset of U2
by A2, FUNCOP_1:7; verum