let f be Element of SCM+FSA-Data*-Loc ; :: thesis: SCM+FSA-OK . f = 2
not f in SCM-Memory by Lm1, XBOOLE_0:3;
then A1: not f in dom SCM-OK by FUNCT_2:def 1;
thus SCM+FSA-OK . f = ((SCM+FSA-Memory --> 2) +* SCM-OK) . f
.= (SCM+FSA-Memory --> 2) . f by A1, FUNCT_4:11
.= 2 ; :: thesis: verum