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 st f is_continuous_in x holds
|.f.| is_continuous_in x
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m st f is_continuous_in x holds
|.f.| is_continuous_in x
let x be Element of REAL m; :: thesis: ( f is_continuous_in x implies |.f.| is_continuous_in x )
assume A1: f is_continuous_in x ; :: thesis: |.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: ||.f1.|| is_continuous_in y by NFCONT_1:17;
|.f.| = ||.f1.|| by NFCONT_4:9, A20;
hence |.f.| is_continuous_in x by A2, NFCONT_4:21; :: thesis: verum