consider m, a being OperSymbol of C such that
A1: the_result_sort_of m = a_Type and
A2: the_arity_of m = {} and
the_result_sort_of a = an_Adj and
the_arity_of a = {} by Def12;
root-tree [m, the carrier of C] in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by A1, A2, MSAFREE3:5;
then reconsider mm = root-tree [m, the carrier of C] as expression of C, a_Type C by Th41;
take mm ; :: thesis: ( mm is ground & mm is pure )
set p = <*> (Union the Sorts of (Free (C,(MSVars C))));
A3: mm = [m, the carrier of C] -tree (<*> (Union the Sorts of (Free (C,(MSVars C))))) by TREES_4:20;
A4: m <> * by A2, Def9;
m <> non_op by A1, Def9;
then A5: m is constructor by A4;
variables_in mm c= {}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in variables_in mm or x in {} )
assume x in variables_in mm ; :: thesis: x in {}
then x in union { (variables_in t) where t is quasi-term of C : t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) } by A3, A5, Th88;
then consider Y being set such that
x in Y and
A6: Y in { (variables_in t) where t is quasi-term of C : t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) } by TARSKI:def 4;
ex t being quasi-term of C st
( Y = variables_in t & t in rng (<*> (Union the Sorts of (Free (C,(MSVars C))))) ) by A6;
hence x in {} ; :: thesis: verum

end;

then variables_in mm = {} ;
hence mm is ground by Th107; :: thesis: mm is pure
ex t being expression of C, a_Type C st
( t = root-tree [m, the carrier of C] & t is pure ) by A1, A2, Th70;
hence mm is pure ; :: thesis: verum