let f be PartFunc of COMPLEX,COMPLEX; :: thesis: ( f is total & ( for x1, x2 being Complex holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Complex st f is_continuous_in x0 implies f is_continuous_on COMPLEX )
assume that
A1: f is total and
A2: for x1, x2 being Complex holds f /. (x1 + x2) = (f /. x1) + (f /. x2) and
A3: ex x0 being Complex st f is_continuous_in x0 ; :: thesis: f is_continuous_on COMPLEX
A4: dom f = COMPLEX by A1, PARTFUN1:def 2;
consider x0 being Complex such that
A5: f is_continuous_in x0 by A3;
A6: (f /. x0) + 0c = f /. (x0 + 0c)
.= (f /. x0) + (f /. 0c) by A2 ;
A7: now :: thesis: for x1 being Complex holds - (f /. x1) = f /. (- x1)
let x1 be Complex; :: thesis: - (f /. x1) = f /. (- x1)
0c = f /. (x1 + (- x1)) by A6
.= (f /. x1) + (f /. (- x1)) by A2 ;
hence - (f /. x1) = f /. (- x1) ; :: thesis: verum
end;
A8: now :: thesis: for x1, x2 being Complex holds f /. (x1 - x2) = (f /. x1) - (f /. x2)
let x1, x2 be Complex; :: thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
thus f /. (x1 - x2) = f /. (x1 + (- x2))
.= (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) + (- (f /. x2)) by A7
.= (f /. x1) - (f /. x2) ; :: thesis: verum
end;
now :: thesis: for x1 being Complex
for r being Real st x1 in COMPLEX & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
let x1 be Complex; :: thesis: for r being Real st x1 in COMPLEX & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
let r be Real; :: thesis: ( x1 in COMPLEX & r > 0 implies ex s being Real st
( s > 0 & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) ) )
assume that
x1 in COMPLEX and
A9: r > 0 ; :: thesis: ex s being Real st
( s > 0 & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
set y = x1 - x0;
consider s being Real such that
A10: 0 < s and
A11: for x1 being Complex st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r by A5, A9, Th32;
take s = s; :: thesis: ( s > 0 & ( for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
thus s > 0 by A10; :: thesis: for x2 being Complex st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r
let x2 be Complex; :: thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.((f /. x2) - (f /. x1)).| < r )
assume that
x2 in COMPLEX and
A12: |.(x2 - x1).| < s ; :: thesis: |.((f /. x2) - (f /. x1)).| < r
A13: |.((x2 - (x1 - x0)) - x0).| = |.(x2 - x1).| ;
A14: x2 - (x1 - x0) in dom f by A4, XCMPLX_0:def 2;
(x1 - x0) + x0 = x1 ;
then |.((f /. x2) - (f /. x1)).| = |.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).| by A2
.= |.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|
.= |.((f /. (x2 - (x1 - x0))) - (f /. x0)).| by A8 ;
hence |.((f /. x2) - (f /. x1)).| < r by A11, A12, A13, A14; :: thesis: verum
end;
hence f is_continuous_on COMPLEX by A4, Th39; :: thesis: verum