assume SCM+FSA-Data*-Loc meets SCM-Memory ; :: thesis: contradiction
then consider x being object such that
A1: x in SCM+FSA-Data*-Loc and
A2: x in SCM-Memory by XBOOLE_0:3;
A3: ( x in {NAT} \/ SCM-Data-Loc or x in NAT ) by A2;
x in (NAT \/ [:{0},NAT:]) \ {[0,0]} by A1, NUMBERS:def 4;
then A4: ( x in NAT or x in [:{0},NAT:] ) by XBOOLE_0:def 3;

per cases ( x in {NAT} or x in SCM-Data-Loc or x in NAT ) by A3, XBOOLE_0:def 3;

suppose A5: x in {NAT} ; :: thesis: contradiction

then ex y, z being object st x = [y,z] by A4, RELAT_1:def 1, TARSKI:def 1;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

suppose x in SCM-Data-Loc ; :: thesis: contradiction

then A6: ex k being Nat st x = [1,k] by AMI_2:23;
then consider y, z being object such that
A7: y in {0} and
z in NAT and
A8: x = [y,z] by A4, ZFMISC_1:84;
y = 0 by A7, TARSKI:def 1;
hence contradiction by A6, A8, XTUPLE_0:1; :: thesis: verum

end;

suppose x in NAT ; :: thesis: contradiction

hence contradiction by A1, XBOOLE_0:def 5; :: thesis: verum

end;

end;