let U1, U2 be Universal_Algebra; :: thesis: ( U1 is SubAlgebra of U2 implies the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) )
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;
A1: MSSign U2 = ManySortedSign(# {0},(dom (signature U2)),gg1,((dom (signature U2)) --> z) #) by MSUALG_1:10;
MSAlg U2 = MSAlgebra(# (MSSorts U2),(MSCharact U2) #) by MSUALG_1:def 11;
then A2: the Sorts of (MSAlg U2) = 0 .--> the carrier of U2 by MSUALG_1:def 9;
assume A3: U1 is SubAlgebra of U2 ; :: thesis: the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2)
then MSSign U1 = MSSign U2 by Th7;
then reconsider A = MSAlg U1 as non-empty MSAlgebra over MSSign U2 ;
MSAlg U1 = MSAlgebra(# (MSSorts U1),(MSCharact U1) #) by MSUALG_1:def 11;
then A4: the Sorts of A = 0 .--> the carrier of U1 by MSUALG_1:def 9;
A5: 0 in {0} by TARSKI:def 1;
A6: the carrier of U1 is Subset of U2 by A3, UNIALG_2:def 7;
the Sorts of A c= the Sorts of (MSAlg U2)
proof
let i be object ; :: according to PBOOLE:def 2 :: 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 A7: i = 0 by A1, TARSKI:def 1;
( the Sorts of A . 0 = the carrier of U1 & the Sorts of (MSAlg U2) . 0 = the carrier of U2 ) by A4, A2, A5, FUNCOP_1:7;
hence the Sorts of A . i c= the Sorts of (MSAlg U2) . i by A6, A7; :: thesis: verum
end;
hence the Sorts of (MSAlg U1) is MSSubset of (MSAlg U2) by PBOOLE:def 18; :: thesis: verum