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

A6: now

let x1 be Point of S; :: thesis: - (f /. x1) = f /. (- x1)
0. T = 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 S; :: thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
thus f /. (x1 - x2) = (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) - (f /. x2) by A6 ; :: thesis: verum

end;

now

let x1 be Point of S; :: thesis: for r being Real st x1 in the carrier of S & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
let r be Real; :: thesis: ( x1 in the carrier of S & r > 0 implies ex s being Real st
( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) ) )
assume ( x1 in the carrier of S & r > 0 ) ; :: thesis: ex s being Real st
( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
then consider s being Real such that
A8: ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A3, Th14;
take s = s; :: thesis: ( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
thus s > 0 by A8; :: thesis: for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r
let x2 be Point of S; :: thesis: ( x2 in the carrier of S & ||.(x2 - x1).|| < s implies ||.((f /. x2) - (f /. x1)).|| < r )
assume A9: ( x2 in the carrier of S & ||.(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. S) 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 S by A4, Th26; :: thesis: verum