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

now

let s1 be sequence of RNS; :: thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (z (#) f) /* s1 is convergent & (z (#) f) /. (lim s1) = lim ((z (#) f) /* s1) ) )
assume A4: ( rng s1 c= X & s1 is convergent & lim s1 in X ) ; :: thesis: ( (z (#) f) /* s1 is convergent & (z (#) f) /. (lim s1) = lim ((z (#) f) /* s1) )
then A5: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A1, Th64;
then A6: z * (f /* s1) is convergent by CLVECT_1:118;
(z (#) f) /. (lim s1) = z * (lim (f /* s1)) by A3, A4, A5, VFUNCT_2:def 4
.= lim (z * (f /* s1)) by A5, CLVECT_1:124
.= lim ((z (#) f) /* s1) by A2, A4, Th49, XBOOLE_1:1 ;
hence ( (z (#) f) /* s1 is convergent & (z (#) f) /. (lim s1) = lim ((z (#) f) /* s1) ) by A2, A4, A6, Th49, XBOOLE_1:1; :: thesis: verum

end;

hence z (#) f is_continuous_on X by A3, Th64; :: thesis: verum