theorem :: FINANCE2:9

ex A being SetSequence of NAT st
for n being Nat holds A . n = {n}