theorem Th24: :: FINSEQ_4:24

for p being FinSequence
for x being object
for k being Nat st k in dom p & k < x .. p holds
p . k <> x