let m be non zero 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 A1: r (#) (<>* f) is_continuous_in x0 by Th30, Th37;
r (#) (<>* f) = <>* (r (#) f) by Th8;
hence r (#) f is_continuous_in x0 by A1, Th37; :: thesis: verum