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:9;

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 set such that
A4: ( z in dom the Sorts of (Free (C,(MSVars C))) & e in the Sorts of (Free (C,(MSVars C))) . z ) by CARD_5:10;
reconsider z = z as SortSymbol of C by A4, PARTFUN1:def 4;
the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def 9;
then A5: ( z = a_Type or z = an_Adj or z = a_Term ) by ENUMSET1:def 1;
A3: q = root-tree [v,s] by A1, MSATERM:5;
then A6: the_sort_of q = s by MSATERM:14;
A7: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) by MSAFREE3:25;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def 23;
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}))) #) ) by PBOOLE:def 5;
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 A4, MSAFREE:def 13;
then A8: s = z by A6, MSATERM:def 5;
then v in (MSVars C) . z by A3, A4, A7, MSAFREE3:19;
then A9: ( v in Vars & z = a_Term ) by A5, ABCMIZ_1:def 25;
then reconsider x = v as Element of Vars ;
e = x -term C by A1, MSATERM:5, A8, A9;
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, A8, A9; :: 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 set such that
B1: ( 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 B1;
( o is constructor iff ( o <> * & o <> non_op ) ) by ABCMIZ_1:def 11;
then ( s = the carrier of C & ( o in Constructors or o = * or o = non_op ) ) by B1, TARSKI:def 1, StandardizedDef;
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 B1; :: thesis: verum

end;

end;