let r be Real; :: thesis: for CNS being ComplexNormSpace
for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
r (#) f is_continuous_on X
let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
r (#) f is_continuous_on X
let RNS be RealNormSpace; :: thesis: for X being set
for f being PartFunc of CNS,RNS st f is_continuous_on X holds
r (#) f is_continuous_on X
let X be set ; :: thesis: for f being PartFunc of CNS,RNS st f is_continuous_on X holds
r (#) f is_continuous_on X
let f be PartFunc of CNS,RNS; :: thesis: ( f is_continuous_on X implies r (#) f is_continuous_on X )
assume A1: f is_continuous_on X ; :: thesis: r (#) f is_continuous_on X
then A2: X c= dom f ;
then A3: X c= dom (r (#) f) by VFUNCT_1:def 4;

now :: thesis: for s1 being sequence of CNS 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 sequence of CNS; :: 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 and
A5: s1 is convergent and
A6: lim s1 in X ; :: thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )
A7: f /* s1 is convergent by A1, A4, A5, A6, Th42;
then A8: r * (f /* s1) is convergent by NORMSP_1:22;
f /. (lim s1) = lim (f /* s1) by A1, A4, A5, A6, Th42;
then (r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A3, A6, VFUNCT_1:def 4
.= lim (r * (f /* s1)) by A7, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A2, A4, Th27, XBOOLE_1:1 ;
hence ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A2, A4, A8, Th27, XBOOLE_1:1; :: thesis: verum

end;

hence r (#) f is_continuous_on X by A3, Th42; :: thesis: verum