let CNS1, CNS2 be ComplexNormSpace; :: thesis: for f being PartFunc of CNS1,CNS2 st f is total & ( for x1, x2 being Point of CNS1 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS1 st f is_continuous_in x0 holds
f is_continuous_on the carrier of CNS1
let f be PartFunc of CNS1,CNS2; :: thesis: ( f is total & ( for x1, x2 being Point of CNS1 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of CNS1 st f is_continuous_in x0 implies f is_continuous_on the carrier of CNS1 )
assume that
A1: f is total and
A2: for x1, x2 being Point of CNS1 holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ; :: thesis: ( for x0 being Point of CNS1 holds not f is_continuous_in x0 or f is_continuous_on the carrier of CNS1 )
given x0 being Point of CNS1 such that A3: f is_continuous_in x0 ; :: thesis: f is_continuous_on the carrier of CNS1
A4: dom f = the carrier of CNS1 by A1, PARTFUN1:def 4;
(f /. x0) + (0. CNS2) = f /. x0 by RLVECT_1:10
.= f /. (x0 + (0. CNS1)) by RLVECT_1:10
.= (f /. x0) + (f /. (0. CNS1)) by A2 ;
then A5: f /. (0. CNS1) = 0. CNS2 by RLVECT_1:21;

A6: now

let x1 be Point of CNS1; :: thesis: - (f /. x1) = f /. (- x1)
0. CNS2 = f /. (x1 + (- x1)) by A5, RLVECT_1:16
.= (f /. x1) + (f /. (- x1)) by A2 ;
hence - (f /. x1) = f /. (- x1) by RLVECT_1:19; :: thesis: verum

end;

A7: now

let x1, x2 be Point of CNS1; :: thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
thus f /. (x1 - x2) = f /. (x1 + (- x2)) by RLVECT_1:def 12
.= (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) + (- (f /. x2)) by A6
.= (f /. x1) - (f /. x2) by RLVECT_1:def 12 ; :: thesis: verum

end;

now

let x1 be Point of CNS1; :: thesis: for r being Real st x1 in the carrier of CNS1 & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Point of CNS1 st x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
let r be Real; :: thesis: ( x1 in the carrier of CNS1 & r > 0 implies ex s being Real st
( s > 0 & ( for x2 being Point of CNS1 st x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) ) )
assume ( x1 in the carrier of CNS1 & r > 0 ) ; :: thesis: ex s being Real st
( s > 0 & ( for x2 being Point of CNS1 st x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
then consider s being Real such that
A8: ( 0 < s & ( for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A3, Th29;
take s = s; :: thesis: ( s > 0 & ( for x2 being Point of CNS1 st x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
thus s > 0 by A8; :: thesis: for x2 being Point of CNS1 st x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r
let x2 be Point of CNS1; :: thesis: ( x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s implies ||.((f /. x2) - (f /. x1)).|| < r )
assume A9: ( x2 in the carrier of CNS1 & ||.(x2 - x1).|| < s ) ; :: thesis: ||.((f /. x2) - (f /. x1)).|| < r
set y = x1 - x0;
A10: (x1 - x0) + x0 = x1 - (x0 - x0) by RLVECT_1:43
.= x1 - (0. CNS1) by RLVECT_1:28
.= x1 by RLVECT_1:26 ;
then A11: ||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).|| by A2
.= ||.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|| by RLVECT_1:41
.= ||.((f /. (x2 - (x1 - x0))) - (f /. x0)).|| by A7 ;
||.((x2 - (x1 - x0)) - x0).|| = ||.(x2 - x1).|| by A10, RLVECT_1:41;
hence ||.((f /. x2) - (f /. x1)).|| < r by A4, A8, A9, A11; :: thesis: verum

end;

hence f is_continuous_on the carrier of CNS1 by A4, Th65; :: thesis: verum