set T = m term ;
the_arity_of m = 0 by Ndef;
then len (the_arity_of m) = 0 ;
then A0: 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 A0, Th43a;
T is pure

proof

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

end;

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