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 PBOOLE:def 23, MSAFREE3:25;
then A6: ( 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 PBOOLE:def 5, ABCMIZ_1:def 28;
then t in (FreeSort ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Term C) ;
then A1: t in FreeSort ((MSVars C) \/ (the carrier of C --> {0 })),(a_Term C) by MSAFREE:def 13;
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:9;

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
A2: t . {} = [v,s] ;
A4: ( q = root-tree [v,s] & the_sort_of q = a_Term C ) by A1, A2, MSATERM:5, MSATERM:def 5;
then A5: ( a_Term C = s & (t . {} ) `1 = v ) by A2, MCART_1:7, MSATERM:14;
then reconsider x = v as Element of Vars by A3, A4, A6, MSAFREE3:19;
( q = x -term C & vars x <> 2 ) by A4, A5, Lem1;
hence ( t is compound iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = a_Term ) ) by A5; :: 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 set 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 B2: the_result_sort_of o = the_sort_of q by A7, MSATERM:17
.= a_Term C by A6, MSAFREE3:18 ;
then ( o <> ast C & o <> non_op C ) by ABCMIZ_1:38;
then A9: o is constructor by ABCMIZ_1:def 11;
then B3: a_Term C = o `1 by B2, StandardizedDef
.= ((q . {} ) `1 ) `1 by A7, MCART_1:7 ;
B4: (q . {} ) `1 = o by A7, MCART_1:7;

now

given x being Element of Vars such that A8: q = x -term C ; :: thesis: contradiction
q . {} = [x,a_Term ] by TREES_4:3, A8;
then k = a_Term by A7, ZFMISC_1:33;
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, B3, B4, CompoundDef, StandardizedDef; :: thesis: verum

end;

end;