let Y be Subset of COMPLEX; :: thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds
Y is open
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; :: thesis: Y is open
then A2: Y c= dom f by Def9;

now

let x0 be Complex; :: thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )
assume x0 in Y ; :: thesis: ex N being Neighbourhood of x0 st N c= Y
then A3: x0 in dom (f | Y) by A2, RELAT_1:57;
f | Y is differentiable by A1, Def9;
then f | Y is_differentiable_in x0 by A3, Def8;
then consider N being Neighbourhood of x0 such that
A4: N c= dom (f | Y) and
ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N holds
((f | Y) /. x) - ((f | Y) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
take N = N; :: thesis: N c= Y
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then dom (f | Y) c= Y by XBOOLE_1:17;
hence N c= Y by A4, XBOOLE_1:1; :: thesis: verum

end;

hence Y is open by Th11; :: thesis: verum