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 --> {0})))
let X be ManySortedSet of the carrier of S; :: thesis: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> {0})))
set Y = X (\/) ( the carrier of S --> {0});
set B = MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> {0})))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> {0}))),(S -Terms (X,(X (\/) ( the carrier of S --> {0})))))) #);
for Z being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st Z = the Sorts of MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> {0})))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> {0}))),(S -Terms (X,(X (\/) ( the carrier of S --> {0})))))) #) holds
( Z is opers_closed & the Charact of MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> {0})))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> {0}))),(S -Terms (X,(X (\/) ( the carrier of S --> {0})))))) #) = Opers ((FreeMSA (X (\/) ( the carrier of S --> {0}))),Z) ) by Th21;
then reconsider B = MSAlgebra(# (S -Terms (X,(X (\/) ( the carrier of S --> {0})))),(Opers ((FreeMSA (X (\/) ( the carrier of S --> {0}))),(S -Terms (X,(X (\/) ( the carrier of S --> {0})))))) #) as MSSubAlgebra of FreeMSA (X (\/) ( the carrier of S --> {0})) by MSUALG_2:def 9;
A1: ( FreeMSA (X (\/) ( the carrier of S --> {0})) = MSAlgebra(# (FreeSort (X (\/) ( the carrier of S --> {0}))),(FreeOper (X (\/) ( the carrier of S --> {0}))) #) & dom (FreeSort (X (\/) ( the carrier of S --> {0}))) = the carrier of S ) by MSAFREE:def 14, PARTFUN1:def 2;
(Reverse (X (\/) ( the carrier of S --> {0}))) "" X c= S -Terms (X,(X (\/) ( the carrier of S --> {0}))) by Th22;
then A2: (Reverse (X (\/) ( the carrier of S --> {0}))) "" 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 --> {0})))) . s
ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st
( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;
then Free (S,X) is MSSubAlgebra of B by A2, MSUALG_2:def 17;
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 --> {0}))) by PBOOLE:def 18;
hence the Sorts of (Free (S,X)) . s c= (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: according to XBOOLE_0:def 10 :: thesis: (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . 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 --> {0})))) . s or x in the Sorts of (Free (S,X)) . s )
assume A3: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: x in the Sorts of (Free (S,X)) . s
S -Terms (X,(X (\/) ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by PBOOLE:def 18;
then (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s ;
then x in Union (FreeSort (X (\/) ( the carrier of S --> {0}))) by A3, A1, CARD_5:2;
then x is Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:13;
hence x in the Sorts of (Free (S,X)) . s by A3, Th23; :: thesis: verum