theorem :: FINSEQ_1:12

for z being object
for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )