the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;
hence the_Values_of (SCM R) is non-empty ; :: according to MEMSTR_0:def 3 :: thesis: verum