let m, n be non zero 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;
A2: ( 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) ;
A3: r (#) f1 is_continuous_in y by NFCONT_1:16, A1;
r (#) f = r (#) f1 by A2, NFCONT_4:6;
hence r (#) f is_continuous_in x by A3; :: thesis: verum