let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for x0 being Element of REAL m st f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let f be PartFunc of (REAL m),REAL; :: thesis: for x0 being Element of REAL m st f is_continuous_in x0 holds
|.f.| is_continuous_in x0
let x0 be Element of REAL m; :: thesis: ( f is_continuous_in x0 implies |.f.| is_continuous_in x0 )
assume f is_continuous_in x0 ; :: thesis: |.f.| is_continuous_in x0
then <>* f is_continuous_in x0 by Th37;
then |.(<>* f).| is_continuous_in x0 by Th32;
hence |.f.| is_continuous_in x0 by Th9; :: thesis: verum