let G be non empty 1-sorted ; :: thesis: for i being Element of SCM-Memory st i in SCM-Data-Loc holds
((SCM-VAL G) * SCM-OK) . i = the carrier of G
let i be Element of SCM-Memory ; :: thesis: ( i in SCM-Data-Loc implies ((SCM-VAL G) * SCM-OK) . i = the carrier of G )
i in SCM-Memory ;
then i in dom SCM-OK by PARTFUN1:def 2;
then A1: ((SCM-VAL G) * SCM-OK) . i = (SCM-VAL G) . (SCM-OK . i) by FUNCT_1:13;
assume i in SCM-Data-Loc ; :: thesis: ((SCM-VAL G) * SCM-OK) . i = the carrier of G
then ((SCM-VAL G) * SCM-OK) . i = (SCM-VAL G) . 1 by A1, AMI_2:def 4;
hence ((SCM-VAL G) * SCM-OK) . i = the carrier of G ; :: thesis: verum