theorem :: AFINSQ_1:7

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