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
not i in NAT by A1, Th11, Th13;
then A2: i in ({NAT } \/ SCM+FSA-Data-Loc ) \/ SCM+FSA-Data*-Loc by Th8, XBOOLE_0:def 3;
not i in SCM+FSA-Data*-Loc by A1, Th12, FUNCT_7:18;
then A3: i in {NAT } \/ SCM+FSA-Data-Loc by A2, XBOOLE_0:def 3;
not i in {NAT } by A1, Th9, Th13, TARSKI:def 1;
hence i in SCM+FSA-Data-Loc by A3, XBOOLE_0:def 3; :: thesis: verum