let dl be FinSeq-Location ; :: thesis: dl <> IC SCM+FSA
( ObjectKind dl = INT * & ObjectKind (IC SCM+FSA ) = NAT ) by Th27, AMI_1:def 11;
hence dl <> IC SCM+FSA by SCMFSA_1:13; :: thesis: verum