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;

A2: now

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

end;

A4: not f in dom SCM-OK by A1, FUNCT_2:def 1;
thus SCM+FSA-OK . f = ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) . f by A2, FUNCT_4:12
.= (SCM+FSA-Memory --> (INT * )) . f by A4, FUNCT_4:12
.= INT * by FUNCOP_1:13 ; :: thesis: verum