for T1 being non empty 1-sorted
for T2 being 1-sorted
for S being sequence of T1 st rng S c= the carrier of T2 holds
S is sequence of T2