let m, n be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m
for r being Real st f is_continuous_in x holds
r (#) f is_continuous_in x
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m
for r being Real st f is_continuous_in x holds
r (#) f is_continuous_in x
let x be Element of REAL m; :: thesis: for r being Real st f is_continuous_in x holds
r (#) f is_continuous_in x
let r be Real; :: thesis: ( f is_continuous_in x implies r (#) f is_continuous_in x )
assume A1: f is_continuous_in x ; :: thesis: r (#) f is_continuous_in x
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
A20: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider f1 = f as PartFunc of (REAL-NS m),(REAL-NS n) ;
f1 is_continuous_in y by A1, PDIFF_7:35;
then A2: r (#) f1 is_continuous_in y by NFCONT_1:16;
r (#) f = r (#) f1 by NFCONT_4:6, A20;
hence r (#) f is_continuous_in x by A2, PDIFF_7:35; :: thesis: verum