let x0 be Element of COMPLEX ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st f is_continuous_in x0 holds
- f is_continuous_in x0
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is_continuous_in x0 implies - f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; :: thesis: - f is_continuous_in x0
- f = (- 1r ) (#) f by CFUNCT_1:40;
hence - f is_continuous_in x0 by A1, Th56; :: thesis: verum