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 f is_continuous_in x ; :: thesis: - f is_continuous_in x
then (- 1) (#) f is_continuous_in x by Th30;
hence - f is_continuous_in x by NFCONT_4:7; :: thesis: verum