for X being set
for p being Function-yielding FinSequence st p <> {} holds
rng (compose (p,X)) c= lastrng p