assume IC SCM+FSA in FinSeq-Locations ; :: thesis: contradiction
then IC SCM+FSA is FinSeq-Location by SCMFSA_2:12;
then ObjectKind (IC SCM+FSA ) = INT * by SCMFSA_2:27;
hence contradiction by AMI_1:def 11, SCMFSA_1:13; :: thesis: verum