let i be Element of SCM+FSA-Memory ; :: thesis: ( SCM+FSA-OK . i = INT * implies i in SCM+FSA-Data*-Loc )
assume A1: SCM+FSA-OK . i = INT * ; :: thesis: i in SCM+FSA-Data*-Loc

A2: now

assume A3: i in {NAT} \/ SCM+FSA-Data-Loc ; :: thesis: contradiction
not i in {NAT} by A1, Th9, Th13, TARSKI:def 1;
then i in SCM+FSA-Data-Loc by A3, XBOOLE_0:def 3;
hence contradiction by A1, Th10, FUNCT_7:16; :: thesis: verum

end;

thus i in SCM+FSA-Data*-Loc by A2, XBOOLE_0:def 3; :: thesis: verum