let b be Element of SCM+FSA-Data-Loc ; :: thesis: SCM+FSA-OK . b = 1
A1: b in SCM-Data-Loc ;
then b in SCM-Memory ;
then A2: b in dom SCM-OK by FUNCT_2:def 1;
thus SCM+FSA-OK . b = ((SCM+FSA-Memory --> 2) +* SCM-OK) . b
.= SCM-OK . b by A2, FUNCT_4:13
.= 1 by A1, AMI_2:def 4 ; :: thesis: verum