let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: ( f is total & ( for x1, x2 being Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Element of 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 Element of COMPLEX holds f /. (x1 + x2) = (f /. x1) + (f /. x2) and
A3: ex x0 being Element of COMPLEX st f is_continuous_in x0 ; :: thesis: f is_continuous_on COMPLEX
A4: dom f = COMPLEX by A1, PARTFUN1:def 4;
consider x0 being Element of 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

let x1 be Element of 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

let x1, x2 be Element of 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

let x1 be Element of COMPLEX ; :: thesis: for r being Real st x1 in COMPLEX & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Element of 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 Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) ) )
assume ( x1 in COMPLEX & r > 0 ) ; :: thesis: ex s being Real st
( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
then consider s being Real such that
A9: ( 0 < s & ( for x1 being Element of COMPLEX st x1 in dom f & |.(x1 - x0).| < s holds
|.((f /. x1) - (f /. x0)).| < r ) ) by A5, Th54;
take s = s; :: thesis: ( s > 0 & ( for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r ) )
thus s > 0 by A9; :: thesis: for x2 being Element of COMPLEX st x2 in COMPLEX & |.(x2 - x1).| < s holds
|.((f /. x2) - (f /. x1)).| < r
let x2 be Element of COMPLEX ; :: thesis: ( x2 in COMPLEX & |.(x2 - x1).| < s implies |.((f /. x2) - (f /. x1)).| < r )
assume A10: ( x2 in COMPLEX & |.(x2 - x1).| < s ) ; :: thesis: |.((f /. x2) - (f /. x1)).| < r
set y = x1 - x0;
(x1 - x0) + x0 = x1 ;
then A11: |.((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 ;
|.((x2 - (x1 - x0)) - x0).| = |.(x2 - x1).| ;
hence |.((f /. x2) - (f /. x1)).| < r by A4, A9, A10, A11; :: thesis: verum

end;

hence f is_continuous_on COMPLEX by A4, Th61; :: thesis: verum