let C be initialized standardized ConstructorSignature; :: thesis:
set X = MSVars C;
set V = (MSVars C) \/ (the carrier of C --> {0 });
let t be expression of C; :: thesis:
consider A being MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) such that
A1: ( Free C,(MSVars C) = GenMSAlg A & A = (Reverse ((MSVars C) \/ (the carrier of C --> {0 }))) "" (MSVars C) ) by MSAFREE3:def 2;
the Sorts of (Free C,(MSVars C)) is MSSubset of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by A1, MSUALG_2:def 10;
then the Sorts of (Free C,(MSVars C)) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) by PBOOLE:def 23;
then A2: the Sorts of (Free C,(MSVars C)) . (a_Type C) c= the Sorts of (FreeMSA ((MSVars C) \/ (the carrier of C --> {0 }))) . (a_Type C) by PBOOLE:def 5;

per cases ) `1 in Vars & (t . {} ) `2 = a_Term & t is quasi-term of C ) or ( (t . {} ) `2 = the carrier of C & (t . {} ) `1 in Constructors & (t . {} ) `1 in the carrier' of C ) or (t . {} ) `1 = * or (t . {} ) `1 = non_op ) by Th50;

suppose ( (t . {} ) `1 in Vars & (t . {} ) `2 = a_Term & t is quasi-term of C ) ; :: thesis:

hence ( t is pure expression of C, a_Type C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = a_Type ) ) by Lem2, XBOOLE_0:3, ABCMIZ_1:48; :: thesis:

end;

suppose that B1: (t . {} ) `2 = the carrier of C and
B2: (t . {} ) `1 in Constructors and
B3: (t . {} ) `1 in the carrier' of C ; :: thesis:

reconsider o = (t . {} ) `1 as OperSymbol of C by B3;
reconsider tt = t as Term of C,((MSVars C) \/ (the carrier of C --> {0 })) by MSAFREE3:9;
not o in {* ,non_op } by B2, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def 2;
then o is constructor by ABCMIZ_1:def 11;
then B4: o `1 = the_result_sort_of o by StandardizedDef;
B7: t . {} = [o,((t . {} ) `2 )] by Lem5;
then B5: the_sort_of tt = the_result_sort_of o by B1, MSATERM:17;

hereby :: thesis:

assume t is pure expression of C, a_Type C ; :: thesis:
then B6: t in the Sorts of (Free C,(MSVars C)) . (a_Type C) by ABCMIZ_1:def 28;
thus (t . {} ) `1 in Constructors by B2; :: thesis:
assume ((t . {} ) `1 ) `1 <> a_Type ; :: thesis:
hence contradiction by A2, B6, B4, B5, MSAFREE3:8; :: thesis:

end;

assume (t . {} ) `1 in Constructors ; :: thesis:
assume ((t . {} ) `1 ) `1 = a_Type ; :: thesis:
then reconsider t = t as expression of C, a_Type C by B1, B7, Th46, B4;
t is pure

given a being expression of C, an_Adj C, q being expression of C, a_Type C such that B9: t = (ast C) term a,q ; :: according to ABCMIZ_1:def 41 :: thesis:
t = [* ,the carrier of C] -tree <*a,q*> by B9, ABCMIZ_1:46;
then t . {} = [* ,the carrier of C] by TREES_4:def 4;
then (t . {} ) `1 = * by MCART_1:7;
then (t . {} ) `1 in {* ,non_op } by TARSKI:def 2;
hence contradiction by B2, XBOOLE_0:3, ABCMIZ_1:39; :: thesis:

end;

hence t is pure expression of C, a_Type C ; :: thesis:

end;

suppose Z0: (t . {} ) `1 = * ; :: thesis:

then (t . {} ) `1 in {* ,non_op } by TARSKI:def 2;
then Z2: not (t . {} ) `1 in Constructors by XBOOLE_0:3, ABCMIZ_1:39;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
Z1: t = [* ,3] -tree a,q by Z0, Th52;
t = [* ,3] -tree <*a,q*> by Z1, TREES_4:def 6
.= [* ,the carrier of C] -tree <*a,q*> by ABCMIZ_1:def 9, YELLOW11:1
.= (ast C) term a,q by ABCMIZ_1:46 ;
hence ( t is pure expression of C, a_Type C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = a_Type ) ) by Z2, ABCMIZ_1:def 41; :: thesis:

end;

suppose Z0: (t . {} ) `1 = non_op ; :: thesis:

then (t . {} ) `1 in {* ,non_op } by TARSKI:def 2;
then Z2: not (t . {} ) `1 in Constructors by XBOOLE_0:3, ABCMIZ_1:39;
consider a being expression of C, an_Adj C such that
Z1: t = [non_op ,3] -tree a by Z0, Th53;
t = [non_op ,3] -tree <*a*> by Z1, TREES_4:def 5;
then t . {} = [non_op ,3] by TREES_4:def 4;
then (t . {} ) `1 = non_op by MCART_1:7;
then t is expression of C, an_Adj C by Th47;
hence ( t is pure expression of C, a_Type C iff ( (t . {} ) `1 in Constructors & ((t . {} ) `1 ) `1 = a_Type ) ) by Z2, ABCMIZ_1:48; :: thesis:

end;

end;