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 )
A3: dom f = the carrier of CNS1 by A1, PARTFUN1:def 2;
given x0 being Point of CNS1 such that A4: f is_continuous_in x0 ; :: thesis: f is_continuous_on the carrier of CNS1
(f /. x0) + (0. CNS2) = f /. x0 by RLVECT_1:4
.= f /. (x0 + (0. CNS1)) by RLVECT_1:4
.= (f /. x0) + (f /. (0. CNS1)) by A2 ;
then A5: f /. (0. CNS1) = 0. CNS2 by RLVECT_1:8;

A6: now :: thesis: for x1 being Point of CNS1 holds - (f /. x1) = f /. (- x1)

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

end;

A7: now :: thesis: for x1, x2 being Point of CNS1 holds f /. (x1 - x2) = (f /. x1) - (f /. x2)

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 11
.= (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) + (- (f /. x2)) by A6
.= (f /. x1) - (f /. x2) by RLVECT_1:def 11 ; :: thesis: verum

end;

now :: thesis: for x1 being Point of CNS1
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 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 that
x1 in the carrier of CNS1 and
A8: 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 ) )
set y = x1 - x0;
consider s being Real such that
A9: 0 < s and
A10: for x1 being Point of CNS1 st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th8;
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 A9; :: 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 that
x2 in the carrier of CNS1 and
A11: ||.(x2 - x1).|| < s ; :: thesis: ||.((f /. x2) - (f /. x1)).|| < r
A12: (x1 - x0) + x0 = x1 - (x0 - x0) by RLVECT_1:29
.= x1 - (0. CNS1) by RLVECT_1:15
.= x1 by RLVECT_1:13 ;
then A13: ||.((x2 - (x1 - x0)) - x0).|| = ||.(x2 - x1).|| by RLVECT_1:27;
||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).|| by A2, A12
.= ||.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|| by RLVECT_1:27
.= ||.((f /. (x2 - (x1 - x0))) - (f /. x0)).|| by A7 ;
hence ||.((f /. x2) - (f /. x1)).|| < r by A3, A10, A11, A13; :: thesis: verum

end;

hence f is_continuous_on the carrier of CNS1 by A3, Th44; :: thesis: verum