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

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