let X be set ; :: thesis: for f being PartFunc of COMPLEX ,COMPLEX st f is_continuous_on X holds
- f is_continuous_on X
let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is_continuous_on X implies - f is_continuous_on X )
A1: - f = (- 1r ) (#) f by CFUNCT_1:40;
assume f is_continuous_on X ; :: thesis: - f is_continuous_on X
hence - f is_continuous_on X by A1, Th67; :: thesis: verum