now

assume NAT in FinSeq-Locations ; :: thesis: contradiction
then A1: NAT in (NAT \/ [:{0},NAT:]) \ {[0,0]} by NUMBERS:def 4;
not NAT in NAT ;
then NAT in [:{0},NAT:] by A1, 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 A2: FinSeq-Locations \ ({NAT} \/ NAT) = FinSeq-Locations by XBOOLE_1:83;
SCM-Data-Loc misses {NAT} by AMI_2:27, ZFMISC_1:56;
then A3: SCM-Data-Loc misses {NAT} \/ NAT by AMI_2:29, XBOOLE_1:70;
A4: 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 A3, 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 A2, A4, XBOOLE_1:42 ; :: thesis: verum