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 1;
the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by A1, MSUALG_2:def 9;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) by PBOOLE:def 18;
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) ;

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

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 Th8, ABCMIZ_1:48, XBOOLE_0:3; :: thesis:

end;

suppose that A3: (t . {}) `2 = the carrier of C and
A4: (t . {}) `1 in Constructors and
A5: (t . {}) `1 in the carrier' of C ; :: thesis:

reconsider o = (t . {}) `1 as OperSymbol of C by A5;
reconsider tt = t as Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def 2;
then o is constructor ;
then A6: o `1 = the_result_sort_of o by Def1;
A7: t . {} = [o,((t . {}) `2)] ;
then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17;

hereby :: thesis:

assume t is pure expression of C, a_Type C ; :: thesis:
then A9: t in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by ABCMIZ_1:def 28;
thus (t . {}) `1 in Constructors by A4; :: thesis:
assume ((t . {}) `1) `1 <> a_Type ; :: thesis:
hence contradiction by A2, A9, A6, A8, MSAFREE3:7; :: 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 A3, A7, Th12, A6;
t is pure

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

end;

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

end;

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

then (t . {}) `1 in {*,non_op} by TARSKI:def 2;
then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
A13: t = [*,3] -tree (a,q) by A11, Th18;
t = [*,3] -tree <*a,q*> by A13, 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 A12, ABCMIZ_1:def 41; :: thesis:

end;

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

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

end;

end;