let C be initialized standardized ConstructorSignature; :: thesis: for e being expression of C st (e . {} ) `1 = * holds
ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [* ,3] -tree a,q
let e be expression of C; :: thesis: ( (e . {} ) `1 = * implies ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [* ,3] -tree a,q )
assume A1: (e . {} ) `1 = * ; :: thesis: ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [* ,3] -tree a,q

now

given x being Element of Vars such that A3: ( e = x -term C & e . {} = [x,a_Term ] ) ; :: thesis: contradiction
thus contradiction by A1, A3, MCART_1:7; :: thesis: verum

end;

then consider o being OperSymbol of C such that
A4: e . {} = [o,the carrier of C] and
( o in Constructors or o = * or o = non_op ) by Th49;
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:9;
consider aa being ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) such that
A5: t = [o,the carrier of C] -tree aa by A4, MSATERM:10;
A6: * = [o,the carrier of C] `1 by A1, A5, TREES_4:def 4
.= o by MCART_1:7 ;
A7: the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by ABCMIZ_1:38;
A8: len aa = len (the_arity_of o) by MSATERM:22
.= 2 by A6, A7, FINSEQ_1:61 ;
then dom aa = Seg 2 by FINSEQ_1:def 3;
then A9: ( 1 in dom aa & 2 in dom aa ) ;
then reconsider t1 = aa . 1, t2 = aa . 2 as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSATERM:22;
B4: len (doms aa) = len aa by TREES_3:40;
( (doms aa) . 1 = dom t1 & (doms aa) . 2 = dom t2 ) by A9, FUNCT_6:31;
then B5: ( 0 < 2 & 0 + 1 = 1 & 1 < 2 & 1 + 1 = 2 & {} in (doms aa) . 1 & {} in (doms aa) . 2 & <*0 *> ^ (<*> NAT ) = <*0 *> & <*1*> ^ (<*> NAT ) = <*1*> ) by FINSEQ_1:47, TREES_1:47;
dom t = tree (doms aa) by A5, TREES_4:10;
then reconsider 00 = <*0 *>, 01 = <*1*> as Element of dom t by A8, B4, B5, TREES_3:def 15;
( 0 < 2 & 1 = 0 + 1 & 1 < 2 & 2 = 1 + 1 & aa is DTree-yielding ) ;
then ( t1 = t | 00 & t2 = t | 01 ) by A5, A8, TREES_4:def 4;
then B1: ( t1 is expression of C & t2 is expression of C & variables_in t1 c= variables_in t & variables_in t2 c= variables_in t ) by MSAFREE3:33, MSAFREE3:34;
then B3: ( variables_in t1 c= MSVars C & variables_in t2 c= MSVars C ) by MSAFREE3:28;
the_sort_of t1 = (the_arity_of o) . 1 by A9, MSATERM:23
.= an_Adj C by A6, A7, FINSEQ_1:61 ;
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 B3;
then t1 in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by MSAFREE3:def 6;
then t1 in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by MSAFREE3:25;
then reconsider a = t1 as expression of C, an_Adj C by B1, ABCMIZ_1:def 28;
the_sort_of t2 = (the_arity_of o) . 2 by A9, MSATERM:23
.= a_Type C by A6, A7, FINSEQ_1:61 ;
then t2 in { s where s is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of s = a_Type C & variables_in s c= MSVars C ) } by B3;
then t2 in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Type C) by MSAFREE3:def 6;
then t2 in the Sorts of (Free C,(MSVars C)) . (a_Type C) by MSAFREE3:25;
then reconsider q = t2 as expression of C, a_Type C by B1, ABCMIZ_1:def 28;
take a ; :: thesis: ex q being expression of C, a_Type C st e = [* ,3] -tree a,q
take q ; :: thesis: e = [* ,3] -tree a,q
B2: the carrier of C = 3 by ABCMIZ_1:def 9, YELLOW11:1;
aa = <*a,q*> by A8, FINSEQ_1:61;
hence e = [* ,3] -tree a,q by A5, A6, B2, TREES_4:def 6; :: thesis: verum