let m be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of (REAL m),REAL; :: thesis: for x0 being Element of REAL m
for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let x0 be Element of REAL m; :: thesis: for r being Real st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let r be Real; :: thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0
then <>* f is_continuous_in x0 by XTh35;
then A2: r (#) (<>* f) is_continuous_in x0 by XTh351;
r (#) (<>* f) = <>* (r (#) f) by LMXTh11;
hence r (#) f is_continuous_in x0 by A2, XTh35; :: thesis: verum