let a be Real_Sequence; :: thesis: for f2, f1 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 f2, f1 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 rng a c= dom (f2 * f1) ; :: thesis: ( rng a c= dom f1 & rng (f1 /* a) c= dom f2 )
then ( rng a c= dom f1 & f1 .: (rng a) c= dom f2 ) by FUNCT_1:171;
hence ( rng a c= dom f1 & rng (f1 /* a) c= dom f2 ) by VALUED_0:30; :: thesis: verum