let n be Element of NAT ; :: thesis: for r, x0 being Real

for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

let r, x0 be Real; :: 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 A1: f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

g is_continuous_in x0 by A1;

then A2: r (#) g is_continuous_in x0 by NFCONT_3:13;

r (#) g = r (#) f by Th6;

hence r (#) f is_continuous_in x0 by A2; :: thesis: verum

for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

let r, x0 be Real; :: 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 A1: f is_continuous_in x0 ; :: thesis: r (#) f is_continuous_in x0

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

g is_continuous_in x0 by A1;

then A2: r (#) g is_continuous_in x0 by NFCONT_3:13;

r (#) g = r (#) f by Th6;

hence r (#) f is_continuous_in x0 by A2; :: thesis: verum