theorem Th1: :: LIMFUNC4:1

for f1, f2 being PartFunc of REAL,REAL
for s being Real_Sequence
for X being set st rng s c= (dom (f2 * f1)) /\ X holds
( rng s c= dom (f2 * f1) & rng s c= X & rng s c= dom f1 & rng s c= (dom f1) /\ X & rng (f1 /* s) c= dom f2 )