let X be set ; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
f is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_differentiable_on X implies f is_continuous_on X )
assume A1: f is_differentiable_on X ; :: thesis: f is_continuous_on X
hence A2: X c= dom f by Def9; :: according to CFCONT_1:def 2 :: thesis: for b₁ being Element of COMPLEX holds
( not b₁ in X or f | X is_continuous_in b₁ )
let x be Complex; :: thesis: ( not x in X or f | X is_continuous_in x )
assume x in X ; :: thesis: f | X is_continuous_in x
then A3: x in dom (f | X) by A2, RELAT_1:57;
f | X is differentiable by A1, Def9;
then f | X is_differentiable_in x by A3, Def8;
hence f | X is_continuous_in x by Th34; :: thesis: verum