let b be Element of SCM+FSA-Data-Loc ; :: thesis: 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;
thus SCM+FSA-OK . b = ((SCM+FSA-Memory --> (INT *)) +* SCM-OK) . b
.= SCM-OK . b by A1, FUNCT_4:13
.= INT by AMI_2:8 ; :: thesis: verum