let r be real number ; :: thesis: for X being set
for f being PartFunc of REAL ,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let X be set ; :: thesis: for f being PartFunc of REAL ,REAL st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL ,REAL ; :: thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume Z: X c= dom f ; :: thesis: ( not f | X is continuous or (r (#) f) | X is continuous )
assume A1: f | X is continuous ; :: thesis: (r (#) f) | X is continuous
A3: X c= dom (r (#) f) by Z, VALUED_1:def 5;

now

let s1 be Real_Sequence; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) )
assume A4: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) )
then A5: ( f /* s1 is convergent & f . (lim s1) = lim (f /* s1) ) by A1, Th14, Z;
then A6: r (#) (f /* s1) is convergent by SEQ_2:21;
(r (#) f) . (lim s1) = r * (lim (f /* s1)) by A3, A4, A5, VALUED_1:def 5
.= lim (r (#) (f /* s1)) by A5, SEQ_2:22
.= lim ((r (#) f) /* s1) by Z, A4, RFUNCT_2:24, XBOOLE_1:1 ;
hence ( (r (#) f) /* s1 is convergent & (r (#) f) . (lim s1) = lim ((r (#) f) /* s1) ) by Z, A4, A6, RFUNCT_2:24, XBOOLE_1:1; :: thesis: verum

end;

hence (r (#) f) | X is continuous by A3, Th14; :: thesis: verum