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 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;
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: ||.f1.|| is_continuous_in y by NFCONT_1:17, A1;
|.f.| = ||.f1.|| by A2, NFCONT_4:9;
hence |.f.| is_continuous_in x by A3, NFCONT_4:21; :: thesis: verum