let dl be FinSeq-Location ; :: thesis: dl <> IC SCM+FSA
dl in SCM+FSA-Data*-Loc by Def5;
then A: dl in INT \ NAT ;
B: INT = (NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]} by NUMBERS:def 4;

now

assume NAT in INT \ NAT ; :: thesis: contradiction
then pc: NAT in NAT \/ [:{0 },NAT :] by B, XBOOLE_0:def 5;

per cases ( NAT in NAT or NAT in [:{0 },NAT :] ) by pc, XBOOLE_0:def 3;

suppose NAT in NAT ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose NAT in [:{0 },NAT :] ; :: thesis: contradiction

hence contradiction by FINSET_1:34; :: thesis: verum

end;

end;

end;

hence dl <> IC SCM+FSA by A, Th7; :: thesis: verum