let m, n be non zero Element of NAT ; :: thesis: for Z being set
for r being Real
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
r (#) f is_continuous_on Z
let Z be set ; :: thesis: for r being Real
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
r (#) f is_continuous_on Z
let r be Real; :: thesis: for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
r (#) f is_continuous_on Z
let f, g be PartFunc of (REAL m),(REAL n); :: thesis: ( f is_continuous_on Z implies r (#) f is_continuous_on Z )
assume A1: f is_continuous_on Z ; :: thesis: r (#) f is_continuous_on Z
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) ;
f1 is_continuous_on Z by A1, PDIFF_7:37;
then A3: r (#) f1 is_continuous_on Z by NFCONT_1:27;
r (#) f1 = r (#) f by A2, NFCONT_4:6;
hence r (#) f is_continuous_on Z by A3, PDIFF_7:37; :: thesis: verum