:: NFCONT_3 semantic presentation

begin


theorem Th1: :: NFCONT_3:1
for n being Element of 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
proof
let n be Element of NAT ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let seq be Real_Sequence; ::_thesis: for h being PartFunc of REAL, the carrier of S st rng seq c= dom h holds
seq . n in dom h
let h be PartFunc of REAL, the carrier of S; ::_thesis: ( rng seq c= dom h implies seq . n in dom h )
 n in NAT ;
then A1: n in dom seq by FUNCT_2:def_1;
assume  rng seq c= dom h ; ::_thesis: seq . n in dom h
then  n in dom (h * seq) by A1, RELAT_1:27;
hence  seq . n in dom h by FUNCT_1:11; ::_thesis: verum
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) )
proof
let S be RealNormSpace; ::_thesis: 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) )
let h1, h2 be PartFunc of REAL, the carrier of S; ::_thesis: 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) )
let seq be Real_Sequence; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) )
A1: ( (dom h1) /\ (dom h2) c= dom h1 & (dom h1) /\ (dom h2) c= dom h2 ) by XBOOLE_1:17;
assume A2: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_+_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n)
A3: ( h1 /. (seq . n) = (h1 /* seq) . n & h2 /. (seq . n) = (h2 /* seq) . n ) by A1, A2, FUNCT_2:109, XBOOLE_1:1;
A4: rng seq c= dom (h1 + h2) by A2, VFUNCT_1:def_1;
then A5: seq . n in dom (h1 + h2) by Th1;
thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109
.= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A5, VFUNCT_1:def_1 ; ::_thesis: verum
end;
hence  (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by NORMSP_1:def_2; ::_thesis: (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n)
A6: ( h1 /. (seq . n) = (h1 /* seq) . n & h2 /. (seq . n) = (h2 /* seq) . n ) by A1, A2, FUNCT_2:109, XBOOLE_1:1;
A7: rng seq c= dom (h1 - h2) by A2, VFUNCT_1:def_2;
then A8: seq . n in dom (h1 - h2) by Th1;
thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A7, FUNCT_2:109
.= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A6, A8, VFUNCT_1:def_2 ; ::_thesis: verum
end;
hence  (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by NORMSP_1:def_3; ::_thesis: verum
end;

theorem :: NFCONT_3:3
for S being RealNormSpace
for h being sequence of S
for r being Real holds r (#) h = r * h
proof
let S be RealNormSpace; ::_thesis: for h being sequence of S
for r being Real holds r (#) h = r * h
let h be sequence of S; ::_thesis: for r being Real holds r (#) h = r * h
let r be Real; ::_thesis: r (#) h = r * h
 dom h = NAT by FUNCT_2:def_1;
then A1: dom (r (#) h) = NAT by VFUNCT_1:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_h)_._n_=_r_*_(h_._n)
let n be Element of NAT ; ::_thesis: (r (#) h) . n = r * (h . n)
 (r (#) h) . n = (r (#) h) /. n ;
then  (r (#) h) . n = r * (h /. n) by A1, VFUNCT_1:def_4;
hence  (r (#) h) . n = r * (h . n) ; ::_thesis: verum
end;
hence  r (#) h = r * h by NORMSP_1:def_5; ::_thesis: verum
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)
proof
let S be RealNormSpace; ::_thesis: 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)
let h be PartFunc of REAL, the carrier of S; ::_thesis: for seq being Real_Sequence
for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
let seq be Real_Sequence; ::_thesis: for r being Real st rng seq c= dom h holds
(r (#) h) /* seq = r * (h /* seq)
let r be Real; ::_thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r * (h /* seq) )
assume A1: rng seq c= dom h ; ::_thesis: (r (#) h) /* seq = r * (h /* seq)
then A2: rng seq c= dom (r (#) h) by VFUNCT_1:def_4;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_h)_/*_seq)_._n_=_r_*_((h_/*_seq)_._n)
let n be Element of NAT ; ::_thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n)
A3: seq . n in dom (r (#) h) by A2, Th1;
thus ((r (#) h) /* seq) . n = (r (#) h) /. (seq . n) by A2, FUNCT_2:109
.= r * (h /. (seq . n)) by A3, VFUNCT_1:def_4
.= r * ((h /* seq) . n) by A1, FUNCT_2:109 ; ::_thesis: verum
end;
hence  (r (#) h) /* seq = r * (h /* seq) by NORMSP_1:def_5; ::_thesis: verum
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 )
proof
let S be RealNormSpace; ::_thesis: 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 )
let h be PartFunc of REAL, the carrier of S; ::_thesis: for seq being Real_Sequence st rng seq c= dom h holds
( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
let seq be Real_Sequence; ::_thesis: ( rng seq c= dom h implies ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) )
assume A1: rng seq c= dom h ; ::_thesis: ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq )
then A2: rng seq c= dom ||.h.|| by NORMSP_0:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.(h_/*_seq).||_._n_=_(||.h.||_/*_seq)_._n
let n be Element of NAT ; ::_thesis: ||.(h /* seq).|| . n = (||.h.|| /* seq) . n
 seq . n in rng seq by FUNCT_2:4;
then  seq . n in dom h by A1;
then A3: seq . n in dom ||.h.|| by NORMSP_0:def_3;
thus ||.(h /* seq).|| . n = ||.((h /* seq) . n).|| by NORMSP_0:def_4
.= ||.(h /. (seq . n)).|| by A1, FUNCT_2:109
.= ||.h.|| . (seq . n) by A3, NORMSP_0:def_3
.= ||.h.|| /. (seq . n) by A3, PARTFUN1:def_6
.= (||.h.|| /* seq) . n by A2, FUNCT_2:109 ; ::_thesis: verum
end;
hence  ||.(h /* seq).|| = ||.h.|| /* seq by FUNCT_2:63; ::_thesis: - (h /* seq) = (- h) /* seq
now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_(h_/*_seq))_._n_=_((-_h)_/*_seq)_._n
let n be Element of NAT ; ::_thesis: (- (h /* seq)) . n = ((- h) /* seq) . n
thus (- (h /* seq)) . n = - ((h /* seq) . n) by BHSP_1:44
.= (- 1) * ((h /* seq) . n) by RLVECT_1:16
.= ((- 1) * (h /* seq)) . n by NORMSP_1:def_5
.= (((- 1) (#) h) /* seq) . n by A1, Th4
.= ((- h) /* seq) . n by VFUNCT_1:23 ; ::_thesis: verum
end;
hence  - (h /* seq) = (- h) /* seq by FUNCT_2:63; ::_thesis: verum
end;

begin

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
let x0 be real number ;
predf is_continuous_in x0 means :Def1: :: 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) ) ) );
end;

:: deftheorem Def1 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 number 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 number
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
let X be set ; ::_thesis: for x0 being real number
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
let x0 be real number ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 )
assume that
A1: x0 in X and
A2: f is_continuous_in x0 ; ::_thesis: f | X is_continuous_in x0
A3: x0 in dom f by Def1, A2;
A4: dom (f | X) = X /\ (dom f) by RELAT_1:61;
hence A5: x0 in dom (f | X) by A1, A3, XBOOLE_0:def_4; :: according to NFCONT_3:def_1 ::_thesis: for s1 being Real_Sequence st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x0 holds
( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) )
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x0 implies ( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) ) )
assume that
A6: rng s1 c= dom (f | X) and
A7: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) /. x0 = lim ((f | X) /* s1) )
A8: rng s1 c= dom f by A6, A4, XBOOLE_1:18;
A9: (f | X) /* s1 = f /* s1 by A6, FUNCT_2:117;
hence  (f | X) /* s1 is convergent by A2, A7, A8, Def1; ::_thesis: (f | X) /. x0 = lim ((f | X) /* s1)
 x0 in REAL by XREAL_0:def_1;
hence (f | X) /. x0 = f /. x0 by A5, PARTFUN2:15
.= lim ((f | X) /* s1) by A2, A7, A8, A9, Def1 ;
::_thesis: verum
end;

theorem :: NFCONT_3:7
for x0 being real number
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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
proof
let x0 be real number ; ::_thesis: 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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let S be RealNormSpace; ::_thesis: 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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( 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 Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) )
thus  ( f is_continuous_in x0 implies ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ) by Def1; ::_thesis: ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) implies f is_continuous_in x0 )
assume A1: ( x0 in dom f & ( for s1 being Real_Sequence st rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) holds
( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ; ::_thesis: f is_continuous_in x0
thus  x0 in dom f by A1; :: according to NFCONT_3:def_1 ::_thesis: 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) )
let s2 be Real_Sequence; ::_thesis: ( rng s2 c= dom f & s2 is convergent & lim s2 = x0 implies ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) )
assume that
A2: rng s2 c= dom f and
A3: ( s2 is convergent & lim s2 = x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
percases ( ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 or for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ) ;
suppose ex n being Element of NAT st
for m being Element of NAT st n <= m holds
s2 . m = x0 ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
then consider N being Element of NAT  such that
A4: for m being Element of NAT st N <= m holds
s2 . m = x0 ;
A5: f /* (s2 ^\ N) = (f /* s2) ^\ N by A2, VALUED_0:27;
A6: now__::_thesis:_for_p_being_Real_st_p_>_0_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.(((f_/*_(s2_^\_N))_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( p > 0 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )
assume A7: p > 0 ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p )
assume  n <= m ; ::_thesis: ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p
A8: s2 . (m + N) = x0 by A4, NAT_1:12;
 rng (s2 ^\ N) c= rng s2 by VALUED_0:21;
then ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| = ||.((f /. ((s2 ^\ N) . m)) - (f /. x0)).|| by A2, FUNCT_2:109, XBOOLE_1:1
.= ||.((f /. x0) - (f /. x0)).|| by A8, NAT_1:def_3
.= 0 by NORMSP_1:6 ;
hence  ||.(((f /* (s2 ^\ N)) . m) - (f /. x0)).|| < p by A7; ::_thesis: verum
end;
then A9: f /* (s2 ^\ N) is convergent by NORMSP_1:def_6;
then  f /. x0 = lim ((f /* s2) ^\ N) by A6, A5, NORMSP_1:def_7;
hence  ( f /* s2 is convergent & f /. x0 = lim (f /* s2) ) by A9, A5, LOPBAN_3:10, LOPBAN_3:11; ::_thesis: verum
end;
supposeA10: for n being Element of NAT ex m being Element of NAT st
( n <= m & s2 . m <> x0 ) ; ::_thesis: ( f /* s2 is convergent & f /. x0 = lim (f /* s2) )
defpred S1[ Element of NAT , set , set ] means  for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & s2 . m <> x0 & ( for k being Element of NAT st n < k & s2 . k <> x0 holds
m <= k ) );
defpred S2[ set ] means s2 . $1 <> x0;
 ex m1 being Element of NAT st
( 0 <= m1 & s2 . m1 <> x0 ) by A10;
then A11: ex m being Nat st S2[m] ;
consider M being Nat such that
A12: ( S2[M] & ( for n being Nat st S2[n] holds
M <= n ) ) from NAT_1:sch_5(A11);
reconsider M9 = M as Element of NAT by ORDINAL1:def_12;
A13: now__::_thesis:_for_n_being_Element_of_NAT_ex_m_being_Element_of_NAT_st_
(_n_<_m_&_s2_._m_<>_x0_)
let n be Element of NAT ; ::_thesis: ex m being Element of NAT st
( n < m & s2 . m <> x0 )
consider m being Element of NAT  such that
A14: ( n + 1 <= m & s2 . m <> x0 ) by A10;
take m = m; ::_thesis: ( n < m & s2 . m <> x0 )
thus  ( n < m & s2 . m <> x0 ) by A14, NAT_1:13; ::_thesis: verum
end;
A15: for n, x being Element of NAT ex y being Element of NAT st S1[n,x,y]
proof
let n, x be Element of NAT ; ::_thesis: ex y being Element of NAT st S1[n,x,y]
defpred S3[ Nat] means ( x < $1 & s2 . $1 <> x0 );
 ex m being Element of NAT st S3[m] by A13;
then A16: ex m being Nat st S3[m] ;
consider l being Nat such that
A17: ( S3[l] & ( for k being Nat st S3[k] holds
l <= k ) ) from NAT_1:sch_5(A16);
take  l ; ::_thesis: ( l is Element of REAL & l is Element of NAT & S1[n,x,l] )
 l in NAT by ORDINAL1:def_12;
hence  ( l is Element of REAL & l is Element of NAT & S1[n,x,l] ) by A17; ::_thesis: verum
end;
consider F being Function of NAT,NAT such that
A18: ( F . 0 = M9 & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A15);
A19: ( dom F = NAT & rng F c= REAL ) by FUNCT_2:def_1, XBOOLE_1:1;
then reconsider F = F as Real_Sequence by RELSET_1:4;
A20: now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_is_Element_of_NAT
let n be Element of NAT ; ::_thesis: F . n is Element of NAT
 ( F . n in rng F & rng F c= NAT ) by A19, FUNCT_1:def_3;
hence  F . n is Element of NAT ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_F_._n_<_F_._(n_+_1)
let n be Element of NAT ; ::_thesis: F . n < F . (n + 1)
 ( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A20;
hence  F . n < F . (n + 1) by A18; ::_thesis: verum
end;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def_6;
A21: for n being Element of NAT st s2 . n <> x0 holds
ex m being Element of NAT st F . m = n
proof
defpred S3[ set ] means ( s2 . $1 <> x0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume  ex n being Element of NAT st S3[n] ; ::_thesis: contradiction
then A22: ex n being Nat st S3[n] ;
consider M1 being Nat such that
A23: ( S3[M1] & ( for n being Nat st S3[n] holds
M1 <= n ) ) from NAT_1:sch_5(A22);
reconsider M1 = M1 as Element of NAT by ORDINAL1:def_12;
defpred S4[ Nat] means ( $1 < M1 & s2 . $1 <> x0 & ex m being Element of NAT st F . m = $1 );
A24: ex n being Nat st S4[n]
proof
take  M ; ::_thesis: S4[M]
 ( M <= M1 & M <> M1 ) by A12, A18, A23;
hence  M < M1 by XXREAL_0:1; ::_thesis: ( s2 . M <> x0 & ex m being Element of NAT st F . m = M )
thus  s2 . M <> x0 by A12; ::_thesis: ex m being Element of NAT st F . m = M
take  0 ; ::_thesis: F . 0 = M
thus  F . 0 = M by A18; ::_thesis: verum
end;
A25: for n being Nat st S4[n] holds
n <= M1 ;
consider MX being Nat such that
A26: ( S4[MX] & ( for n being Nat st S4[n] holds
n <= MX ) ) from NAT_1:sch_6(A25, A24);
consider m being Element of NAT  such that
A27: F . m = MX by A26;
A28: ( F . m is Element of NAT & F . (m + 1) is Element of NAT ) by A20;
then A29: ( MX < F . (m + 1) & s2 . (F . (m + 1)) <> x0 ) by A18, A27;
 ( F . (m + 1) <> M1 & F . (m + 1) <= M1 ) by A18, A23, A26, A27, A28;
then  F . (m + 1) < M1 by XXREAL_0:1;
hence  contradiction by A26, A29; ::_thesis: verum
end;
A30: for n being Element of NAT holds (s2 * F) . n <> x0
proof
defpred S3[ Element of NAT ] means (s2 * F) . $1 <> x0;
A31: for k being Element of NAT st S3[k] holds
S3[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S3[k] implies S3[k + 1] )
assume  (s2 * F) . k <> x0 ; ::_thesis: S3[k + 1]
 ( F . k is Element of NAT & F . (k + 1) is Element of NAT ) by A20;
then  s2 . (F . (k + 1)) <> x0 by A18;
hence  S3[k + 1] by FUNCT_2:15; ::_thesis: verum
end;
A32: S3[ 0 ] by A12, A18, FUNCT_2:15;
thus  for n being Element of NAT holds S3[n] from NAT_1:sch_1(A32, A31); ::_thesis: verum
end;
A33: ( s2 * F is convergent & lim (s2 * F) = x0 ) by A3, SEQ_4:16, SEQ_4:17;
A34: rng (s2 * F) c= rng s2 by VALUED_0:21;
then  rng (s2 * F) c= dom f by A2, XBOOLE_1:1;
then A35: ( f /* (s2 * F) is convergent & f /. x0 = lim (f /* (s2 * F)) ) by A1, A30, A33;
A36: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((f_/*_s2)_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s2) . b5) - (f /. x0)).|| < b3 )
assume A37: 0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s2) . b5) - (f /. x0)).|| < b3
then consider n being Element of NAT  such that
A38: for m being Element of NAT st n <= m holds
||.(((f /* (s2 * F)) . m) - (f /. x0)).|| < p by A35, NORMSP_1:def_7;
reconsider k = F . n as Element of NAT by A20;
take k = k; ::_thesis: for m being Element of NAT st k <= m holds
||.(((f /* s2) . b4) - (f /. x0)).|| < b2
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((f /* s2) . b3) - (f /. x0)).|| < b1 )
assume A39: k <= m ; ::_thesis: ||.(((f /* s2) . b3) - (f /. x0)).|| < b1
percases ( s2 . m = x0 or s2 . m <> x0 ) ;
suppose s2 . m = x0 ; ::_thesis: ||.(((f /* s2) . b3) - (f /. x0)).|| < b1
then ||.(((f /* s2) . m) - (f /. x0)).|| = ||.((f /. x0) - (f /. x0)).|| by A2, FUNCT_2:109
.= 0 by NORMSP_1:6 ;
hence  ||.(((f /* s2) . m) - (f /. x0)).|| < p by A37; ::_thesis: verum
end;
suppose s2 . m <> x0 ; ::_thesis: ||.(((f /* s2) . b3) - (f /. x0)).|| < b1
then consider l being Element of NAT  such that
A40: m = F . l by A21;
 n <= l by A39, A40, SEQM_3:1;
then  ||.(((f /* (s2 * F)) . l) - (f /. x0)).|| < p by A38;
then  ||.((f /. ((s2 * F) . l)) - (f /. x0)).|| < p by A2, A34, FUNCT_2:109, XBOOLE_1:1;
then  ||.((f /. (s2 . m)) - (f /. x0)).|| < p by A40, FUNCT_2:15;
hence  ||.(((f /* s2) . m) - (f /. x0)).|| < p by A2, FUNCT_2:109; ::_thesis: verum
end;
end;
end;
hence  f /* s2 is convergent by NORMSP_1:def_6; ::_thesis: f /. x0 = lim (f /* s2)
hence  f /. x0 = lim (f /* s2) by A36, NORMSP_1:def_7; ::_thesis: verum
end;
end;
end;

theorem Th8: :: NFCONT_3:8
for x0 being real number
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 number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
proof
let x0 be real number ; ::_thesis: 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 number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let S be RealNormSpace; ::_thesis: 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 number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) )
thus  ( f is_continuous_in x0 implies ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) )
hence  x0 in dom f by Def1; ::_thesis: for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
given r being Real such that A2: 0 < r and
A3: for s being real number holds
( not 0 < s or ex x1 being real number st
( x1 in dom f & abs (x1 - x0) < s & not ||.((f /. x1) - (f /. x0)).|| < r ) ) ; ::_thesis: contradiction
defpred S1[ Element of NAT , real number ] means ( $2 in dom f & abs ($2 - x0) < 1 / ($1 + 1) & not ||.((f /. $2) - (f /. x0)).|| < r );
A4: for n being Element of NAT ex p being Real st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Real st S1[n,p]
 0 < (n + 1) " ;
then  0 < 1 / (n + 1) by XCMPLX_1:215;
then consider x1 being real number  such that
A5: ( x1 in dom f & abs (x1 - x0) < 1 / (n + 1) & not ||.((f /. x1) - (f /. x0)).|| < r ) by A3;
take  x1 ; ::_thesis: ( x1 is Real & S1[n,x1] )
thus  ( x1 is Real & S1[n,x1] ) by A5; ::_thesis: verum
end;
consider s1 being Real_Sequence such that
A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A4);
now__::_thesis:_for_x_being_set_st_x_in_rng_s1_holds_
x_in_dom_f
let x be set ; ::_thesis: ( x in rng s1 implies x in dom f )
assume  x in rng s1 ; ::_thesis: x in dom f
then  ex n being Element of NAT st x = s1 . n by FUNCT_2:113;
hence  x in dom f by A6; ::_thesis: verum
end;
then A7: rng s1 c= dom f by TARSKI:def_3;
A8: now__::_thesis:_for_s_being_real_number_st_0_<_s_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
abs_((s1_._m)_-_x0)_<_s
let s be real number ; ::_thesis: ( 0 < s implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s )
assume A9: 0 < s ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s
consider n being Element of NAT  such that
A10: s " < n by SEQ_4:3;
 (s ") + 0 < n + 1 by A10, XREAL_1:8;
then  1 / (n + 1) < 1 / (s ") by A9, XREAL_1:76;
then A11: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
abs ((s1 . m) - x0) < s
let m be Element of NAT ; ::_thesis: ( k <= m implies abs ((s1 . m) - x0) < s )
assume  k <= m ; ::_thesis: abs ((s1 . m) - x0) < s
then  k + 1 <= m + 1 by XREAL_1:6;
then  1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then  1 / (m + 1) < s by A11, XXREAL_0:2;
hence  abs ((s1 . m) - x0) < s by A6, XXREAL_0:2; ::_thesis: verum
end;
then A12: s1 is convergent by SEQ_2:def_6;
then  lim s1 = x0 by A8, SEQ_2:def_7;
then  ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A12, Def1;
then consider n being Element of NAT  such that
A13: for m being Element of NAT st n <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < r by A2, NORMSP_1:def_7;
 ||.(((f /* s1) . n) - (f /. x0)).|| < r by A13;
then  ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A7, FUNCT_2:109;
hence  contradiction by A6; ::_thesis: verum
end;
assume A14: ( x0 in dom f & ( for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_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)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A15: rng s1 c= dom f and
A16: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
A17: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_k_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_k_<=_m_holds_
||.(((f_/*_s1)_._m)_-_(f_/._x0)).||_<_p
let p be Real; ::_thesis: ( 0 < p implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < p )
assume  0 < p ; ::_thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < p
then consider s being real number  such that
A18: 0 < s and
A19: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < p by A14;
consider n being Element of NAT  such that
A20: for m being Element of NAT st n <= m holds
abs ((s1 . m) - x0) < s by A16, A18, SEQ_2:def_7;
take k = n; ::_thesis: for m being Element of NAT st k <= m holds
||.(((f /* s1) . m) - (f /. x0)).|| < p
let m be Element of NAT ; ::_thesis: ( k <= m implies ||.(((f /* s1) . m) - (f /. x0)).|| < p )
assume  k <= m ; ::_thesis: ||.(((f /* s1) . m) - (f /. x0)).|| < p
then  ( s1 . m in rng s1 & abs ((s1 . m) - x0) < s ) by A20, VALUED_0:28;
then  ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A15, A19;
hence  ||.(((f /* s1) . m) - (f /. x0)).|| < p by A15, FUNCT_2:109; ::_thesis: verum
end;
then  f /* s1 is convergent by NORMSP_1:def_6;
hence  ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A17, NORMSP_1:def_7; ::_thesis: verum
end;
hence  f is_continuous_in x0 by A14, Def1; ::_thesis: verum
end;

theorem Th9: :: NFCONT_3:9
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being real number 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 number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
proof
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S
for x0 being real number 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 number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: for x0 being real number 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 number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
let x0 be real number ; ::_thesis: ( 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 number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) )
thus  ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ) ::_thesis: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) )
hence  x0 in dom f by Def1; ::_thesis: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1
let N01 be Neighbourhood of f /. x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
consider r being Real such that
A2: 0 < r and
A3:  {  p where p is Point of S : ||.(p - (f /. x0)).|| < r  }  c= N01 by NFCONT_1:def_1;
set N1 =  {  p where p is Point of S : ||.(p - (f /. x0)).|| < r  }  ;
consider s being real number  such that
A4: 0 < s and
A5: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th8;
reconsider N = ].(x0 - s),(x0 + s).[ as Neighbourhood of x0 by A4, RCOMP_1:def_6;
take  N ; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N01
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N01 )
assume that
A6: x1 in dom f and
A7: x1 in N ; ::_thesis: f /. x1 in N01
 abs (x1 - x0) < s by A7, RCOMP_1:1;
then  ||.((f /. x1) - (f /. x0)).|| < r by A5, A6;
then  f /. x1 in  {  p where p is Point of S : ||.(p - (f /. x0)).|| < r  }  ;
hence  f /. x1 in N01 by A3; ::_thesis: verum
end;
assume A8: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_r_being_Real_st_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_)
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
then reconsider N1 =  {  p where p is Point of S : ||.(p - (f /. x0)).|| < r  }  as Neighbourhood of f /. x0 by NFCONT_1:3;
consider N2 being Neighbourhood of x0 such that
A9: for x1 being real number st x1 in dom f & x1 in N2 holds
f /. x1 in N1 by A8;
consider s being real number  such that
A10: 0 < s and
A11: N2 = ].(x0 - s),(x0 + s).[ by RCOMP_1:def_6;
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
 for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r
proof
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume that
A12: x1 in dom f and
A13: abs (x1 - x0) < s ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
 x1 in N2 by A11, A13, RCOMP_1:1;
then  f /. x1 in N1 by A9, A12;
then  ex p being Point of S st
( p = f /. x1 & ||.(p - (f /. x0)).|| < r ) ;
hence  ||.((f /. x1) - (f /. x0)).|| < r ; ::_thesis: verum
end;
hence  ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) by A10; ::_thesis: verum
end;
hence  f is_continuous_in x0 by A8, Th8; ::_thesis: verum
end;

theorem Th10: :: NFCONT_3:10
for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S
for x0 being real number 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
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S
for x0 being real number 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 ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: for x0 being real number 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 ) ) )
let x0 be real number ; ::_thesis: ( 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 ) ) )
thus  ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) ::_thesis: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 )
proof
assume A1: f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) )
hence  x0 in dom f by Def1; ::_thesis: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1
let N1 be Neighbourhood of f /. x0; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
consider N being Neighbourhood of x0 such that
A2: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1 by A1, Th9;
take  N ; ::_thesis: f .: N c= N1
now__::_thesis:_for_r_being_set_st_r_in_f_.:_N_holds_
r_in_N1
let r be set ; ::_thesis: ( r in f .: N implies r in N1 )
assume  r in f .: N ; ::_thesis: r in N1
then consider x being Element of REAL  such that
A3: ( x in dom f & x in N & r = f . x ) by PARTFUN2:59;
 r = f /. x by A3, PARTFUN1:def_6;
hence  r in N1 by A2, A3; ::_thesis: verum
end;
hence  f .: N c= N1 by TARSKI:def_3; ::_thesis: verum
end;
assume A4: ( x0 in dom f & ( for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ; ::_thesis: f is_continuous_in x0
now__::_thesis:_for_N1_being_Neighbourhood_of_f_/._x0_ex_N_being_Neighbourhood_of_x0_st_
for_x1_being_real_number_st_x1_in_dom_f_&_x1_in_N_holds_
f_/._x1_in_N1
let N1 be Neighbourhood of f /. x0; ::_thesis: ex N being Neighbourhood of x0 st
for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1
consider N being Neighbourhood of x0 such that
A5: f .: N c= N1 by A4;
take N = N; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds
f /. x1 in N1
let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N1 )
assume A6: ( x1 in dom f & x1 in N ) ; ::_thesis: f /. x1 in N1
then  f . x1 in f .: N by FUNCT_1:def_6;
then  f /. x1 in f .: N by A6, PARTFUN1:def_6;
hence  f /. x1 in N1 by A5; ::_thesis: verum
end;
hence  f is_continuous_in x0 by A4, Th9; ::_thesis: verum
end;

theorem :: NFCONT_3:11
for x0 being real number
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
let x0 be real number ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 )
given N being Neighbourhood of x0 such that A1: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0
 x0 in (dom f) /\ N by A1, TARSKI:def_1;
then A2: x0 in dom f by XBOOLE_0:def_4;
now__::_thesis:_for_N1_being_Neighbourhood_of_f_/._x0_ex_N_being_Neighbourhood_of_x0_st_f_.:_N_c=_N1
let N1 be Neighbourhood of f /. x0; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1
take N = N; ::_thesis: f .: N c= N1
A3: f /. x0 in N1 by NFCONT_1:4;
f .: N = Im (f,x0) by A1, RELAT_1:112
.= {(f . x0)} by A2, FUNCT_1:59
.= {(f /. x0)} by A2, PARTFUN1:def_6 ;
hence  f .: N c= N1 by A3, ZFMISC_1:31; ::_thesis: verum
end;
hence  f is_continuous_in x0 by Th10, A2; ::_thesis: verum
end;

theorem :: NFCONT_3:12
for x0 being real number
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
let x0 be real number ; ::_thesis: 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 )
let S be RealNormSpace; ::_thesis: 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 )
let f1, f2 be PartFunc of REAL, the carrier of S; ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) )
assume A1: x0 in (dom f1) /\ (dom f2) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in x0 or ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) )
assume A2: ( f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 )
A3: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
A4: x0 in dom (f1 + f2) by A1, VFUNCT_1:def_1;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._x0_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 = x0 implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) ) )
assume that
A5: rng s1 c= dom (f1 + f2) and
A6: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) )
A7: rng s1 c= (dom f1) /\ (dom f2) by A5, VFUNCT_1:def_1;
 ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by A3, XBOOLE_1:17;
then A8: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A5, XBOOLE_1:1;
then A9: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A2, A6, Def1;
then  (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:19;
hence  (f1 + f2) /* s1 is convergent by A7, Th2; ::_thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1)
A10: ( f1 /. x0 = lim (f1 /* s1) & f2 /. x0 = lim (f2 /* s1) ) by A2, A6, A8, Def1;
thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by A4, VFUNCT_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A9, A10, NORMSP_1:25
.= lim ((f1 + f2) /* s1) by A7, Th2 ; ::_thesis: verum
end;
hence  f1 + f2 is_continuous_in x0 by A4, Def1; ::_thesis: f1 - f2 is_continuous_in x0
A11: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
A12: x0 in dom (f1 - f2) by A1, VFUNCT_1:def_2;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_=_x0_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._x0_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 = x0 implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) )
assume that
A13: rng s1 c= dom (f1 - f2) and
A14: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) )
A15: rng s1 c= (dom f1) /\ (dom f2) by A13, VFUNCT_1:def_2;
 ( dom (f1 - f2) c= dom f1 & dom (f1 - f2) c= dom f2 ) by A11, XBOOLE_1:17;
then A16: ( rng s1 c= dom f1 & rng s1 c= dom f2 ) by A13, XBOOLE_1:1;
then A17: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A2, A14, Def1;
then  (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:20;
hence  (f1 - f2) /* s1 is convergent by A15, Th2; ::_thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1)
A18: ( f1 /. x0 = lim (f1 /* s1) & f2 /. x0 = lim (f2 /* s1) ) by A2, A14, A16, Def1;
thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by A12, VFUNCT_1:def_2
.= lim ((f1 /* s1) - (f2 /* s1)) by A18, A17, NORMSP_1:26
.= lim ((f1 - f2) /* s1) by A15, Th2 ; ::_thesis: verum
end;
hence  f1 - f2 is_continuous_in x0 by A12, Def1; ::_thesis: verum
end;

theorem Th13: :: NFCONT_3:13
for r being Real
for x0 being real number
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
let r be Real; ::_thesis: for x0 being real number
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
let x0 be real number ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S st f is_continuous_in x0 holds
r (#) f is_continuous_in x0
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is_continuous_in x0 implies r (#) f is_continuous_in x0 )
assume A1: f is_continuous_in x0 ; ::_thesis: r (#) f is_continuous_in x0
then  x0 in dom f by Def1;
hence A2: x0 in dom (r (#) f) by VFUNCT_1:def_4; :: according to NFCONT_3:def_1 ::_thesis: for s1 being Real_Sequence st rng s1 c= dom (r (#) f) & s1 is convergent & lim s1 = x0 holds
( (r (#) f) /* s1 is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* s1) )
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (r (#) f) & s1 is convergent & lim s1 = x0 implies ( (r (#) f) /* s1 is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom (r (#) f) and
A4: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. x0 = lim ((r (#) f) /* s1) )
A5: rng s1 c= dom f by A3, VFUNCT_1:def_4;
then A6: f /. x0 = lim (f /* s1) by A1, A4, Def1;
A7: f /* s1 is convergent by A1, A4, A5, Def1;
then  r * (f /* s1) is convergent by NORMSP_1:22;
hence  (r (#) f) /* s1 is convergent by A5, Th4; ::_thesis: (r (#) f) /. x0 = lim ((r (#) f) /* s1)
thus (r (#) f) /. x0 = r * (f /. x0) by A2, VFUNCT_1:def_4
.= lim (r * (f /* s1)) by A7, A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A5, Th4 ; ::_thesis: verum
end;

theorem :: NFCONT_3:14
for x0 being real number
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
let x0 be real number ; ::_thesis: 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 )
let S be RealNormSpace; ::_thesis: 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 )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A1: x0 in dom f ; ::_thesis: ( not f is_continuous_in x0 or ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) )
assume A2: f is_continuous_in x0 ; ::_thesis: ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 )
A3: x0 in dom ||.f.|| by A1, NORMSP_0:def_3;
now__::_thesis:_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)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom ||.f.|| & s1 is convergent & lim s1 = x0 implies ( ||.f.|| /* s1 is convergent & ||.f.|| . x0 = lim (||.f.|| /* s1) ) )
assume that
A4: rng s1 c= dom ||.f.|| and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( ||.f.|| /* s1 is convergent & ||.f.|| . x0 = lim (||.f.|| /* s1) )
A6: rng s1 c= dom f by A4, NORMSP_0:def_3;
then A7: f /. x0 = lim (f /* s1) by A2, A5, Def1;
A8: f /* s1 is convergent by A2, A5, A6, Def1;
then  ||.(f /* s1).|| is convergent by NORMSP_1:23;
hence  ||.f.|| /* s1 is convergent by A6, Th5; ::_thesis: ||.f.|| . x0 = lim (||.f.|| /* s1)
thus ||.f.|| . x0 = ||.(f /. x0).|| by A3, NORMSP_0:def_3
.= lim ||.(f /* s1).|| by A8, A7, LOPBAN_1:20
.= lim (||.f.|| /* s1) by A6, Th5 ; ::_thesis: verum
end;
hence  ||.f.|| is_continuous_in x0 by FCONT_1:def_1; ::_thesis: - f is_continuous_in x0
 (- 1) (#) f is_continuous_in x0 by A2, Th13;
hence  - f is_continuous_in x0 by VFUNCT_1:23; ::_thesis: verum
end;

theorem :: NFCONT_3:15
for x0 being real number
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
let x0 be real number ; ::_thesis: 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
let S, T be RealNormSpace; ::_thesis: 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
let f1 be PartFunc of REAL, the carrier of S; ::_thesis: 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
let f2 be PartFunc of the carrier of S, the carrier of T; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 )
assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 )
assume that
A2: f1 is_continuous_in x0 and
A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0
thus  x0 in dom (f2 * f1) by A1; :: according to NFCONT_3:def_1 ::_thesis: for s1 being Real_Sequence st rng s1 c= dom (f2 * f1) & s1 is convergent & lim s1 = x0 holds
( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f2 * f1) & s1 is convergent & lim s1 = x0 implies ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) )
assume that
A4: rng s1 c= dom (f2 * f1) and
A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) )
A6: dom (f2 * f1) c= dom f1 by RELAT_1:25;
now__::_thesis:_for_x_being_set_st_x_in_rng_(f1_/*_s1)_holds_
x_in_dom_f2
let x be set ; ::_thesis: ( x in rng (f1 /* s1) implies x in dom f2 )
assume  x in rng (f1 /* s1) ; ::_thesis: x in dom f2
then consider n being Element of NAT  such that
A7: x = (f1 /* s1) . n by FUNCT_2:113;
 s1 . n in rng s1 by VALUED_0:28;
then  f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11;
hence  x in dom f2 by A4, A6, A7, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum
end;
then A8: rng (f1 /* s1) c= dom f2 by TARSKI:def_3;
A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n
let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n
 s1 . n in rng s1 by VALUED_0:28;
then A10: s1 . n in dom f1 by A4, FUNCT_1:11;
thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108
.= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13
.= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1
.= (f2 /* (f1 /* s1)) . n by A8, FUNCT_2:108 ; ::_thesis: verum
end;
then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63;
 rng s1 c= dom f1 by A4, A6, XBOOLE_1:1;
then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, Def1;
(f2 * f1) /. x0 = f2 /. (f1 /. x0) by A1, PARTFUN2:3
.= lim (f2 /* (f1 /* s1)) by A12, A3, A8, NFCONT_1:def_5
.= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ;
hence  ( (f2 * f1) /* s1 is convergent & (f2 * f1) /. x0 = lim ((f2 * f1) /* s1) ) by A3, A12, A8, A11, NFCONT_1:def_5; ::_thesis: verum
end;

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
attrf is continuous  means :Def2: :: NFCONT_3:def 2
 for x0 being real number st x0 in dom f holds
f is_continuous_in x0;
end;

:: 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 number 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) ) )
proof
let S be RealNormSpace; ::_thesis: 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) ) )
let X be set ; ::_thesis: 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) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= dom f implies ( 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) ) ) )
assume A1: X c= dom f ; ::_thesis: ( 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) ) )
thus  ( f | X is continuous implies 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) ) ) ::_thesis: ( ( 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) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: 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) )
hereby  ::_thesis: verum
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) )
assume that
A3: rng s1 c= X and
A4: s1 is convergent and
A5: lim s1 in X ; ::_thesis: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) )
A6: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then A7: f | X is_continuous_in lim s1 by A2, A5, Def2;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A8: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A3, A6, FUNCT_2:109
.= f /. (s1 . n) by A3, A6, A8, PARTFUN2:15
.= (f /* s1) . n by A1, A3, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
then A9: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
f /. (lim s1) = (f | X) /. (lim s1) by A5, A6, PARTFUN2:15
.= lim (f /* s1) by A3, A4, A6, A7, A9, Def1 ;
hence  ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A6, A7, A9, Def1; ::_thesis: verum
end;
end;
assume A10: 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) ) ; ::_thesis: f | X is continuous
now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x1
A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) implies f | X is_continuous_in x1 )
assume A12: x1 in dom (f | X) ; ::_thesis: f | X is_continuous_in x1
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f_|_X)_&_s1_is_convergent_&_lim_s1_=_x1_holds_
(_(f_|_X)_/*_s1_is_convergent_&_(f_|_X)_/._x1_=_lim_((f_|_X)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = x1 implies ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) )
assume that
A13: rng s1 c= dom (f | X) and
A14: s1 is convergent and
A15: lim s1 = x1 ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) )
now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_(f_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = (f /* s1) . n
A16: s1 . n in rng s1 by VALUED_0:28;
thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A13, FUNCT_2:109
.= f /. (s1 . n) by A13, A16, PARTFUN2:15
.= (f /* s1) . n by A1, A11, A13, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum
end;
then A17: (f | X) /* s1 = f /* s1 by FUNCT_2:63;
(f | X) /. (lim s1) = f /. (lim s1) by A12, A15, PARTFUN2:15
.= lim ((f | X) /* s1) by A10, A12, A11, A13, A14, A15, A17 ;
hence  ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A10, A12, A11, A13, A14, A15, A17; ::_thesis: verum
end;
hence  f | X is_continuous_in x1 by Def1, A12; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
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 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
proof
let X be set ; ::_thesis: 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 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S st X c= dom f holds
( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= dom f implies ( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) )
assume A1: X c= dom f ; ::_thesis: ( f | X is continuous iff for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
thus  ( f | X is continuous implies for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) ::_thesis: ( ( for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ) implies f | X is continuous )
proof
assume A2: f | X is continuous ; ::_thesis: for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let x0 be real number ; ::_thesis: for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume that
A3: x0 in X and
A4: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
 x0 in dom (f | X) by A1, A3, RELAT_1:62;
then  f | X is_continuous_in x0 by A2, Def2;
then consider s being real number  such that
A5: 0 < s and
A6: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r by A4, Th8;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus  0 < s by A5; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume that
A7: x1 in X and
A8: abs (x1 - x0) < s ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
A9: x0 in REAL by XREAL_0:def_1;
A10: x1 in REAL by XREAL_0:def_1;
A11: dom (f | X) = (dom f) /\ X by RELAT_1:61
.= X by A1, XBOOLE_1:28 ;
then ||.((f /. x1) - (f /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A7, PARTFUN2:15, A10
.= ||.(((f | X) /. x1) - ((f | X) /. x0)).|| by A3, A11, PARTFUN2:15, A9 ;
hence  ||.((f /. x1) - (f /. x0)).|| < r by A6, A11, A7, A8; ::_thesis: verum
end;
assume A12: for x0 being real number
for r being Real st x0 in X & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) ; ::_thesis: f | X is continuous
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A13: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then A14: x0 in X ;
 for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) )
proof
let r be Real; ::_thesis: ( 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) )
assume  0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) )
then consider s being real number  such that
A15: 0 < s and
A16: for x1 being real number st x1 in X & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r by A12, A14;
take  s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) )
thus  0 < s by A15; ::_thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds
||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r
let x1 be real number ; ::_thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r )
assume that
A17: x1 in dom (f | X) and
A18: abs (x1 - x0) < s ; ::_thesis: ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r
A19: x0 in REAL by XREAL_0:def_1;
A20: x1 in REAL by XREAL_0:def_1;
||.(((f | X) /. x1) - ((f | X) /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A13, PARTFUN2:15, A19
.= ||.((f /. x1) - (f /. x0)).|| by A17, PARTFUN2:15, A20 ;
hence  ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r by A16, A17, A18; ::_thesis: verum
end;
hence  f | X is_continuous_in x0 by Th8, A13; ::_thesis: verum
end;
hence  f | X is continuous by Def2; ::_thesis: verum
end;

registration
let S be RealNormSpace;
cluster Function-like constant  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is constant holds
b1 is continuous
proof
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is constant implies f is continuous )
assume A1: f is constant ; ::_thesis: f is continuous
now__::_thesis:_for_x0_being_real_number_
for_r_being_Real_st_x0_in_dom_f_&_0_<_r_holds_
ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_)
reconsider s = 1 as real number ;
let x0 be real number ; ::_thesis: for r being Real st x0 in dom f & 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
let r be Real; ::_thesis: ( x0 in dom f & 0 < r implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) ) )
assume that
A2: x0 in dom f and
A3: 0 < r ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
thus  0 < s ; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume A4: x1 in dom f ; ::_thesis: ( abs (x1 - x0) < s implies ||.((f /. x1) - (f /. x0)).|| < r )
assume  abs (x1 - x0) < s ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r
f /. x1 = f . x1 by A4, PARTFUN1:def_6
.= f . x0 by A1, A2, A4, FUNCT_1:def_10
.= f /. x0 by A2, PARTFUN1:def_6 ;
hence  ||.((f /. x1) - (f /. x0)).|| < r by A3, NORMSP_1:6; ::_thesis: verum
end;
then  f | (dom f) is continuous by Th17;
hence  f is continuous ; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
cluster Relation-like REAL -defined the carrier of S -valued Function-like continuous for Element of bool [:REAL, the carrier of S:];
existence
 ex b1 being PartFunc of REAL, the carrier of S st b1 is continuous
proof
set f = the constant PartFunc of REAL, the carrier of S;
take  the constant PartFunc of REAL, the carrier of S ; ::_thesis: the constant PartFunc of REAL, the carrier of S is continuous
thus  the constant PartFunc of REAL, the carrier of S is continuous ; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
let f be continuous PartFunc of REAL, the carrier of S;
let X be set ;
clusterf | X ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous
proof
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 )
assume A1: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0
then  x0 in dom f by RELAT_1:57;
then A2: f is_continuous_in x0 by Def2;
 x0 in X by A1;
hence  f | X is_continuous_in x0 by A2, Th6; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous by Def2; ::_thesis: verum
end;
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
proof
let X, X1 be set ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S st f | X is continuous & X1 c= X holds
f | X1 is continuous
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous )
assume A1: f | X is continuous ; ::_thesis: ( not X1 c= X or f | X1 is continuous )
assume  X1 c= X ; ::_thesis: f | X1 is continuous
then  f | X1 = (f | X) | X1 by RELAT_1:74;
hence  f | X1 is continuous by A1; ::_thesis: verum
end;

registration
let S be RealNormSpace;
cluster empty Function-like  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is empty holds
b1 is continuous ;
end;

registration
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
let X be trivial set ;
clusterf | X ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous
proof
now__::_thesis:_(_not_f_|_X_is_empty_implies_for_b1_being_PartFunc_of_REAL,_the_carrier_of_S_st_b1_=_f_|_X_holds_
b1_is_continuous_)
assume  not f | X is empty ; ::_thesis: for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous
then consider x0 being real number  such that
A1: x0 in dom (f | X) by MEMBERED:9;
 x0 in X by A1, RELAT_1:57;
then A2: X = {x0} by ZFMISC_1:132;
now__::_thesis:_for_p_being_real_number_st_p_in_dom_(f_|_X)_holds_
f_|_X_is_continuous_in_p
let p be real number ; ::_thesis: ( p in dom (f | X) implies f | X is_continuous_in p )
assume A3: p in dom (f | X) ; ::_thesis: f | X is_continuous_in p
then A4: p in {x0} by A2;
thus  f | X is_continuous_in p ::_thesis: verum
proof
thus  p in dom (f | X) by A3; :: according to NFCONT_3:def_1 ::_thesis: for s1 being Real_Sequence st rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p holds
( (f | X) /* s1 is convergent & (f | X) /. p = lim ((f | X) /* s1) )
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f | X) & s1 is convergent & lim s1 = p implies ( (f | X) /* s1 is convergent & (f | X) /. p = lim ((f | X) /* s1) ) )
assume that
A5: rng s1 c= dom (f | X) and
 s1 is convergent and
 lim s1 = p ; ::_thesis: ( (f | X) /* s1 is convergent & (f | X) /. p = lim ((f | X) /* s1) )
A6: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17;
 rng s1 c= (dom f) /\ {x0} by A2, A5, RELAT_1:61;
then A7: rng s1 c= {x0} by A6, XBOOLE_1:1;
A8: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_x0
let n be Element of NAT ; ::_thesis: s1 . n = x0
 s1 . n in rng s1 by VALUED_0:28;
hence  s1 . n = x0 by A7, TARSKI:def_1; ::_thesis: verum
end;
A9: p = x0 by A4, TARSKI:def_1;
A10: now__::_thesis:_for_g_being_Real_st_0_<_g_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
||.((((f_|_{x0})_/*_s1)_._m)_-_((f_|_{x0})_/._p)).||_<_g
let g be Real; ::_thesis: ( 0 < g implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g )
assume A11: 0 < g ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
let m be Element of NAT ; ::_thesis: ( n <= m implies ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g )
assume  n <= m ; ::_thesis: ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g
||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| = ||.(((f | {x0}) /. (s1 . m)) - ((f | {x0}) /. x0)).|| by A2, A9, A5, FUNCT_2:109
.= ||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| by A8
.= 0 by NORMSP_1:6 ;
hence  ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g by A11; ::_thesis: verum
end;
hence  (f | X) /* s1 is convergent by A2, NORMSP_1:def_6; ::_thesis: (f | X) /. p = lim ((f | X) /* s1)
hence  lim ((f | X) /* s1) = (f | X) /. p by A2, A10, NORMSP_1:def_7; ::_thesis: verum
end;
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous by Def2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is continuous ; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
let f1, f2 be continuous PartFunc of REAL, the carrier of S;
clusterf1 + f2 ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is continuous
proof
set X = dom (f1 + f2);
 dom (f1 + f2) c= (dom f1) /\ (dom f2) by VFUNCT_1:def_1;
then A1: ( dom (f1 + f2) c= dom f1 & dom (f1 + f2) c= dom f2 ) by XBOOLE_1:18;
A2: ( f1 | (dom (f1 + f2)) is continuous & f2 | (dom (f1 + f2)) is continuous ) ;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_+_f2)_&_s1_is_convergent_&_lim_s1_in_dom_(f1_+_f2)_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 + f2) & s1 is convergent & lim s1 in dom (f1 + f2) implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A3: rng s1 c= dom (f1 + f2) and
A4: s1 is convergent and
A5: lim s1 in dom (f1 + f2) ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
A6: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A2, A3, A4, A5, Th16;
then A7: (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:19;
A8: rng s1 c= (dom f1) /\ (dom f2) by A3, VFUNCT_1:def_1;
 ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A2, A3, A4, A5, Th16;
then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A5, VFUNCT_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A6, NORMSP_1:25
.= lim ((f1 + f2) /* s1) by A8, Th2 ;
hence  ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A8, A7, Th2; ::_thesis: verum
end;
then  (f1 + f2) | (dom (f1 + f2)) is continuous by Th16;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is continuous ; ::_thesis: verum
end;
clusterf1 - f2 ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is continuous
proof
set X = dom (f1 - f2);
 dom (f1 - f2) c= (dom f1) /\ (dom f2) by VFUNCT_1:def_2;
then A9: ( dom (f1 - f2) c= dom f1 & dom (f1 - f2) c= dom f2 ) by XBOOLE_1:18;
A10: ( f1 | (dom (f1 - f2)) is continuous & f2 | (dom (f1 - f2)) is continuous ) ;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_(f1_-_f2)_&_s1_is_convergent_&_lim_s1_in_dom_(f1_-_f2)_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom (f1 - f2) & s1 is convergent & lim s1 in dom (f1 - f2) implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A11: rng s1 c= dom (f1 - f2) and
A12: s1 is convergent and
A13: lim s1 in dom (f1 - f2) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A9, A10, A11, A12, A13, Th16;
then A15: (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:20;
A16: rng s1 c= (dom f1) /\ (dom f2) by A11, VFUNCT_1:def_2;
 ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A9, A10, A11, A12, A13, Th16;
then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A13, VFUNCT_1:def_2
.= lim ((f1 /* s1) - (f2 /* s1)) by A14, NORMSP_1:26
.= lim ((f1 - f2) /* s1) by A16, Th2 ;
hence  ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A16, A15, Th2; ::_thesis: verum
end;
then  (f1 - f2) | (dom (f1 - f2)) is continuous by Th16;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is continuous ; ::_thesis: verum
end;
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 )
proof
let S be RealNormSpace; ::_thesis: 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 )
let X be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) )
assume that
A1: X c= (dom f1) /\ (dom f2) and
A2: ( f1 | X is continuous & f2 | X is continuous ) ; ::_thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous )
A3: ( X c= dom f1 & X c= dom f2 ) by A1, XBOOLE_1:18;
A4: ( X c= dom (f1 + f2) & X c= dom (f1 - f2) ) by A1, VFUNCT_1:def_1, VFUNCT_1:def_2;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_+_f2)_/*_s1_is_convergent_&_(f1_+_f2)_/._(lim_s1)_=_lim_((f1_+_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) )
assume that
A5: ( rng s1 c= X & s1 is convergent ) and
A6: lim s1 in X ; ::_thesis: ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) )
A7: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A5, A6, Th16;
then A8: (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:19;
A9: rng s1 c= (dom f1) /\ (dom f2) by A1, A5, XBOOLE_1:1;
 ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A3, A2, A5, A6, Th16;
then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A4, A6, VFUNCT_1:def_1
.= lim ((f1 /* s1) + (f2 /* s1)) by A7, NORMSP_1:25
.= lim ((f1 + f2) /* s1) by A9, Th2 ;
hence  ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th2; ::_thesis: verum
end;
hence  (f1 + f2) | X is continuous by A4, Th16; ::_thesis: (f1 - f2) | X is continuous
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(f1_-_f2)_/*_s1_is_convergent_&_(f1_-_f2)_/._(lim_s1)_=_lim_((f1_-_f2)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) )
assume that
A10: ( rng s1 c= X & s1 is convergent ) and
A11: lim s1 in X ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) )
A12: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A3, A2, A10, A11, Th16;
then A13: (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:20;
A14: rng s1 c= (dom f1) /\ (dom f2) by A1, A10, XBOOLE_1:1;
 ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A3, A2, A10, A11, Th16;
then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A4, A11, VFUNCT_1:def_2
.= lim ((f1 /* s1) - (f2 /* s1)) by A12, NORMSP_1:26
.= lim ((f1 - f2) /* s1) by A14, Th2 ;
hence  ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A14, A13, Th2; ::_thesis: verum
end;
hence  (f1 - f2) | X is continuous by A4, Th16; ::_thesis: verum
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 )
proof
let S be RealNormSpace; ::_thesis: 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 )
let X, X1 be set ; ::_thesis: 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 )
let f1, f2 be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
assume  ( X c= dom f1 & X1 c= dom f2 ) ; ::_thesis: ( not f1 | X is continuous or not f2 | X1 is continuous or ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) )
then A1: X /\ X1 c= (dom f1) /\ (dom f2) by XBOOLE_1:27;
assume  ( f1 | X is continuous & f2 | X1 is continuous ) ; ::_thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous )
then  ( f1 | (X /\ X1) is continuous & f2 | (X /\ X1) is continuous ) by Th18, XBOOLE_1:17;
hence  ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) by A1, Th19; ::_thesis: verum
end;

registration
let S be RealNormSpace;
let f be continuous PartFunc of REAL, the carrier of S;
let r be Real;
clusterr (#) f ->  continuous for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = r (#) f holds
b1 is continuous
proof
set X = dom f;
A1: dom f = dom (r (#) f) by VFUNCT_1:def_4;
then A2: (r (#) f) | (dom f) = r (#) f by RELAT_1:69;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_in_dom_f_holds_
(_(r_(#)_f)_/*_s1_is_convergent_&_(r_(#)_f)_/._(lim_s1)_=_lim_((r_(#)_f)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 in dom f implies ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) )
assume that
A3: rng s1 c= dom f and
A4: s1 is convergent and
A5: lim s1 in dom f ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )
 f | (dom f) is continuous ;
then A6: ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A5, Th16;
then A7: r * (f /* s1) is convergent by NORMSP_1:22;
(r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A1, A5, A6, VFUNCT_1:def_4
.= lim (r * (f /* s1)) by A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A3, Th4 ;
hence  ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A3, A7, Th4; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = r (#) f holds
b1 is continuous by A1, A2, Th16; ::_thesis: verum
end;
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
proof
let X be set ; ::_thesis: 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
let r be Real; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous )
assume that
A1: X c= dom f and
A2: f | X is continuous ; ::_thesis: (r (#) f) | X is continuous
A3: X c= dom (r (#) f) by A1, VFUNCT_1:def_4;
now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_
(_(r_(#)_f)_/*_s1_is_convergent_&_(r_(#)_f)_/._(lim_s1)_=_lim_((r_(#)_f)_/*_s1)_)
let s1 be Real_Sequence; ::_thesis: ( rng s1 c= X & s1 is convergent & lim s1 in X implies ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) )
assume that
A4: ( rng s1 c= X & s1 is convergent ) and
A5: lim s1 in X ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) )
A6: f /* s1 is convergent by A1, A2, A4, A5, Th16;
then A7: r * (f /* s1) is convergent by NORMSP_1:22;
 f /. (lim s1) = lim (f /* s1) by A1, A2, A4, A5, Th16;
then (r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A3, A5, VFUNCT_1:def_4
.= lim (r * (f /* s1)) by A6, NORMSP_1:28
.= lim ((r (#) f) /* s1) by A1, A4, Th4, XBOOLE_1:1 ;
hence  ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A1, A4, A7, Th4, XBOOLE_1:1; ::_thesis: verum
end;
hence  (r (#) f) | X is continuous by A3, Th16; ::_thesis: verum
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 )
proof
let X be set ; ::_thesis: 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 )
let S be RealNormSpace; ::_thesis: 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 )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( X c= dom f & f | X is continuous implies ( ||.f.|| | X is continuous & (- f) | X is continuous ) )
assume that
A1: X c= dom f and
A2: f | X is continuous ; ::_thesis: ( ||.f.|| | X is continuous & (- f) | X is continuous )
thus  ||.f.|| | X is continuous ::_thesis: (- f) | X is continuous
proof
let r be real number ; :: according to FCONT_1:def_2 ::_thesis: ( not r in dom (||.f.|| | X) or ||.f.|| | X is_continuous_in r )
assume A3: r in dom (||.f.|| | X) ; ::_thesis: ||.f.|| | X is_continuous_in r
then A4: ( r in dom ||.f.|| & r in X ) by RELAT_1:57;
then  r in dom f by NORMSP_0:def_3;
then A5: r in dom (f | X) by A4, RELAT_1:57;
then A6: f | X is_continuous_in r by A2, Def2;
thus  ||.f.|| | X is_continuous_in r ::_thesis: verum
proof
let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( not rng s1 c= dom (||.f.|| | X) or not s1 is convergent or not lim s1 = r or ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) ) )
assume that
A7: rng s1 c= dom (||.f.|| | X) and
A8: ( s1 is convergent & lim s1 = r ) ; ::_thesis: ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) )
 rng s1 c= (dom ||.f.||) /\ X by A7, RELAT_1:61;
then  rng s1 c= (dom f) /\ X by NORMSP_0:def_3;
then A9: rng s1 c= dom (f | X) by RELAT_1:61;
now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((f_|_X)_/*_s1).||_._n_=_((||.f.||_|_X)_/*_s1)_._n
let n be Element of NAT ; ::_thesis: ||.((f | X) /* s1).|| . n = ((||.f.|| | X) /* s1) . n
A10: s1 . n in rng s1 by VALUED_0:28;
then  s1 . n in dom (f | X) by A9;
then  s1 . n in (dom f) /\ X by RELAT_1:61;
then A11: ( s1 . n in X & s1 . n in dom f ) by XBOOLE_0:def_4;
then A12: s1 . n in dom ||.f.|| by NORMSP_0:def_3;
thus ||.((f | X) /* s1).|| . n = ||.(((f | X) /* s1) . n).|| by NORMSP_0:def_4
.= ||.((f | X) /. (s1 . n)).|| by A9, FUNCT_2:109
.= ||.(f /. (s1 . n)).|| by A9, A10, PARTFUN2:15
.= ||.f.|| . (s1 . n) by A12, NORMSP_0:def_3
.= (||.f.|| | X) . (s1 . n) by A11, FUNCT_1:49
.= ((||.f.|| | X) /* s1) . n by A7, FUNCT_2:108 ; ::_thesis: verum
end;
then A13: ||.((f | X) /* s1).|| = (||.f.|| | X) /* s1 by FUNCT_2:63;
 r in REAL by XREAL_0:def_1;
then A14: ||.((f | X) /. r).|| = ||.(f /. r).|| by A5, PARTFUN2:15
.= ||.f.|| . r by A4, NORMSP_0:def_3
.= (||.f.|| | X) . r by A3, FUNCT_1:47 ;
A15: (f | X) /* s1 is convergent by A6, A8, A9, Def1;
hence  (||.f.|| | X) /* s1 is convergent by A13, NORMSP_1:23; ::_thesis: (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1)
 (f | X) /. r = lim ((f | X) /* s1) by A6, A8, A9, Def1;
hence  (||.f.|| | X) . r = lim ((||.f.|| | X) /* s1) by A15, A13, A14, LOPBAN_1:20; ::_thesis: verum
end;
end;
 ((- 1) (#) f) | X is continuous by A1, A2, Th21;
hence  (- f) | X is continuous by VFUNCT_1:23; ::_thesis: verum
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 number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
proof
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds
f | REAL is continuous
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous )
assume that
A1: f is total and
A2: for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ; ::_thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous )
A3: dom f = REAL by A1, PARTFUN1:def_2;
given x0 being real number  such that A4: f is_continuous_in x0 ; ::_thesis: f | REAL is continuous
reconsider z0 = 0 as real number ;
 (f /. z0) + (f /. z0) = f /. (z0 + z0) by A2;
then  (f /. z0) + ((f /. z0) - (f /. z0)) = (f /. z0) - (f /. z0) by RLVECT_1:28;
then  (f /. z0) + (0. S) = (f /. z0) - (f /. z0) by RLVECT_1:15;
then A5: (f /. z0) + (0. S) = 0. S by RLVECT_1:15;
A6: now__::_thesis:_for_x1_being_real_number_holds_-_(f_/._x1)_=_f_/._(-_x1)
let x1 be real number ; ::_thesis: - (f /. x1) = f /. (- x1)
 0. S = f /. (x1 + (- x1)) by A5, RLVECT_1:4;
then  0. S = (f /. x1) + (f /. (- x1)) by A2;
hence  - (f /. x1) = f /. (- x1) by RLVECT_1:def_10; ::_thesis: verum
end;
A7: now__::_thesis:_for_x1,_x2_being_real_number_holds_f_/._(x1_-_x2)_=_(f_/._x1)_-_(f_/._x2)
let x1, x2 be real number ; ::_thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
 f /. (x1 - x2) = f /. (x1 + (- x2)) ;
then  f /. (x1 - x2) = (f /. x1) + (f /. (- x2)) by A2;
hence  f /. (x1 - x2) = (f /. x1) - (f /. x2) by A6; ::_thesis: verum
end;
now__::_thesis:_for_x1_being_real_number_
for_r_being_Real_st_x1_in_REAL_&_r_>_0_holds_
ex_s_being_real_number_st_
(_s_>_0_&_(_for_x2_being_real_number_st_x2_in_REAL_&_abs_(x2_-_x1)_<_s_holds_
||.((f_/._x2)_-_(f_/._x1)).||_<_r_)_)
let x1 be real number ; ::_thesis: for r being Real st x1 in REAL & r > 0 holds
ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
let r be Real; ::_thesis: ( x1 in REAL & r > 0 implies ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
||.((f /. x2) - (f /. x1)).|| < r ) ) )
assume that
 x1 in REAL and
A8: r > 0 ; ::_thesis: ex s being real number st
( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
set y = x1 - x0;
consider s being real number  such that
A9: 0 < s and
A10: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th8;
take s = s; ::_thesis: ( s > 0 & ( for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
thus  s > 0 by A9; ::_thesis: for x2 being real number st x2 in REAL & abs (x2 - x1) < s holds
||.((f /. x2) - (f /. x1)).|| < r
let x2 be real number ; ::_thesis: ( x2 in REAL & abs (x2 - x1) < s implies ||.((f /. x2) - (f /. x1)).|| < r )
assume that
 x2 in REAL and
A11: abs (x2 - x1) < s ; ::_thesis: ||.((f /. x2) - (f /. x1)).|| < r
A12: ( x2 - (x1 - x0) is Real & abs ((x2 - (x1 - x0)) - x0) = abs (x2 - x1) ) by XREAL_0:def_1;
 (x1 - x0) + x0 = x1 ;
then ||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).|| by A2
.= ||.(((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, A12; ::_thesis: verum
end;
hence  f | REAL is continuous by A3, Th17; ::_thesis: verum
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
proof
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( dom f is compact & f | (dom f) is continuous implies rng f is compact )
assume that
A1: dom f is compact and
A2: f | (dom f) is continuous ; ::_thesis: rng f is compact
now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_rng_f_holds_
ex_q2_being_Element_of_bool_[:NAT,_the_carrier_of_S:]_st_
(_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_)
let s1 be sequence of S; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of bool [:NAT, the carrier of S:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) )
assume A3: rng s1 c= rng f ; ::_thesis: ex q2 being Element of bool [:NAT, the carrier of S:] st
( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
defpred S1[ set , set ] means ( $2 in dom f & f /. $2 = s1 . $1 );
A4: for n being Element of NAT ex p being Real st S1[n,p]
proof
let n be Element of NAT ; ::_thesis: ex p being Real st S1[n,p]
 dom s1 = NAT by FUNCT_2:def_1;
then  s1 . n in rng s1 by FUNCT_1:3;
then consider p being Real such that
A5: ( p in dom f & s1 . n = f . p ) by A3, PARTFUN1:3;
take  p ; ::_thesis: S1[n,p]
thus  S1[n,p] by A5, PARTFUN1:def_6; ::_thesis: verum
end;
consider q1 being Real_Sequence such that
A6: for n being Element of NAT holds S1[n,q1 . n] from FUNCT_2:sch_3(A4);
now__::_thesis:_for_x_being_set_st_x_in_rng_q1_holds_
x_in_dom_f
let x be set ; ::_thesis: ( x in rng q1 implies x in dom f )
assume  x in rng q1 ; ::_thesis: x in dom f
then  ex n being Element of NAT st x = q1 . n by FUNCT_2:113;
hence  x in dom f by A6; ::_thesis: verum
end;
then A7: rng q1 c= dom f by TARSKI:def_3;
then consider s2 being Real_Sequence such that
A8: s2 is subsequence of q1 and
A9: s2 is convergent and
A10: lim s2 in dom f by A1, RCOMP_1:def_3;
take q2 = f /* s2; ::_thesis: ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f )
 rng s2 c= rng q1 by A8, VALUED_0:21;
then A11: rng s2 c= dom f by A7, XBOOLE_1:1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(f_/*_q1)_._n_=_s1_._n
let n be Element of NAT ; ::_thesis: (f /* q1) . n = s1 . n
 f /. (q1 . n) = s1 . n by A6;
hence  (f /* q1) . n = s1 . n by A7, FUNCT_2:109; ::_thesis: verum
end;
then A12: f /* q1 = s1 by FUNCT_2:63;
 lim s2 in dom (f | (dom f)) by A10;
then  f | (dom f) is_continuous_in lim s2 by A2, Def2;
then A13: f is_continuous_in lim s2 ;
then  f /. (lim s2) = lim (f /* s2) by A9, A11, Def1;
hence  ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A12, A8, A9, A10, A13, A11, Def1, PARTFUN2:2, VALUED_0:22; ::_thesis: verum
end;
hence  rng f is compact by NFCONT_1:def_2; ::_thesis: verum
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
proof
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: for Y being Subset of REAL st Y c= dom f & Y is compact & f | Y is continuous holds
f .: Y is compact
let Y be Subset of REAL; ::_thesis: ( Y c= dom f & Y is compact & f | Y is continuous implies f .: Y is compact )
assume that
A1: Y c= dom f and
A2: Y is compact and
A3: f | Y is continuous ; ::_thesis: f .: Y is compact
A4: (f | Y) | Y is continuous by A3;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61
.= Y by A1, XBOOLE_1:28 ;
then  rng (f | Y) is compact by A2, A4, Th24;
hence  f .: Y is compact by RELAT_1:115; ::_thesis: verum
end;

begin

definition
let S be RealNormSpace;
let f be PartFunc of REAL, the carrier of S;
attrf is Lipschitzian  means :Def3: :: NFCONT_3:def 3
 ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) );
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 number st
( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (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 number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
proof
let X be set ; ::_thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
thus  ( f | X is Lipschitzian implies ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) ) ::_thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )
proof
given r being real number  such that A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) ; :: according to NFCONT_3:def_3 ::_thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
take  r ; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
thus  0 < r by A1; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) )
A3: ( x1 in REAL & x2 in REAL ) by XREAL_0:def_1;
assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
then  ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by PARTFUN2:15, A3;
hence  ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by A2, A4; ::_thesis: verum
end;
given r being real number  such that A5: 0 < r and
A6: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ; ::_thesis: f | X is Lipschitzian
take  r ; :: according to NFCONT_3:def_3 ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) ) )
thus  0 < r by A5; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) )
A7: ( x1 in REAL & x2 in REAL ) by XREAL_0:def_1;
assume A8: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2))
then  ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by PARTFUN2:15, A7;
hence  ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) by A6, A8; ::_thesis: verum
end;

registration
let S be RealNormSpace;
cluster empty Function-like  ->  Lipschitzian for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is empty holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is empty implies f is Lipschitzian )
assume A1: f is empty ; ::_thesis: f is Lipschitzian
take  1 ; :: according to NFCONT_3:def_3 ::_thesis: ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) ) )
thus  ( 0 < 1 & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) ) ) by A1; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
cluster empty Relation-like REAL -defined the carrier of S -valued Function-like for Element of bool [:REAL, the carrier of S:];
existence
 ex b1 being PartFunc of REAL, the carrier of S st b1 is empty
proof
take  the empty PartFunc of REAL, the carrier of S ; ::_thesis: the empty PartFunc of REAL, the carrier of S is empty
thus  the empty PartFunc of REAL, the carrier of S is empty ; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let X be set ;
clusterf | X ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is Lipschitzian
proof
consider r being real number  such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by Def3;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
||.((f_/._x1)_-_(f_/._x2)).||_<=_r_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) )
assume  ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
then  ( x1 in dom f & x2 in dom f ) by RELAT_1:57;
hence  ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by A2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f | X holds
b1 is Lipschitzian by A1, Th26; ::_thesis: verum
end;
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
proof
let X, X1 be set ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S st f | X is Lipschitzian & X1 c= X holds
f | X1 is Lipschitzian
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian )
assume that
A1: f | X is Lipschitzian and
A2: X1 c= X ; ::_thesis: f | X1 is Lipschitzian
 f | X1 = (f | X) | X1 by A2, RELAT_1:74;
hence  f | X1 is Lipschitzian by A1; ::_thesis: verum
end;

registration
let S be RealNormSpace;
let f1, f2 be Lipschitzian PartFunc of REAL, the carrier of S;
clusterf1 + f2 ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is Lipschitzian
proof
set X = dom f1;
set X1 = dom f2;
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
||.((f1 /. x1) - (f1 /. x2)).|| <= s * (abs (x1 - x2)) by Th26;
consider g being real number  such that
A3: 0 < g and
A4: for x1, x2 being real number st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
||.((f2 /. x1) - (f2 /. x2)).|| <= g * (abs (x1 - x2)) by Th26;
now__::_thesis:_ex_p_being_set_st_
(_0_<_p_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(f1_+_f2)_&_x2_in_dom_(f1_+_f2)_holds_
||.(((f1_+_f2)_/._x1)_-_((f1_+_f2)_/._x2)).||_<=_p_*_(abs_(x1_-_x2))_)_)
take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * (abs (x1 - x2)) ) )
thus  0 < p by A1, A3; ::_thesis: for x1, x2 being real number st x1 in dom (f1 + f2) & x2 in dom (f1 + f2) holds
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * (abs (x1 - x2)) )
assume A5: ( x1 in dom (f1 + f2) & x2 in dom (f1 + f2) ) ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * (abs (x1 - x2))
||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A5, VFUNCT_1:def_1
.= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A5, VFUNCT_1:def_1
.= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:28
.= ||.((f1 /. x1) + (((f2 /. x1) - (f1 /. x2)) - (f2 /. x2))).|| by RLVECT_1:27
.= ||.((f1 /. x1) + (((- (f1 /. x2)) + (f2 /. x1)) - (f2 /. x2))).||
.= ||.((f1 /. x1) + ((- (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:28
.= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ;
then A6: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:def_1;
dom (f2 | ((dom f1) /\ (dom f2))) = (dom f2) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f2) /\ (dom f2)) /\ (dom f1) by XBOOLE_1:16
.= dom (f1 + f2) by VFUNCT_1:def_1 ;
then A7: ||.((f2 /. x1) - (f2 /. x2)).|| <= g * (abs (x1 - x2)) by A4, A5;
dom (f1 | ((dom f1) /\ (dom f2))) = (dom f1) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f1) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= dom (f1 + f2) by VFUNCT_1:def_1 ;
then  ||.((f1 /. x1) - (f1 /. x2)).|| <= s * (abs (x1 - x2)) by A2, A5;
then  ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * (abs (x1 - x2))) + (g * (abs (x1 - x2))) by A7, XREAL_1:7;
hence  ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * (abs (x1 - x2)) by A6, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f1 + f2 holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
clusterf1 - f2 ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is Lipschitzian
proof
set X = dom f1;
set X1 = dom f2;
consider s being real number  such that
A8: 0 < s and
A9: for x1, x2 being real number st x1 in dom (f1 | ((dom f1) /\ (dom f2))) & x2 in dom (f1 | ((dom f1) /\ (dom f2))) holds
||.((f1 /. x1) - (f1 /. x2)).|| <= s * (abs (x1 - x2)) by Th26;
consider g being real number  such that
A10: 0 < g and
A11: for x1, x2 being real number st x1 in dom (f2 | ((dom f1) /\ (dom f2))) & x2 in dom (f2 | ((dom f1) /\ (dom f2))) holds
||.((f2 /. x1) - (f2 /. x2)).|| <= g * (abs (x1 - x2)) by Th26;
now__::_thesis:_ex_p_being_set_st_
(_0_<_p_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(f1_-_f2)_&_x2_in_dom_(f1_-_f2)_holds_
||.(((f1_-_f2)_/._x1)_-_((f1_-_f2)_/._x2)).||_<=_p_*_(abs_(x1_-_x2))_)_)
take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being real number st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * (abs (x1 - x2)) ) )
thus  0 < p by A8, A10; ::_thesis: for x1, x2 being real number st x1 in dom (f1 - f2) & x2 in dom (f1 - f2) holds
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f1 - f2) & x2 in dom (f1 - f2) implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * (abs (x1 - x2)) )
assume A12: ( x1 in dom (f1 - f2) & x2 in dom (f1 - f2) ) ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * (abs (x1 - x2))
||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A12, VFUNCT_1:def_2
.= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A12, VFUNCT_1:def_2
.= ||.((f1 /. x1) - ((f2 /. x1) + ((f1 /. x2) - (f2 /. x2)))).|| by RLVECT_1:27
.= ||.((f1 /. x1) - (((f1 /. x2) + (f2 /. x1)) - (f2 /. x2))).|| by RLVECT_1:28
.= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:28
.= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ;
then A13: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3;
dom (f2 | ((dom f1) /\ (dom f2))) = (dom f2) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f2) /\ (dom f2)) /\ (dom f1) by XBOOLE_1:16
.= dom (f1 - f2) by VFUNCT_1:def_2 ;
then A14: ||.((f2 /. x1) - (f2 /. x2)).|| <= g * (abs (x1 - x2)) by A11, A12;
dom (f1 | ((dom f1) /\ (dom f2))) = (dom f1) /\ ((dom f1) /\ (dom f2)) by RELAT_1:61
.= ((dom f1) /\ (dom f1)) /\ (dom f2) by XBOOLE_1:16
.= dom (f1 - f2) by VFUNCT_1:def_2 ;
then  ||.((f1 /. x1) - (f1 /. x2)).|| <= s * (abs (x1 - x2)) by A9, A12;
then  ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * (abs (x1 - x2))) + (g * (abs (x1 - x2))) by A14, XREAL_1:7;
hence  ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * (abs (x1 - x2)) by A13, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = f1 - f2 holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
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
proof
let X, X1 be set ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f1, f2 be PartFunc of REAL, the carrier of S; ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian )
A1: ( f1 | (X /\ X1) = (f1 | X) | (X /\ X1) & f2 | (X /\ X1) = (f2 | X1) | (X /\ X1) ) by RELAT_1:74, XBOOLE_1:17;
A2: (f1 + f2) | (X /\ X1) = (f1 | (X /\ X1)) + (f2 | (X /\ X1)) by VFUNCT_1:27;
assume  ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 + f2) | (X /\ X1) is Lipschitzian
hence  (f1 + f2) | (X /\ X1) is Lipschitzian by A1, A2; ::_thesis: verum
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
proof
let X, X1 be set ; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f1, f2 be PartFunc of REAL, the carrier of S; ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 - f2) | (X /\ X1) is Lipschitzian )
A1: ( f1 | (X /\ X1) = (f1 | X) | (X /\ X1) & f2 | (X /\ X1) = (f2 | X1) | (X /\ X1) ) by RELAT_1:74, XBOOLE_1:17;
A2: (f1 - f2) | (X /\ X1) = (f1 | (X /\ X1)) - (f2 | (X /\ X1)) by VFUNCT_1:30;
assume  ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 - f2) | (X /\ X1) is Lipschitzian
hence  (f1 - f2) | (X /\ X1) is Lipschitzian by A1, A2; ::_thesis: verum
end;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
let p be Real;
clusterp (#) f ->  Lipschitzian for PartFunc of REAL, the carrier of S;
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian
proof
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= s * (abs (x1 - x2)) by Def3;
percases ( p = 0 or p <> 0 ) ;
supposeA3: p = 0 ; ::_thesis: for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian
now__::_thesis:_ex_s_being_real_number_st_
(_0_<_s_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(p_(#)_f)_&_x2_in_dom_(p_(#)_f)_holds_
||.(((p_(#)_f)_/._x1)_-_((p_(#)_f)_/._x2)).||_<=_s_*_(abs_(x1_-_x2))_)_)
take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2)) ) )
thus  0 < s by A1; ::_thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2)) )
assume A4: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) ) ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2))
A5: 0 <= abs (x1 - x2) by COMPLEX1:46;
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, VFUNCT_1:def_4
.= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A4, VFUNCT_1:def_4
.= ||.((0. S) - (p * (f /. x2))).|| by A3, RLVECT_1:10
.= ||.((0. S) - (0. S)).|| by A3, RLVECT_1:10
.= 0 by NORMSP_1:6 ;
hence  ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * (abs (x1 - x2)) by A1, A5; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
suppose p <> 0 ; ::_thesis: for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian
then  0 < abs p by COMPLEX1:47;
then A6: 0 * s < (abs p) * s by A1, XREAL_1:68;
now__::_thesis:_ex_g_being_Element_of_REAL_st_
(_0_<_g_&_(_for_x1,_x2_being_real_number_st_x1_in_dom_(p_(#)_f)_&_x2_in_dom_(p_(#)_f)_holds_
||.(((p_(#)_f)_/._x1)_-_((p_(#)_f)_/._x2)).||_<=_g_*_(abs_(x1_-_x2))_)_)
take g = (abs p) * s; ::_thesis: ( 0 < g & ( for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) ) )
A7: 0 <= abs p by COMPLEX1:46;
thus  0 < g by A6; ::_thesis: for x1, x2 being real number st x1 in dom (p (#) f) & x2 in dom (p (#) f) holds
||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) )
assume A8: ( x1 in dom (p (#) f) & x2 in dom (p (#) f) ) ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2))
then A9: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by VFUNCT_1:def_4
.= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A8, VFUNCT_1:def_4
.= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1:34
.= (abs p) * ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:def_1 ;
 ( x1 in dom f & x2 in dom f ) by A8, VFUNCT_1:def_4;
then  (abs p) * ||.((f /. x1) - (f /. x2)).|| <= (abs p) * (s * (abs (x1 - x2))) by A2, A7, XREAL_1:64;
hence  ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * (abs (x1 - x2)) by A9; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL, the carrier of S st b1 = p (#) f holds
b1 is Lipschitzian by Def3; ::_thesis: verum
end;
end;
end;
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
proof
let X be set ; ::_thesis: 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
let p be Real; ::_thesis: 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
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian )
 (p (#) f) | X = p (#) (f | X) by VFUNCT_1:31;
hence  ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) ; ::_thesis: verum
end;

registration
let S be RealNormSpace;
let f be Lipschitzian PartFunc of REAL, the carrier of S;
cluster||.f.|| ->  Lipschitzian for PartFunc of REAL,REAL;
coherence
 for b1 being PartFunc of REAL,REAL st b1 = ||.f.|| holds
b1 is Lipschitzian
proof
consider s being real number  such that
A1: 0 < s and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= s * (abs (x1 - x2)) by Def3;
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_||.f.||_&_x2_in_dom_||.f.||_holds_
abs_((||.f.||_._x1)_-_(||.f.||_._x2))_<=_s_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom ||.f.|| & x2 in dom ||.f.|| implies abs ((||.f.|| . x1) - (||.f.|| . x2)) <= s * (abs (x1 - x2)) )
assume A3: ( x1 in dom ||.f.|| & x2 in dom ||.f.|| ) ; ::_thesis: abs ((||.f.|| . x1) - (||.f.|| . x2)) <= s * (abs (x1 - x2))
then  ( x1 in dom f & x2 in dom f ) by NORMSP_0:def_3;
then A4: ||.((f /. x1) - (f /. x2)).|| <= s * (abs (x1 - x2)) by A2;
abs ((||.f.|| . x1) - (||.f.|| . x2)) = abs (||.(f /. x1).|| - (||.f.|| . x2)) by A3, NORMSP_0:def_3
.= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A3, NORMSP_0:def_3 ;
then  abs ((||.f.|| . x1) - (||.f.|| . x2)) <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:9;
hence  abs ((||.f.|| . x1) - (||.f.|| . x2)) <= s * (abs (x1 - x2)) by A4, XXREAL_0:2; ::_thesis: verum
end;
hence  for b1 being PartFunc of REAL,REAL st b1 = ||.f.|| holds
b1 is Lipschitzian by A1, FCONT_1:def_3; ::_thesis: verum
end;
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 )
proof
let X be set ; ::_thesis: 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 )
let S be RealNormSpace; ::_thesis: 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 )
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian ) )
assume A1: f | X is Lipschitzian ; ::_thesis: ( - (f | X) is Lipschitzian & (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
A2: - (f | X) = (- 1) (#) (f | X) by VFUNCT_1:23;
hence  - (f | X) is Lipschitzian by A1; ::_thesis: ( (- f) | X is Lipschitzian & ||.f.|| | X is Lipschitzian )
thus  (- f) | X is Lipschitzian by A1, A2, VFUNCT_1:29; ::_thesis: ||.f.|| | X is Lipschitzian
 ||.f.|| | X = ||.(f | X).|| by VFUNCT_1:29;
hence  ||.f.|| | X is Lipschitzian by A1; ::_thesis: verum
end;

registration
let S be RealNormSpace;
cluster Function-like constant  ->  Lipschitzian for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is constant holds
b1 is Lipschitzian
proof
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is constant implies f is Lipschitzian )
assume A1: f is constant ; ::_thesis: f is Lipschitzian
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) )
assume A2: ( x1 in dom f & x2 in dom f ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2))
then f /. x1 = f . x1 by PARTFUN1:def_6
.= f . x2 by A1, A2, FUNCT_1:def_10
.= f /. x2 by A2, PARTFUN1:def_6 ;
then  ||.((f /. x1) - (f /. x2)).|| = 0 by NORMSP_1:6;
hence  ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) by COMPLEX1:46; ::_thesis: verum
end;
hence  f is Lipschitzian by Def3; ::_thesis: verum
end;
end;

registration
let S be RealNormSpace;
cluster Function-like Lipschitzian  ->  continuous for Element of bool [:REAL, the carrier of S:];
coherence
 for b1 being PartFunc of REAL, the carrier of S st b1 is Lipschitzian holds
b1 is continuous
proof
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( f is Lipschitzian implies f is continuous )
set X = dom f;
assume  f is Lipschitzian ; ::_thesis: f is continuous
then consider r being real number  such that
A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom f & x2 in dom f holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by Def3;
now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_f_holds_
f_is_continuous_in_x0
let x0 be real number ; ::_thesis: ( x0 in dom f implies f is_continuous_in x0 )
assume A3: x0 in dom f ; ::_thesis: f is_continuous_in x0
 for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < r ) )
proof
let g be Real; ::_thesis: ( 0 < g implies ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < g ) ) )
assume A4: 0 < g ; ::_thesis: ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds
||.((f /. x1) - (f /. x0)).|| < g ) )
set s = g / r;
take s9 = g / r; ::_thesis: ( 0 < s9 & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s9 holds
||.((f /. x1) - (f /. x0)).|| < g ) )
A5: now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_g_/_r_holds_
||.((f_/._x1)_-_(f_/._x0)).||_<_g
let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < g / r implies ||.((f /. x1) - (f /. x0)).|| < g )
assume that
A6: x1 in dom f and
A7: abs (x1 - x0) < g / r ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < g
 r * (abs (x1 - x0)) < (g / r) * r by A1, A7, XREAL_1:68;
then A8: r * (abs (x1 - x0)) < g by A1, XCMPLX_1:87;
 ||.((f /. x1) - (f /. x0)).|| <= r * (abs (x1 - x0)) by A2, A3, A6;
hence  ||.((f /. x1) - (f /. x0)).|| < g by A8, XXREAL_0:2; ::_thesis: verum
end;
 s9 = g * (r ") by XCMPLX_0:def_9;
hence  ( 0 < s9 & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s9 holds
||.((f /. x1) - (f /. x0)).|| < g ) ) by A1, A4, A5, XREAL_1:129; ::_thesis: verum
end;
hence  f is_continuous_in x0 by A3, Th8; ::_thesis: verum
end;
hence  f is continuous by Def2; ::_thesis: verum
end;
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
proof
let S be RealNormSpace; ::_thesis: 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
let f be PartFunc of REAL, the carrier of S; ::_thesis: ( ex r being Point of S st rng f = {r} implies f is continuous )
given r being Point of S such that A1: rng f = {r} ; ::_thesis: f is continuous
now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_
||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) )
assume A2: ( x1 in dom f & x2 in dom f ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2))
then  f . x2 in rng f by FUNCT_1:def_3;
then  f /. x2 in rng f by A2, PARTFUN1:def_6;
then A3: f /. x2 = r by A1, TARSKI:def_1;
 f . x1 in rng f by A2, FUNCT_1:def_3;
then  f /. x1 in rng f by A2, PARTFUN1:def_6;
then  f /. x1 = r by A1, TARSKI:def_1;
then  ||.((f /. x1) - (f /. x2)).|| = 0 by A3, NORMSP_1:6;
hence  ||.((f /. x1) - (f /. x2)).|| <= 1 * (abs (x1 - x2)) by COMPLEX1:46; ::_thesis: verum
end;
then  f is Lipschitzian by Def3;
hence  f is continuous ; ::_thesis: verum
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 number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
proof
let X be set ; ::_thesis: 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 number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let S be RealNormSpace; ::_thesis: for f being PartFunc of REAL, the carrier of S
for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let f be PartFunc of REAL, the carrier of S; ::_thesis: for r, p being Point of S st ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) holds
f | X is continuous
let r, p be Point of S; ::_thesis: ( ( for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ) implies f | X is continuous )
assume A1: for x0 being real number st x0 in X holds
f /. x0 = (x0 * r) + p ; ::_thesis: f | X is continuous
A2: now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_
||.((f_/._x1)_-_(f_/._x2)).||_<=_(||.r.||_+_1)_*_(abs_(x1_-_x2))
let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2)) )
assume A3: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2))
then  x2 in X ;
then A4: f /. x2 = (x2 * r) + p by A1;
A5: 0 <= abs (x1 - x2) by COMPLEX1:46;
A6: x1 - x2 is Real by XREAL_0:def_1;
 x1 in X by A3;
then  f /. x1 = (x1 * r) + p by A1;
then ||.((f /. x1) - (f /. x2)).|| = ||.((x1 * r) + (p - (p + (x2 * r)))).|| by A4, RLVECT_1:def_3
.= ||.((x1 * r) + ((p - p) - (x2 * r))).|| by RLVECT_1:27
.= ||.((x1 * r) + ((0. S) - (x2 * r))).|| by RLVECT_1:15
.= ||.((x1 * r) - (x2 * r)).|| by RLVECT_1:14
.= ||.((x1 - x2) * r).|| by RLVECT_1:35
.= (abs (x1 - x2)) * ||.r.|| by A6, NORMSP_1:def_1 ;
then  ||.((f /. x1) - (f /. x2)).|| + 0 <= (||.r.|| * (abs (x1 - x2))) + (1 * (abs (x1 - x2))) by A5, XREAL_1:7;
hence  ||.((f /. x1) - (f /. x2)).|| <= (||.r.|| + 1) * (abs (x1 - x2)) ; ::_thesis: verum
end;
 0 + 0 < ||.r.|| + 1 by NORMSP_1:4, XREAL_1:8;
then  f | X is Lipschitzian by A2, Th26;
hence  f | X is continuous ; ::_thesis: verum
end;