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