the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK by Lm1;
then reconsider S = s as SCM-State of R by CARD_3:107;
a is Element of Data-Locations by Th1;
then reconsider a = a as Element of SCM-Data-Loc by AMI_3:27;
S . a in the carrier of R ;
hence s . a is Element of R ; :: thesis: verum