set T = m term ;
the_arity_of m = 0 by Def13;
then len (the_arity_of m) = 0 ;
then A1: m term = [m, the carrier of C] -tree {} by ABCMIZ_1:def 29;
ex m, a being OperSymbol of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def 12;
then the_result_sort_of m = a_Type C by ABCMIZ_1:def 32;
then reconsider T = m term as expression of C, a_Type C by A1, Th39;
T is pure

proof

given a being expression of C, an_Adj C, t being expression of C, a_Type C such that A2: T = (ast C) term (a,t) ; :: according to ABCMIZ_1:def 41 :: thesis: contradiction
T = [*, the carrier of C] -tree <*a,t*> by A2, ABCMIZ_1:46;
hence contradiction by A1, TREES_4:15; :: thesis: verum

end;

hence m term is pure expression of C, a_Type C ; :: thesis: verum