theorem Th24: :: FINSEQ_3:24

for p being FinSequence
for x being object st x in dom p holds
x <> 0