let C be initialized standardized ConstructorSignature; for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
let e be expression of C; ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
set X = MSVars C;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
reconsider q = e as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
per cases
( ex s being SortSymbol of C ex v being Element of ((MSVars C) (\/) ( the carrier of C --> {0})) . s st q . {} = [v,s] or q . {} in [: the carrier' of C,{ the carrier of C}:] )
by MSATERM:2;
suppose
ex
s being
SortSymbol of
C ex
v being
Element of
((MSVars C) (\/) ( the carrier of C --> {0})) . s st
q . {} = [v,s]
;
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )then consider s being
SortSymbol of
C,
v being
Element of
((MSVars C) (\/) ( the carrier of C --> {0})) . s such that A1:
q . {} = [v,s]
;
consider z being
object such that A2:
(
z in dom the
Sorts of
(Free (C,(MSVars C))) &
e in the
Sorts of
(Free (C,(MSVars C))) . z )
by CARD_5:2;
reconsider z =
z as
SortSymbol of
C by A2;
the
carrier of
C = {a_Type,an_Adj,a_Term}
by ABCMIZ_1:def 9;
then A3:
(
z = a_Type or
z = an_Adj or
z = a_Term )
by ENUMSET1:def 1;
A4:
q = root-tree [v,s]
by A1, MSATERM:5;
then A5:
the_sort_of q = s
by MSATERM:14;
A6:
the
Sorts of
(Free (C,(MSVars C))) = C -Terms (
(MSVars C),
((MSVars C) (\/) ( the carrier of C --> {0})))
by MSAFREE3:24;
then
the
Sorts of
(Free (C,(MSVars C))) c= the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by PBOOLE:def 18;
then
( the
Sorts of
(Free (C,(MSVars C))) . z c= the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . z &
FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})) = MSAlgebra(#
(FreeSort ((MSVars C) (\/) ( the carrier of C --> {0}))),
(FreeOper ((MSVars C) (\/) ( the carrier of C --> {0}))) #) )
;
then
(
q in the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . z & the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . z = FreeSort (
((MSVars C) (\/) ( the carrier of C --> {0})),
z) )
by A2, MSAFREE:def 11;
then A7:
s = z
by A5, MSATERM:def 5;
then
v in (MSVars C) . z
by A4, A2, A6, MSAFREE3:18;
then A8:
(
v in Vars &
z = a_Term )
by A3, ABCMIZ_1:def 25;
then reconsider x =
v as
Element of
Vars ;
e = x -term C
by A1, A7, A8, MSATERM:5;
hence
( ex
x being
Element of
Vars st
(
e = x -term C &
e . {} = [x,a_Term] ) or ex
o being
OperSymbol of
C st
(
e . {} = [o, the carrier of C] & (
o in Constructors or
o = * or
o = non_op ) ) )
by A1, A7, A8;
verum end;