let X be RealUnitarySpace; :: thesis: for w being Point of X
for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X
let w be Point of X; :: thesis: for f being Function of X,REAL st ( for v being Point of X holds f . v = w .|. v ) holds
f is_continuous_on the carrier of X
let f be Function of X,REAL; :: thesis: ( ( for v being Point of X holds f . v = w .|. v ) implies f is_continuous_on the carrier of X )
assume AS: for v being Point of X holds f . v = w .|. v ; :: thesis: f is_continuous_on the carrier of X
set Y = RUSp2RNSp X;
reconsider g = f as Function of (RUSp2RNSp X),REAL ;
A3: dom g = the carrier of (RUSp2RNSp X) by FUNCT_2:def 1;
for y0 being Point of (RUSp2RNSp X) st y0 in the carrier of (RUSp2RNSp X) holds
g | the carrier of (RUSp2RNSp X) is_continuous_in y0

proof

let y0 be Point of (RUSp2RNSp X); :: thesis: ( y0 in the carrier of (RUSp2RNSp X) implies g | the carrier of (RUSp2RNSp X) is_continuous_in y0 )
assume y0 in the carrier of (RUSp2RNSp X) ; :: thesis: g | the carrier of (RUSp2RNSp X) is_continuous_in y0
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )

proof

let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) )
assume AS1: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )
thus ex s being Real st
( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) :: thesis: verum

proof

C1: 0 <= ||.w.|| by BHSP_1:28;
reconsider s = r / (||.w.|| + 1) as Real ;
C41: ||.w.|| + 0 < ||.w.|| + 1 by XREAL_1:8;
s * (||.w.|| + 1) = r by C1, XCMPLX_1:87;
then C5: ( 0 < s & s * ||.w.|| < r ) by C1, AS1, C41, XREAL_1:68;
C6: for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r

proof

let y1 be Point of (RUSp2RNSp X); :: thesis: ( y1 in dom g & ||.(y1 - y0).|| < s implies |.((g /. y1) - (g /. y0)).| < r )
assume AS2: ( y1 in dom g & ||.(y1 - y0).|| < s ) ; :: thesis: |.((g /. y1) - (g /. y0)).| < r
reconsider x1 = y1 as Point of X ;
reconsider x0 = y0 as Point of X ;
X0: ||.(y1 - y0).|| = ||.(x1 - x0).|| by RHS4, RHS6;
D1: |.((g /. y1) - (g /. y0)).| = |.((w .|. x1) - (g . y0)).| by AS
.= |.((w .|. x1) - (w .|. x0)).| by AS
.= |.(w .|. (x1 - x0)).| by BHSP_1:12 ;
D2: |.(w .|. (x1 - x0)).| <= ||.w.|| * ||.(x1 - x0).|| by BHSP_1:29;
||.w.|| * ||.(x1 - x0).|| <= ||.w.|| * s by X0, C1, AS2, XREAL_1:64;
then |.((g /. y1) - (g /. y0)).| <= ||.w.|| * s by D1, D2, XXREAL_0:2;
hence |.((g /. y1) - (g /. y0)).| < r by C5, XXREAL_0:2; :: thesis: verum

end;

take s ; :: thesis: ( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) )
thus ( 0 < s & ( for y1 being Point of (RUSp2RNSp X) st y1 in dom g & ||.(y1 - y0).|| < s holds
|.((g /. y1) - (g /. y0)).| < r ) ) by C1, AS1, C6; :: thesis: verum

end;

end;

hence g | the carrier of (RUSp2RNSp X) is_continuous_in y0 by A3, NFCONT_1:8; :: thesis: verum

end;

then g is_continuous_on the carrier of (RUSp2RNSp X) by FUNCT_2:def 1;
hence f is_continuous_on the carrier of X by LM3C; :: thesis: verum