let C be initialized standardized ConstructorSignature; :: thesis: 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; :: thesis: ( 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] ; :: thesis: ( 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; :: thesis: verum

end;

suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; :: thesis: ( 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 o, s being object such that
A9: ( o in the carrier' of C & s in { the carrier of C} & q . {} = [o,s] ) by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of C by A9;
( o is constructor iff ( o <> * & o <> non_op ) ) ;
then ( s = the carrier of C & ( o in Constructors or o = * or o = non_op ) ) by A9, Def1, TARSKI:def 1;
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 A9; :: thesis: verum

end;

end;