:: by Hiroyuki Okazaki , Noboru Endou and Yasunari Shidama

::

:: Received August 17, 2010

:: Copyright (c) 2010-2016 Association of Mizar Users

theorem Th1: :: NFCONT_3:1

for n being Nat

for S being RealNormSpace

for seq being Real_Sequence

for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds

seq . n in dom h

for S being RealNormSpace

for seq being Real_Sequence

for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds

seq . n in dom h

proof end;

theorem Th2: :: NFCONT_3:2

for S being RealNormSpace

for h1, h2 being PartFunc of REAL, the carrier of S

for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

for h1, h2 being PartFunc of REAL, the carrier of S

for seq being Real_Sequence st rng seq c= (dom h1) /\ (dom h2) holds

( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )

proof end;

theorem Th4: :: NFCONT_3:4

for S being RealNormSpace

for h being PartFunc of REAL, the carrier of S

for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

for h being PartFunc of REAL, the carrier of S

for seq being Real_Sequence

for r being Real st rng seq c= dom h holds

(r (#) h) /* seq = r * (h /* seq)

proof end;

theorem Th5: :: NFCONT_3:5

for S being RealNormSpace

for h being PartFunc of REAL, the carrier of S

for seq being Real_Sequence st rng seq c= dom h holds

( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )

for h being PartFunc of REAL, the carrier of S

for seq being Real_Sequence st rng seq c= dom h holds

( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )

proof end;

definition

let S be RealNormSpace;

let f be PartFunc of REAL, the carrier of S;

let x0 be Real;

end;
let f be PartFunc of REAL, the carrier of S;

let x0 be Real;

pred f is_continuous_in x0 means :: NFCONT_3:def 1

( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );

( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) );

:: deftheorem defines is_continuous_in NFCONT_3:def 1 :

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) );

theorem Th6: :: NFCONT_3:6

for X being set

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds

f | X is_continuous_in x0

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st x0 in X & f is_continuous_in x0 holds

f | X is_continuous_in x0

proof end;

theorem :: NFCONT_3:7

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Nat holds s1 . n <> x0 ) holds

( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )

proof end;

theorem Th8: :: NFCONT_3:8

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in dom f & |.(x1 - x0).| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )

proof end;

theorem Th9: :: NFCONT_3:9

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st

for x1 being Real st x1 in dom f & x1 in N holds

f /. x1 in N1 ) ) )

proof end;

theorem Th10: :: NFCONT_3:10

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )

for f being PartFunc of REAL, the carrier of S

for x0 being Real holds

( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) )

proof end;

theorem :: NFCONT_3:11

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds

f is_continuous_in x0

proof end;

theorem :: NFCONT_3:12

for x0 being Real

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds

( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )

proof end;

theorem Th13: :: NFCONT_3:13

for r, x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f is_continuous_in x0 holds

r (#) f is_continuous_in x0

proof end;

theorem :: NFCONT_3:14

for x0 being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st x0 in dom f & f is_continuous_in x0 holds

( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st x0 in dom f & f is_continuous_in x0 holds

( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )

proof end;

theorem :: NFCONT_3:15

for x0 being Real

for S, T being RealNormSpace

for f1 being PartFunc of REAL, the carrier of S

for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

for S, T being RealNormSpace

for f1 being PartFunc of REAL, the carrier of S

for f2 being PartFunc of the carrier of S, the carrier of T st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds

f2 * f1 is_continuous_in x0

proof end;

definition

let S be RealNormSpace;

let f be PartFunc of REAL, the carrier of S;

end;
let f be PartFunc of REAL, the carrier of S;

attr f is continuous means :Def2: :: NFCONT_3:def 2

for x0 being Real st x0 in dom f holds

f is_continuous_in x0;

for x0 being Real st x0 in dom f holds

f is_continuous_in x0;

:: deftheorem Def2 defines continuous NFCONT_3:def 2 :

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is continuous iff for x0 being Real st x0 in dom f holds

f is_continuous_in x0 );

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is continuous iff for x0 being Real st x0 in dom f holds

f is_continuous_in x0 );

theorem Th16: :: NFCONT_3:16

for S being RealNormSpace

for X being set

for f being PartFunc of REAL, the carrier of S st X c= dom f holds

( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )

for X being set

for f being PartFunc of REAL, the carrier of S st X c= dom f holds

( f | X is continuous iff for s1 being Real_Sequence st rng s1 c= X & s1 is convergent & lim s1 in X holds

( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )

proof end;

theorem Th17: :: NFCONT_3:17

for X being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f holds

( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f holds

( f | X is continuous iff for x0, r being Real st x0 in X & 0 < r holds

ex s being Real st

( 0 < s & ( for x1 being Real st x1 in X & |.(x1 - x0).| < s holds

||.((f /. x1) - (f /. x0)).|| < r ) ) )

proof end;

registration

let S be RealNormSpace;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} is constant holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

registration

let S be RealNormSpace;

ex b_{1} being PartFunc of REAL, the carrier of S st b_{1} is continuous

end;
cluster Relation-like REAL -defined the carrier of S -valued Function-like continuous for Element of bool [:REAL, the carrier of S:];

existence ex b

proof end;

registration

let S be RealNormSpace;

let f be continuous PartFunc of REAL, the carrier of S;

let X be set ;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f | X holds

b_{1} is continuous

end;
let f be continuous PartFunc of REAL, the carrier of S;

let X be set ;

coherence

for b

b

proof end;

theorem Th18: :: NFCONT_3:18

for X, X1 being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is continuous & X1 c= X holds

f | X1 is continuous

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is continuous & X1 c= X holds

f | X1 is continuous

proof end;

registration

let S be RealNormSpace;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} is empty holds

b_{1} is continuous
;

end;
coherence

for b

b

registration

let S be RealNormSpace;

let f be PartFunc of REAL, the carrier of S;

let X be trivial set ;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f | X holds

b_{1} is continuous

end;
let f be PartFunc of REAL, the carrier of S;

let X be trivial set ;

coherence

for b

b

proof end;

registration

let S be RealNormSpace;

let f1, f2 be continuous PartFunc of REAL, the carrier of S;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f1 + f2 holds

b_{1} is continuous

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f1 - f2 holds

b_{1} is continuous

end;
let f1, f2 be continuous PartFunc of REAL, the carrier of S;

coherence

for b

b

proof end;

coherence for b

b

proof end;

theorem Th19: :: NFCONT_3:19

for S being RealNormSpace

for X being set

for f1, f2 being PartFunc of REAL, the carrier of S st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )

for X being set

for f1, f2 being PartFunc of REAL, the carrier of S st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds

( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )

proof end;

theorem :: NFCONT_3:20

for S being RealNormSpace

for X, X1 being set

for f1, f2 being PartFunc of REAL, the carrier of S st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds

( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )

for X, X1 being set

for f1, f2 being PartFunc of REAL, the carrier of S st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds

( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )

proof end;

registration

let S be RealNormSpace;

let f be continuous PartFunc of REAL, the carrier of S;

let r be Real;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = r (#) f holds

b_{1} is continuous

end;
let f be continuous PartFunc of REAL, the carrier of S;

let r be Real;

coherence

for b

b

proof end;

theorem Th21: :: NFCONT_3:21

for X being set

for r being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

for r being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds

(r (#) f) | X is continuous

proof end;

theorem :: NFCONT_3:22

for X being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds

( ||.f.|| | X is continuous & (- f) | X is continuous )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st X c= dom f & f | X is continuous holds

( ||.f.|| | X is continuous & (- f) | X is continuous )

proof end;

theorem :: NFCONT_3:23

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 holds

f | REAL is continuous

for f being PartFunc of REAL, the carrier of S st f is total & ( for x1, x2 being Real holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Real st f is_continuous_in x0 holds

f | REAL is continuous

proof end;

theorem Th24: :: NFCONT_3:24

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st dom f is compact & f | (dom f) is continuous holds

rng f is compact

for f being PartFunc of REAL, the carrier of S st dom f is compact & f | (dom f) is continuous holds

rng f is compact

proof end;

theorem :: NFCONT_3:25

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

for f being PartFunc of REAL, the carrier of S

for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds

f .: Y is compact

proof end;

:: deftheorem Def3 defines Lipschitzian NFCONT_3:def 3 :

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is Lipschitzian iff ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) );

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f is Lipschitzian iff ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) );

theorem Th26: :: NFCONT_3:26

for X being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f | X is Lipschitzian iff ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds

||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S holds

( f | X is Lipschitzian iff ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds

||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) )

proof end;

registration

let S be RealNormSpace;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} is empty holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

registration

let S be RealNormSpace;

ex b_{1} being PartFunc of REAL, the carrier of S st b_{1} is empty

end;
cluster Relation-like REAL -defined the carrier of S -valued empty Function-like for Element of bool [:REAL, the carrier of S:];

existence ex b

proof end;

registration

let S be RealNormSpace;

let f be Lipschitzian PartFunc of REAL, the carrier of S;

let X be set ;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f | X holds

b_{1} is Lipschitzian

end;
let f be Lipschitzian PartFunc of REAL, the carrier of S;

let X be set ;

coherence

for b

b

proof end;

theorem :: NFCONT_3:27

for X, X1 being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X1 c= X holds

f | X1 is Lipschitzian

proof end;

registration

let S be RealNormSpace;

let f1, f2 be Lipschitzian PartFunc of REAL, the carrier of S;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f1 + f2 holds

b_{1} is Lipschitzian

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = f1 - f2 holds

b_{1} is Lipschitzian

end;
let f1, f2 be Lipschitzian PartFunc of REAL, the carrier of S;

coherence

for b

b

proof end;

coherence for b

b

proof end;

theorem :: NFCONT_3:28

for X, X1 being set

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 + f2) | (X /\ X1) is Lipschitzian

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 + f2) | (X /\ X1) is Lipschitzian

proof end;

theorem :: NFCONT_3:29

for X, X1 being set

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

for S being RealNormSpace

for f1, f2 being PartFunc of REAL, the carrier of S st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds

(f1 - f2) | (X /\ X1) is Lipschitzian

proof end;

registration

let S be RealNormSpace;

let f be Lipschitzian PartFunc of REAL, the carrier of S;

let p be Real;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} = p (#) f holds

b_{1} is Lipschitzian

end;
let f be Lipschitzian PartFunc of REAL, the carrier of S;

let p be Real;

coherence

for b

b

proof end;

theorem :: NFCONT_3:30

for X being set

for p being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

for p being Real

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X c= dom f holds

(p (#) f) | X is Lipschitzian

proof end;

registration

let S be RealNormSpace;

let f be Lipschitzian PartFunc of REAL, the carrier of S;

coherence

for b_{1} being PartFunc of REAL,REAL st b_{1} = ||.f.|| holds

b_{1} is Lipschitzian

end;
let f be Lipschitzian PartFunc of REAL, the carrier of S;

coherence

for b

b

proof end;

theorem :: NFCONT_3:31

for X being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian holds

( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )

proof end;

registration

let S be RealNormSpace;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} is constant holds

b_{1} is Lipschitzian

end;
coherence

for b

b

proof end;

registration

let S be RealNormSpace;

coherence

for b_{1} being PartFunc of REAL, the carrier of S st b_{1} is Lipschitzian holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

theorem :: NFCONT_3:32

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S st ex r being Point of S st rng f = {r} holds

f is continuous

for f being PartFunc of REAL, the carrier of S st ex r being Point of S st rng f = {r} holds

f is continuous

proof end;

theorem :: NFCONT_3:33

for X being set

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for r, p being Point of S st ( for x0 being Real st x0 in X holds

f /. x0 = (x0 * r) + p ) holds

f | X is continuous

for S being RealNormSpace

for f being PartFunc of REAL, the carrier of S

for r, p being Point of S st ( for x0 being Real st x0 in X holds

f /. x0 = (x0 * r) + p ) holds

f | X is continuous

proof end;