let U1, U2 be Universal_Algebra; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum