theorem Th9: :: FDIFF_2:9

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