let il be Int-Location; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
Values dl = INT * by Th12;
hence il <> dl by Th11, FUNCT_7:16; :: thesis: verum