:: deftheorem def9 defines subsequence DBLSEQ_1:def 14 :
for X being non empty set
for seq, b₃ being Function of [:NAT,NAT:],X holds
( b₃ is subsequence of seq iff ex N, M being increasing sequence of NAT st
for n, m being Nat holds b₃ . (n,m) = seq . ((N . n),(M . m)) );