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 Th7;
hence il <> dl by Th6, FUNCT_7:16; :: thesis: verum