let S be non void Signature; :: thesis: for X being V8() ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X
let X be V8() ManySortedSet of the carrier of S; :: thesis: Free (S,X) = FreeMSA X
set Y = X (\/) ( the carrier of S --> );
A1: the Sorts of (Free (S,X)) = S -Terms (X,(X (\/) ( the carrier of S --> ))) by Th24;
A2: FreeMSA X = MSAlgebra(# (),() #) by MSAFREE:def 14;
A3: the Sorts of (Free (S,X)) = the Sorts of ()
proof
let s be Element of S; :: according to PBOOLE:def 21 :: thesis: the Sorts of (Free (S,X)) . s = the Sorts of () . s
reconsider s9 = s as SortSymbol of S ;
thus the Sorts of (Free (S,X)) . s c= the Sorts of () . s :: according to XBOOLE_0:def 10 :: thesis: the Sorts of () . s c= the Sorts of (Free (S,X)) . s
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of () . s )
assume A4: x in the Sorts of (Free (S,X)) . s ; :: thesis: x in the Sorts of () . s
then reconsider t = x as Term of S,(X (\/) ( the carrier of S --> )) by ;
variables_in t c= X by A1, A4, Th17;
then reconsider t9 = t as Term of S,X by Th30;
the_sort_of t = s by A1, A4, Th17;
then the_sort_of t9 = s by Th29;
then x in FreeSort (X,s9) by MSATERM:def 5;
hence x in the Sorts of () . s by ; :: thesis: verum
end;
reconsider s9 = s as SortSymbol of S ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of () . s or x in the Sorts of (Free (S,X)) . s )
assume x in the Sorts of () . s ; :: thesis: x in the Sorts of (Free (S,X)) . s
then A5: x in FreeSort (X,s9) by ;
FreeSort (X,s9) c= S -Terms X by MSATERM:12;
then reconsider t = x as Term of S,X by A5;
X c= X (\/) ( the carrier of S --> ) by PBOOLE:14;
then reconsider t9 = t as Term of S,(X (\/) ( the carrier of S --> )) by MSATERM:26;
variables_in t = S variables_in t ;
then A6: variables_in t9 c= X by Th28;
the_sort_of t = s by ;
then the_sort_of t9 = s by Th29;
then t in { q where q is Term of S,(X (\/) ( the carrier of S --> )) : ( the_sort_of q = s9 & variables_in q c= X ) } by A6;
hence x in the Sorts of (Free (S,X)) . s by ; :: thesis: verum
end;
( FreeMSA X is MSSubAlgebra of FreeMSA X & 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 ;
hence Free (S,X) = FreeMSA X by ; :: thesis: verum