let S be non void Signature; :: thesis: for X being V5() ManySortedSet of holds Free S,X = FreeMSA X
let X be V5() ManySortedSet of ; :: thesis: Free S,X = FreeMSA X
set Y = X \/ (the carrier of S --> {0 });
A1:
FreeMSA X is MSSubAlgebra of FreeMSA X
by MSUALG_2:6;
consider A being MSSubset of (FreeMSA (X \/ (the carrier of S --> {0 }))) such that
A2:
( Free S,X = GenMSAlg A & A = (Reverse (X \/ (the carrier of S --> {0 }))) "" X )
by Def2;
A3:
the Sorts of (Free S,X) = S -Terms X,(X \/ (the carrier of S --> {0 }))
by Th25;
A4:
FreeMSA X = MSAlgebra(# (FreeSort X),(FreeOper X) #)
by MSAFREE:def 16;
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 A5:
s in the
carrier of
S
;
:: thesis: the Sorts of (Free S,X) . s c= the Sorts of (FreeMSA X) . sthen reconsider s' =
s as
SortSymbol of
S ;
thus
the
Sorts of
(Free S,X) . s c= the
Sorts of
(FreeMSA X) . s
:: thesis: verumproof
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 A6:
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 A3, A5, Th17;
variables_in t c= X
by A3, A5, A6, Th18;
then reconsider t' =
t as
Term of
S,
X by Th31;
the_sort_of t = s
by A3, A5, A6, Th18;
then
the_sort_of t' = s
by Th30;
then
x in FreeSort X,
s'
by MSATERM:def 5;
hence
x in the
Sorts of
(FreeMSA X) . s
by A4, MSAFREE:def 13;
:: thesis: verum
end;
end;
thus
the
Sorts of
(FreeMSA X) c= the
Sorts of
(Free S,X)
:: thesis: verumproof
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 s' =
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 A7:
(
x in FreeSort X,
s' &
FreeSort X,
s' c= S -Terms X )
by A4, MSAFREE:def 13, MSATERM:12;
then reconsider t =
x as
Term of
S,
X ;
A8:
the_sort_of t = s
by A7, MSATERM:def 5;
X c= X \/ (the carrier of S --> {0 })
by PBOOLE:16;
then reconsider t' =
t as
Term of
S,
(X \/ (the carrier of S --> {0 })) by MSATERM:26;
(
variables_in t = S variables_in t &
variables_in t' = S variables_in t )
;
then
(
variables_in t' c= X &
the_sort_of t' = s )
by A8, Th29, Th30;
then
t in { q where q is Term of S,(X \/ (the carrier of S --> {0 })) : ( the_sort_of q = s' & variables_in q c= X ) }
;
hence
x in the
Sorts of
(Free S,X) . s
by A3, Def6;
:: thesis: verum
end;
end;
hence
Free S,X = FreeMSA X
by A1, A2, Th27; :: thesis: verum