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 Th7;

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
A1: t = root-tree [v,s] and
A2: v in (MSVars C) . s ;
the carrier of C = {a_Type,an_Adj,a_Term} by Def9;
then A3: ( s = a_Term or s = an_Adj or s = a_Type ) by ENUMSET1:def 1;
then reconsider v = v as variable by A2, Def25;
t = v -term C by A1, A2, A3, Def25;
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
A4: t = [o, the carrier of C] -tree p and
A5: len p = len (the_arity_of o) and
p is DTree-yielding and
A6: p is ArgumentSeq of Sym (o,((MSVars C) (\/) ( the carrier of C --> {0}))) ;

per cases ;

suppose A7: o = * ; :: thesis:

then A8: the_arity_of o = <*an_Adj,a_Type*> by Def9;
A9: dom p = dom (the_arity_of o) by A6, MSATERM:22;
A10: dom (the_arity_of o) = Seg 2 by A8, FINSEQ_1:89;
A11: len (the_arity_of o) = 2 by A8, FINSEQ_1:44;
A12: 1 in Seg 2 ;
A13: 2 in Seg 2 ;
A14: p . 1 in rng p by A9, A10, A12, FUNCT_1:3;
p . 2 in rng p by A9, A10, A13, FUNCT_1:3;
then reconsider p1 = p . 1, p2 = p . 2 as expression of C by A14;
reconsider t1 = p1, t2 = p2 as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
A15: C variables_in p1 c= MSVars C by MSAFREE3:27;
A16: variables_in t1 = C variables_in t1 ;
A17: C variables_in p2 c= MSVars C by MSAFREE3:27;
A18: variables_in t2 = C variables_in t2 ;
A19: <*an_Adj,a_Type*> . 2 = a_Type C ;
A20: <*an_Adj,a_Type*> . 1 = an_Adj C ;
the_sort_of t1 = (the_arity_of o) . 1 by A6, A9, A10, A12, 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 A8, A15, A16;
then p1 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def 5;
then p1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24;
then reconsider a = p1 as expression of C, an_Adj C by Def28;
the_sort_of t2 = (the_arity_of o) . 2 by A6, A9, A10, A13, 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 A8, A17, A18;
then p2 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Type C) by MSAFREE3:def 5;
then p2 in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by MSAFREE3:24;
then reconsider q = p2 as expression of C, a_Type C by Def28;
p = <*a,q*> by A5, A11, FINSEQ_1:44;
then t = (ast C) term (a,q) by A4, A7, A8, A11, A19, A20, Def31;
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 A21: o = non_op ; :: thesis:

then A22: the_arity_of o = <*an_Adj*> by Def9;
A23: dom p = dom (the_arity_of o) by A6, MSATERM:22;
A24: dom (the_arity_of o) = Seg 1 by A22, FINSEQ_1:38;
A25: len (the_arity_of o) = 1 by A22, FINSEQ_1:39;
A26: 1 in Seg 1 ;
then p . 1 in rng p by A23, A24, FUNCT_1:3;
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:8;
A27: C variables_in p1 c= MSVars C by MSAFREE3:27;
A28: variables_in t1 = C variables_in t1 ;
A29: <*an_Adj*> . 1 = an_Adj C ;
the_sort_of t1 = (the_arity_of o) . 1 by A6, A23, A24, A26, 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 A22, A27, A28;
then p1 in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def 5;
then p1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24;
then reconsider a = p1 as expression of C, an_Adj C by Def28;
p = <*a*> by A5, A25, FINSEQ_1:40;
then t = (non_op C) term a by A4, A21, A22, A25, A29, Def30;
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 A4;
then p in (QuasiTerms C) * by Th51;
then reconsider p = p as FinSequence of QuasiTerms C by FINSEQ_1:def 11;
t = o -trm p by A4, A5, Def35;
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 A5; :: thesis:

end;