let S, T 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 )
A3: dom f = the carrier of S by A1, PARTFUN1:def 2;
given x0 being Point of S such that A4: f is_continuous_in x0 ; :: thesis: f is_continuous_on the carrier of S
(f /. x0) + (0. T) = f /. x0
.= f /. (x0 + (0. S))
.= (f /. x0) + (f /. (0. S)) by A2 ;
then A5: f /. (0. S) = 0. T by RLVECT_1:8;
A6: now :: thesis: for x1 being Point of S holds - (f /. x1) = f /. (- x1)
let x1 be Point of S; :: thesis: - (f /. x1) = f /. (- x1)
0. T = 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 S holds f /. (x1 - x2) = (f /. x1) - (f /. x2)
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 :: thesis: for x1 being Point of S
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 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 that
x1 in the carrier of S and
A8: 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 ) )
set y = x1 - x0;
consider s being Real such that
A9: 0 < s and
A10: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th7;
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 A9; :: 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 that
x2 in the carrier of S and
A11: ||.(x2 - x1).|| < s ; :: thesis: ||.((f /. x2) - (f /. x1)).|| < r
A12: (x1 - x0) + x0 = x1 - (x0 - x0) by RLVECT_1:29
.= x1 - (0. S) by RLVECT_1:15
.= x1 ;
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 S by A3, Th19; :: thesis: verum