let X be set ; :: thesis: for r being Real
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let r be Real; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds
(r (#) f) | X is continuous
let f be PartFunc of REAL, the carrier of S; :: thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is continuous ; :: thesis: (r (#) f) | X is continuous
A3: X c= dom (r (#) f) by A1, VFUNCT_1:def 4;

now :: thesis: for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds
( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )

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 that
A4: ( rng s1 c= X & s1 is convergent ) and
A5: lim s1 in X ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )
A6: f /* s1 is convergent by A1, A2, A4, A5, Th16;
then A7: r * (f /* s1) is convergent by NORMSP_1:22;
A8: lim s1 in REAL by XREAL_0:def 1;
f /. (lim s1) = lim (f /* s1) by A1, A2, A4, A5, Th16;
then (r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A3, A5, VFUNCT_1:def 4, A8
.= lim (r * (f /* s1)) by A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A1, A4, Th4, XBOOLE_1:1 ;
hence ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A1, A4, A7, Th4, XBOOLE_1:1; :: thesis: verum

end;

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