let n be Element of NAT ; :: thesis: for r being Real
for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let r be Real; :: thesis: for x0 being real number
for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let x0 be real number ; :: thesis: for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL,(REAL n); :: thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume AS: f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0
reconsider g = f as PartFunc of REAL, the carrier of (REAL-NS n) by REAL_NS1:def 4;
g is_continuous_in x0 by AS, Def1Th;
then P1: r (#) g is_continuous_in x0 by NFCONT_3:13;
r (#) g = r (#) f by LM003B;
hence r (#) f is_continuous_in x0 by P1, Def1Th; :: thesis: verum