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;

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;

end;

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;hence contradiction by A5, TARSKI:def 1; :: thesis: verum

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;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