theorem :: SCMFSA_2:7

for k1, k2 being Nat st k1 <> k2 holds
fsloc k1 <> fsloc k2 ;