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 )
A1: - 1 is Real by XREAL_0:def 1;
assume f is_continuous_in x ; :: thesis: - f is_continuous_in x
then (- 1) (#) f is_continuous_in x by A1, XTh351;
hence - f is_continuous_in x by NFCONT_4:7; :: thesis: verum