let f be Element of SCM+FSA-Data*-Loc ; :: thesis: SCM+FSA-OK . f = INT *
A1: not f in SCM-Memory by Lm4, XBOOLE_0:3;
then A2: not f in dom SCM-OK by FUNCT_2:def 1;

now

A3: dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT)) c= dom (SCM-OK | NAT) by RELAT_1:44;
assume f in dom ((SCM-Instr .--> SCM+FSA-Instr) * (SCM-OK | NAT)) ; :: thesis: contradiction
then f in dom SCM-OK by A3, RELAT_1:86;
hence contradiction by A1, FUNCT_2:def 1; :: thesis: verum

end;

hence SCM+FSA-OK . f = ((SCM+FSA-Memory --> (INT *)) +* SCM-OK) . f by FUNCT_4:12
.= (SCM+FSA-Memory --> (INT *)) . f by A2, FUNCT_4:12
.= INT * by FUNCOP_1:13 ;
:: thesis: verum