let il be Int-Location ; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
( ObjectKind dl = INT * & ObjectKind il = INT ) by Th26, Th27;
hence il <> dl by FUNCT_7:18; :: thesis: verum