let S be non void Signature; :: thesis: for X being ManySortedSet of the carrier of S holds the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> )))
let X be ManySortedSet of the carrier of S; :: thesis: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> )))
set Y = X (\/) ( the carrier of S --> );
set B = MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> )))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> ))),(S -Terms (X,(X (\/) ( the carrier of S --> )))))) #);
for Z being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) st Z = the Sorts of MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> )))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> ))),(S -Terms (X,(X (\/) ( the carrier of S --> )))))) #) holds
( Z is opers_closed & the Charact of MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> )))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> ))),(S -Terms (X,(X (\/) ( the carrier of S --> )))))) #) = Opers ((FreeMSA (X (\/) ( the carrier of S --> ))),Z) ) by Th21;
then reconsider B = MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> )))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> ))),(S -Terms (X,(X (\/) ( the carrier of S --> )))))) #) as MSSubAlgebra of FreeMSA (X (\/) ( the carrier of S --> )) by MSUALG_2:def 9;
A1: ( FreeMSA (X (\/) ( the carrier of S --> )) = MSAlgebra(# (FreeSort (X (\/) ( the carrier of S --> ))),(FreeOper (X (\/) ( the carrier of S --> ))) #) & dom (FreeSort (X (\/) ( the carrier of S --> ))) = the carrier of S ) by ;
(Reverse (X (\/) ( the carrier of S --> ))) "" X c= S -Terms (X,(X (\/) ( the carrier of S --> ))) by Th22;
then A2: (Reverse (X (\/) ( the carrier of S --> ))) "" X is MSSubset of B by PBOOLE:def 18;
let s be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (Free (S,X)) . s = (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s
ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> ))) "" X ) by Def1;
then Free (S,X) is MSSubAlgebra of B by ;
then the Sorts of (Free (S,X)) is MSSubset of B by MSUALG_2:def 9;
then the Sorts of (Free (S,X)) c= S -Terms (X,(X (\/) ( the carrier of S --> ))) by PBOOLE:def 18;
hence the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s ; :: according to XBOOLE_0:def 10 :: thesis: (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s c= the Sorts of (Free (S,X)) . s
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s or x in the Sorts of (Free (S,X)) . s )
assume A3: x in (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s ; :: thesis: x in the Sorts of (Free (S,X)) . s
S -Terms (X,(X (\/) ( the carrier of S --> ))) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) by PBOOLE:def 18;
then (S -Terms (X,(X (\/) ( the carrier of S --> )))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) . s ;
then x in Union (FreeSort (X (\/) ( the carrier of S --> ))) by ;
then x is Term of S,(X (\/) ( the carrier of S --> )) by MSATERM:13;
hence x in the Sorts of (Free (S,X)) . s by ; :: thesis: verum