let S be non void Signature; for X being non-empty ManySortedSet of the carrier of S holds Free (S,X) = FreeMSA X
let X be non-empty ManySortedSet of the carrier of S; 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 Th24;
A2:
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #)
by MSAFREE:def 14;
A3:
the Sorts of (Free (S,X)) = the Sorts of (FreeMSA X)
proof
let s be
Element of
S;
PBOOLE:def 21 the Sorts of (Free (S,X)) . s = the Sorts of (FreeMSA X) . s
reconsider s9 =
s as
SortSymbol of
S ;
thus
the
Sorts of
(Free (S,X)) . s c= the
Sorts of
(FreeMSA X) . s
XBOOLE_0:def 10 the Sorts of (FreeMSA X) . s c= the Sorts of (Free (S,X)) . sproof
let x be
object ;
TARSKI:def 3 ( not x in the Sorts of (Free (S,X)) . s or x in the Sorts of (FreeMSA X) . s )
assume A4:
x in the
Sorts of
(Free (S,X)) . s
;
x in the Sorts of (FreeMSA X) . s
then reconsider t =
x as
Term of
S,
(X (\/) ( the carrier of S --> {0})) by A1, Th16;
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
(FreeMSA X) . s
by A2, MSAFREE:def 11;
verum
end;
reconsider s9 =
s as
SortSymbol of
S ;
let x be
object ;
TARSKI:def 3 ( 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
;
x in the Sorts of (Free (S,X)) . s
then A5:
x in FreeSort (
X,
s9)
by A2, MSAFREE:def 11;
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 --> {0})
by PBOOLE:14;
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 A6:
variables_in t9 c= X
by Th28;
the_sort_of t = s
by A5, MSATERM:def 5;
then
the_sort_of t9 = s
by Th29;
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 A6;
hence
x in the
Sorts of
(Free (S,X)) . s
by A1, Def5;
verum
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 Def1, MSUALG_2:5;
hence
Free (S,X) = FreeMSA X
by A3, Th26; verum