let a be Real_Sequence; :: thesis: 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 )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( rng a c= dom (f2 * f1) implies ( rng a c= dom f1 & rng (f1 /* a) c= dom f2 ) )
assume A1: rng a c= dom (f2 * f1) ; :: thesis: ( rng a c= dom f1 & rng (f1 /* a) c= dom f2 )
then A2: f1 .: (rng a) c= dom f2 by FUNCT_1:101;
rng a c= dom f1 by A1, FUNCT_1:101;
hence ( rng a c= dom f1 & rng (f1 /* a) c= dom f2 ) by A2, VALUED_0:30; :: thesis: verum