let i, j be natural number ; :: thesis: fsloc i <> intloc j
fsloc i in FinSeq-Locations by Def5;
hence fsloc i <> intloc j by SCMFSA_1:30, XBOOLE_0:3; :: thesis: verum