let m, n be non zero Element of NAT ; for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
|.f.| is_continuous_on Z
let Z be set ; for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
|.f.| is_continuous_on Z
let f, g be PartFunc of (REAL m),(REAL n); ( f is_continuous_on Z implies |.f.| is_continuous_on Z )
assume A1:
f is_continuous_on Z
; |.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:
||.f1.|| is_continuous_on Z
by NFCONT_1:28;
||.f1.|| = |.f.|
by A2, NFCONT_4:9;
hence
|.f.| is_continuous_on Z
by A3, Th49; verum