let C be initialized ConstructorSignature; :: thesis:
let t be expression of C; :: thesis:
set X = MSVars C;
set V = (MSVars C) \/ (the carrier of C --> {0 });

per cases by LemExp;

suppose ex s being SortSymbol of C ex v being set st
( t = root-tree [v,s] & v in (MSVars C) . s ) ; :: thesis:

then consider s being SortSymbol of C, v being set such that
01: ( t = root-tree [v,s] & v in (MSVars C) . s ) ;
{} in dom t by TREES_1:47;
then ( t . {} in rng t & the carrier of C = {a_Type ,an_Adj ,a_Term } ) by CONSTRSIGN, FUNCT_1:12;
then 02: ( v in (MSVars C) . s & ( s = a_Term or s = an_Adj or s = a_Type ) ) by 01, ENUMSET1:def 1;
then reconsider v = v as variable by MSVARS;
t = v -term C by 01, 02, MSVARS;
hence ( ex x being variable st t = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & t = c -trm p ) or ex a being expression of C, an_Adj C st t = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st t = (ast C) term a,t ) ; :: thesis:

end;

suppose ex o being OperSymbol of C ex p being FinSequence of (Free C,(MSVars C)) st
( t = [o,the carrier of C] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) ) ; :: thesis:

then consider o being OperSymbol of C, p being FinSequence of (Free C,(MSVars C)) such that
03: ( t = [o,the carrier of C] -tree p & len p = len (the_arity_of o) ) and
04: ( p is DTree-yielding & p is ArgumentSeq of Sym o,((MSVars C) \/ (the carrier of C --> {0 })) ) ;

per cases by CNSTR2;

suppose o = * ; :: thesis:

then 05: ( the_arity_of o = <*an_Adj ,a_Type *> & o = ast C & the_result_sort_of o = a_Type ) by CONSTRSIGN;
then 06: ( dom p = dom (the_arity_of o) & dom (the_arity_of o) = Seg 2 & len (the_arity_of o) = 2 ) by 04, FINSEQ_1:61, FINSEQ_3:29, MSATERM:22;
07: ( 1 in Seg 2 & 2 in Seg 2 ) ;
then ( p . 1 in rng p & p . 2 in rng p ) by 06, FUNCT_1:12;
then reconsider p1 = p . 1, p2 = p . 2 as expression of C ;
reconsider t1 = p1, t2 = p2 as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
08: ( C variables_in p1 c= MSVars C & variables_in t1 = C variables_in t1 & C variables_in p2 c= MSVars C & variables_in t2 = C variables_in t2 ) by MSAFREE3:28;
09: ( <*an_Adj ,a_Type *> . 2 = a_Type C & <*an_Adj ,a_Type *> . 1 = an_Adj C ) by FINSEQ_1:61;
the_sort_of t1 = (the_arity_of o) . 1 by 04, 06, 07, MSATERM:23;
then t1 in { q where q is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of q = an_Adj C & variables_in q c= MSVars C ) } by 05, 08, 09;
then p1 in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by MSAFREE3:def 6;
then p1 in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by MSAFREE3:25;
then reconsider a = p1 as expression of C, an_Adj C by ELEMENT;
the_sort_of t2 = (the_arity_of o) . 2 by 04, 06, 07, MSATERM:23;
then t2 in { q where q is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of q = a_Type C & variables_in q c= MSVars C ) } by 05, 08, 09;
then p2 in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Type C) by MSAFREE3:def 6;
then p2 in the Sorts of (Free C,(MSVars C)) . (a_Type C) by MSAFREE3:25;
then reconsider q = p2 as expression of C, a_Type C by ELEMENT;
p = <*a,q*> by 03, 06, FINSEQ_1:61;
then t = (ast C) term a,q by 03, 05, 06, 09, TERM2;
hence ( ex x being variable st t = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & t = c -trm p ) or ex a being expression of C, an_Adj C st t = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st t = (ast C) term a,t ) ; :: thesis:

end;

suppose o = non_op ; :: thesis:

then 05: ( the_arity_of o = <*an_Adj *> & o = non_op C & the_result_sort_of o = an_Adj ) by CONSTRSIGN;
then 06: ( dom p = dom (the_arity_of o) & dom (the_arity_of o) = Seg 1 & len (the_arity_of o) = 1 ) by 04, FINSEQ_1:55, FINSEQ_1:56, MSATERM:22;
07: 1 in Seg 1 ;
then p . 1 in rng p by 06, FUNCT_1:12;
then reconsider p1 = p . 1 as expression of C ;
reconsider t1 = p1 as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
08: ( C variables_in p1 c= MSVars C & variables_in t1 = C variables_in t1 ) by MSAFREE3:28;
09: <*an_Adj *> . 1 = an_Adj C by FINSEQ_1:57;
the_sort_of t1 = (the_arity_of o) . 1 by 04, 06, 07, MSATERM:23;
then t1 in { q where q is Term of C,((MSVars C) \/ (the carrier of C --> {0 })) : ( the_sort_of q = an_Adj C & variables_in q c= MSVars C ) } by 05, 08, 09;
then p1 in (C -Terms (MSVars C),((MSVars C) \/ (the carrier of C --> {0 }))) . (an_Adj C) by MSAFREE3:def 6;
then p1 in the Sorts of (Free C,(MSVars C)) . (an_Adj C) by MSAFREE3:25;
then reconsider a = p1 as expression of C, an_Adj C by ELEMENT;
p = <*a*> by 03, 06, FINSEQ_1:57;
then t = (non_op C) term a by 03, 05, 06, 09, TERM1;
hence ( ex x being variable st t = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & t = c -trm p ) or ex a being expression of C, an_Adj C st t = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st t = (ast C) term a,t ) ; :: thesis:

end;

suppose o is constructor ; :: thesis:

then reconsider o = o as constructor OperSymbol of C ;
t = [o,the carrier of C] -tree p by 03;
then p in (QuasiTerms C) * by Th83;
then reconsider p = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
t = o -trm p by 03, TERM;
hence ( ex x being variable st t = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & t = c -trm p ) or ex a being expression of C, an_Adj C st t = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st t = (ast C) term a,t ) by 03; :: thesis:

end;