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

now

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

per cases ( NAT in NAT or NAT in [:{0},NAT:] ) by A3, 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 by A1, Th7; :: thesis: verum