theorem Th70: :: ABCMIZ_1:70

for C being initialized ConstructorSignature
for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} holds
ex t being expression of C, a_Type C st
( t = root-tree [m, the carrier of C] & t is pure )