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