let S be non void Signature; :: thesis: for X being V5() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X
let X be V5() ManySortedSet of the carrier of S; :: thesis: Free (S,X) = FreeMSA X
set Y = X \/ ( the carrier of S --> {0});
A1: the Sorts of (Free (S,X)) = S -Terms (X,(X \/ ( the carrier of S --> {0}))) by Th25;
A2: FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #) by MSAFREE:def 16;
A3: the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X)

proof

hereby :: according to PBOOLE:def 5,PBOOLE:def 13 :: thesis: the Sorts of (FreeMSA X) c= the Sorts of (Free (S,X))

let s be set ; :: thesis: ( s in the carrier of S implies the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s )
assume A4: s in the carrier of S ; :: thesis: the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s
then reconsider s9 = s as SortSymbol of S ;
thus the Sorts of (Free (S,X)) . s c= the Sorts of (FreeMSA X) . s :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of (FreeMSA X) . s )
assume A5: x in the Sorts of (Free (S,X)) . s ; :: thesis: x in the Sorts of (FreeMSA X) . s
then reconsider t = x as Term of S,(X \/ ( the carrier of S --> {0})) by A1, A4, Th17;
variables_in t c= X by A1, A4, A5, Th18;
then reconsider t9 = t as Term of S,X by Th31;
the_sort_of t = s by A1, A4, A5, Th18;
then the_sort_of t9 = s by Th30;
then x in FreeSort (X,s9) by MSATERM:def 5;
hence x in the Sorts of (FreeMSA X) . s by A2, MSAFREE:def 13; :: thesis: verum

end;

end;

thus the Sorts of (FreeMSA X) c= the Sorts of (Free (S,X)) :: thesis: verum

proof

let s be set ; :: according to PBOOLE:def 5 :: thesis: ( not s in the carrier of S or the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s )
assume s in the carrier of S ; :: thesis: the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . s
then reconsider s9 = s as SortSymbol of S ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (FreeMSA X) . s or x in the Sorts of (Free (S,X)) . s )
assume x in the Sorts of (FreeMSA X) . s ; :: thesis: x in the Sorts of (Free (S,X)) . s
then A6: x in FreeSort (X,s9) by A2, MSAFREE:def 13;
FreeSort (X,s9) c= S -Terms X by MSATERM:12;
then reconsider t = x as Term of S,X by A6;
X c= X \/ ( the carrier of S --> {0}) by PBOOLE:16;
then reconsider t9 = t as Term of S,(X \/ ( the carrier of S --> {0})) by MSATERM:26;
variables_in t = S variables_in t ;
then A7: variables_in t9 c= X by Th29;
the_sort_of t = s by A6, MSATERM:def 5;
then the_sort_of t9 = s by Th30;
then t in { q where q is Term of S,(X \/ ( the carrier of S --> {0})) : ( the_sort_of q = s9 & variables_in q c= X ) } by A7;
hence x in the Sorts of (Free (S,X)) . s by A1, Def6; :: thesis: verum

end;

end;

( FreeMSA X is MSSubAlgebra of FreeMSA X & 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 Def2, MSUALG_2:6;
hence Free (S,X) = FreeMSA X by A3, Th27; :: thesis: verum