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

proof

let x be set ; :: 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 A2, A3, Th84;
then consider Y being set such that
A4: ( x in Y & 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 A4;
hence x in {} ; :: thesis: verum

end;

then variables_in mm = {} ;
hence mm is ground by ThG; :: 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, ThP;
hence mm is pure ; :: thesis: verum