let i be Element of SCM+FSA-Memory ; :: thesis: ( SCM+FSA-OK . i = SCM+FSA-Instr implies i in NAT )
assume A1: SCM+FSA-OK . i = SCM+FSA-Instr ; :: thesis: i in NAT

now

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

end;

hence i in NAT ; :: thesis: verum