let C be initialized standardized ConstructorSignature; :: thesis: for t being quasi-term of C holds
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
set X = MSVars C;
set V = (MSVars C) (\/) ( the carrier of C --> {0});
let t be quasi-term of C; :: thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
( C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) & the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))) ) by MSAFREE3:24, PBOOLE:def 18;
then A1: ( 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}))) #) & (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) & t in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C) ) by ABCMIZ_1:def 28;
then t in (FreeSort ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C) ;
then A2: t in FreeSort (((MSVars C) (\/) ( the carrier of C --> {0})),(a_Term C)) by MSAFREE:def 11;
A3: ( (MSVars C) . a_Term = Vars & a_Term C = a_Term & a_Term = 2 ) by ABCMIZ_1:def 25;
reconsider q = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;

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: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )

then consider s being SortSymbol of C, v being Element of ((MSVars C) (\/) ( the carrier of C --> {0})) . s such that
A4: t . {} = [v,s] ;
A5: ( q = root-tree [v,s] & the_sort_of q = a_Term C ) by A2, A4, MSATERM:5, MSATERM:def 5;
then A6: ( a_Term C = s & (t . {}) `1 = v ) by A4, MSATERM:14;
then reconsider x = v as Element of Vars by A3, A5, A1, MSAFREE3:18;
( q = x -term C & vars x <> 2 ) by A5, A6, Th7;
hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A6; :: thesis: verum

end;

suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; :: thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )

then consider o, k being object such that
A7: ( o in the carrier' of C & k in { the carrier of C} & q . {} = [o,k] ) by ZFMISC_1:def 2;
reconsider o = o as OperSymbol of C by A7;
k = the carrier of C by A7, TARSKI:def 1;
then A8: the_result_sort_of o = the_sort_of q by A7, MSATERM:17
.= a_Term C by A1, MSAFREE3:17 ;
then ( o <> ast C & o <> non_op C ) by ABCMIZ_1:38;
then A9: o is constructor ;
then A10: a_Term C = o `1 by A8, Def1
.= ((q . {}) `1) `1 by A7 ;
A11: (q . {}) `1 = o by A7;

now :: thesis: for x being Element of Vars holds not q = x -term C

given x being Element of Vars such that A12: q = x -term C ; :: thesis: contradiction
q . {} = [x,a_Term] by A12, TREES_4:3;
then k = a_Term by A7, XTUPLE_0:1;
then 2 = the carrier of C by A7, TARSKI:def 1;
hence contradiction by ABCMIZ_1:def 9, YELLOW11:1; :: thesis: verum

end;

hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A9, A10, A11, Th3, Def1; :: thesis: verum

end;

end;