let b be Element of SCM+FSA-Data-Loc ; :: thesis: (SCM*-VAL * SCM+FSA-OK) . b = INT
b in SCM-Data-Loc ;
then b in SCM-Memory ;
then A1: b in dom SCM-OK by FUNCT_2:def 1;
A2: SCM+FSA-OK . b = 1 by Lm5;
A3: b in dom SCM+FSA-OK by A1, Lm2;
thus (SCM*-VAL * SCM+FSA-OK) . b = SCM*-VAL . (SCM+FSA-OK . b) by A3, FUNCT_1:13
.= SCM*-VAL . 1 by A2
.= INT ; :: thesis: verum