let m, n be non zero Element of NAT ; :: thesis: for Z being set
for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
- f is_continuous_on Z
let Z be set ; :: thesis: for f, g being PartFunc of (REAL m),(REAL n) st f is_continuous_on Z holds
- f is_continuous_on Z
let f, g be PartFunc of (REAL m),(REAL n); :: thesis: ( f is_continuous_on Z implies - f is_continuous_on Z )
assume A1: f is_continuous_on Z ; :: thesis: - f is_continuous_on Z
(- 1) (#) f is_continuous_on Z by A1, Th34;
hence - f is_continuous_on Z by NFCONT_4:7; :: thesis: verum