for T being non empty 1-sorted
for S being SetSequence of the carrier of T
for R being subsequence of S
for n being Nat ex m being Element of NAT st
( m >= n & R . n = S . m )