now

assume NAT in FinSeq-Locations ; :: thesis: contradiction
then Y: NAT in (NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]} by NUMBERS:def 4;
not NAT in NAT ;
then NAT in [:{0 },NAT :] by Y, XBOOLE_0:def 3;
then ex x, y being set st NAT = [x,y] by RELAT_1:def 1;
hence contradiction ; :: thesis: verum

end;

then FinSeq-Locations misses {NAT } by ZFMISC_1:56;
then FinSeq-Locations misses {NAT } \/ NAT by Th14, XBOOLE_1:70;
then E: FinSeq-Locations \ ({NAT } \/ NAT ) = FinSeq-Locations by XBOOLE_1:83;
SCM-Data-Loc misses {NAT } by AMI_2:27, ZFMISC_1:56;
then D: SCM-Data-Loc misses {NAT } \/ NAT by AMI_2:29, XBOOLE_1:70;
X: SCM-Memory \ ({NAT } \/ NAT ) = (SCM-Data-Loc \/ ({NAT } \/ NAT )) \ ({NAT } \/ NAT ) by XBOOLE_1:4
.= SCM-Data-Loc \ ({NAT } \/ NAT ) by XBOOLE_1:40
.= SCM-Data-Loc by D, XBOOLE_1:83
.= Int-Locations ;
thus Data-Locations SCM+FSA = SCM+FSA-Memory \ ({NAT } \/ NAT ) by FUNCT_7:def 1, SCMFSA_1:5
.= (SCM-Memory \/ FinSeq-Locations ) \ ({NAT } \/ NAT )
.= Int-Locations \/ FinSeq-Locations by X, E, XBOOLE_1:42 ; :: thesis: verum