let i be Element of SCM-Memory ; :: thesis: ( i in SCM-Data-Loc implies (SCM-VAL * SCM-OK) . i = INT )
i in SCM-Memory ;
then i in dom SCM-OK by PARTFUN1:def 2;
then A1: (SCM-VAL * SCM-OK) . i = SCM-VAL . (SCM-OK . i) by FUNCT_1:13;
assume i in SCM-Data-Loc ; :: thesis: (SCM-VAL * SCM-OK) . i = INT
then (SCM-VAL * SCM-OK) . i = SCM-VAL . 1 by A1, Def2;
hence (SCM-VAL * SCM-OK) . i = INT ; :: thesis: verum