the Object-Kind of (SCM R) = SCM-OK R by Def1;
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