for T being non empty 1-sorted
for S being sequence of T
for NS being increasing sequence of NAT holds S * NS is sequence of T ;