theorem Th58: :: FUNCT_7:59

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