let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C st (e . {}) `1 = non_op holds
ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
let e be expression of C; :: thesis: ( (e . {}) `1 = non_op implies ex a being expression of C, an_Adj C st e = [non_op,3] -tree a )
assume A1: (e . {}) `1 = non_op ; :: thesis: ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
for x being Element of Vars holds
( not e = x -term C or not e . {} = [x,a_Term] ) by A1;
then consider o being OperSymbol of C such that
A2: e . {} = [o, the carrier of C] and
( o in Constructors or o = * or o = non_op ) by Th11;
set Y = (MSVars C) (\/) ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
consider aa being ArgumentSeq of Sym (o,((MSVars C) (\/) ( the carrier of C --> {0}))) such that
A3: t = [o, the carrier of C] -tree aa by A2, MSATERM:10;
A4: non_op = [o, the carrier of C] `1 by A1, A3, TREES_4:def 4
.= o ;
A5: the_arity_of (non_op C) = <*(an_Adj C)*> by ABCMIZ_1:38;
A6: len aa = len (the_arity_of o) by MSATERM:22
.= 1 by A4, A5, FINSEQ_1:40 ;
then dom aa = Seg 1 by FINSEQ_1:def 3;
then A7: 1 in dom aa ;
then reconsider t1 = aa . 1 as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSATERM:22;
A8: len (doms aa) = len aa by TREES_3:38;
(doms aa) . 1 = dom t1 by A7, FUNCT_6:22;
then A9: ( 0 < 1 & 0 + 1 = 1 & {} in (doms aa) . 1 & <*0*> ^ (<*> NAT) = <*0*> ) by FINSEQ_1:34, TREES_1:22;
dom t = tree (doms aa) by A3, TREES_4:10;
then reconsider 00 = <*0*> as Element of dom t by A6, A8, A9, TREES_3:def 15;
t1 = t | 00 by A3, A6, A9, TREES_4:def 4;
then A10: ( t1 is expression of C & variables_in t1 c= variables_in t ) by MSAFREE3:32, MSAFREE3:33;
then A11: variables_in t1 c= MSVars C by MSAFREE3:27;
the_sort_of t1 = (the_arity_of o) . 1 by A7, MSATERM:23
.= an_Adj C by A4, A5 ;
then t1 in { s where s is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) } by A11;
then t1 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def 5;
then t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24;
then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def 28;
take a ; :: thesis: e = [non_op,3] -tree a
A12: the carrier of C = 3 by ABCMIZ_1:def 9, YELLOW11:1;
aa = <*a*> by A6, FINSEQ_1:40;
hence e = [non_op,3] -tree a by A3, A4, A12, TREES_4:def 5; :: thesis: verum