let n be Element of NAT ; :: thesis: for x0 being Real
for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let x0 be Real; :: thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let f be PartFunc of REAL,(REAL n); :: thesis: ( x0 in dom f & f is_continuous_in x0 implies |.f.| is_continuous_in x0 )
assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; :: thesis: |.f.| is_continuous_in x0
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
g is_continuous_in x0 by A1;
then ||.g.|| is_continuous_in x0 by NFCONT_3:14;
hence |.f.| is_continuous_in x0 by Th9; :: thesis: verum