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;