let i, j be natural number ; :: thesis: fsloc i <> intloc j
( fsloc i in FinSeq-Locations & intloc j in Int-Locations ) by Def4, Def5;
hence fsloc i <> intloc j by SCMFSA_1:33, XBOOLE_0:3; :: thesis: verum