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