let il be Element of NAT ; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
dl in SCM+FSA-Data*-Loc by Def5;
then B: dl in INT \ NAT ;
NAT misses INT \ NAT by XBOOLE_1:79;
hence il <> dl by B, XBOOLE_0:3; :: thesis: verum