:: NFCONT_1 semantic presentation begin theorem :: NFCONT_1:1 for S being non empty addLoopStr for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2) proof let S be non empty addLoopStr ; ::_thesis: for seq1, seq2 being sequence of S holds seq1 - seq2 = seq1 + (- seq2) let seq1, seq2 be sequence of S; ::_thesis: seq1 - seq2 = seq1 + (- seq2) for n being Element of NAT holds (seq1 - seq2) . n = (seq1 + (- seq2)) . n proof let n be Element of NAT ; ::_thesis: (seq1 - seq2) . n = (seq1 + (- seq2)) . n thus (seq1 - seq2) . n = (seq1 . n) - (seq2 . n) by NORMSP_1:def_3 .= (seq1 . n) + ((- seq2) . n) by BHSP_1:44 .= (seq1 + (- seq2)) . n by NORMSP_1:def_2 ; ::_thesis: verum end; hence seq1 - seq2 = seq1 + (- seq2) by FUNCT_2:63; ::_thesis: verum end; theorem Th2: :: NFCONT_1:2 for S being RealNormSpace for seq being sequence of S holds - seq = (- 1) * seq proof let S be RealNormSpace; ::_thesis: for seq being sequence of S holds - seq = (- 1) * seq let seq be sequence of S; ::_thesis: - seq = (- 1) * seq now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_1)_*_seq)_._n_=_(-_seq)_._n let n be Element of NAT ; ::_thesis: ((- 1) * seq) . n = (- seq) . n thus ((- 1) * seq) . n = (- 1) * (seq . n) by NORMSP_1:def_5 .= - (seq . n) by RLVECT_1:16 .= (- seq) . n by BHSP_1:44 ; ::_thesis: verum end; hence - seq = (- 1) * seq by FUNCT_2:63; ::_thesis: verum end; definition let S be RealNormSpace; let x0 be Point of S; mode Neighbourhood of x0 -> Subset of S means :Def1: :: NFCONT_1:def 1 ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= it ); existence ex b1 being Subset of S ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b1 ) proof set N = { y where y is Point of S : ||.(y - x0).|| < 1 } ; take { y where y is Point of S : ||.(y - x0).|| < 1 } ; ::_thesis: ( { y where y is Point of S : ||.(y - x0).|| < 1 } is Subset of S & ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= { y where y is Point of S : ||.(y - x0).|| < 1 } ) ) { y where y is Point of S : ||.(y - x0).|| < 1 } c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of S : ||.(y - x0).|| < 1 } or x in the carrier of S ) assume x in { y where y is Point of S : ||.(y - x0).|| < 1 } ; ::_thesis: x in the carrier of S then ex y being Point of S st ( x = y & ||.(y - x0).|| < 1 ) ; hence x in the carrier of S ; ::_thesis: verum end; hence ( { y where y is Point of S : ||.(y - x0).|| < 1 } is Subset of S & ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= { y where y is Point of S : ||.(y - x0).|| < 1 } ) ) ; ::_thesis: verum end; end; :: deftheorem Def1 defines Neighbourhood NFCONT_1:def_1_:_ for S being RealNormSpace for x0 being Point of S for b3 being Subset of S holds ( b3 is Neighbourhood of x0 iff ex g being Real st ( 0 < g & { y where y is Point of S : ||.(y - x0).|| < g } c= b3 ) ); theorem Th3: :: NFCONT_1:3 for S being RealNormSpace for x0 being Point of S for g being Real st 0 < g holds { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 proof let S be RealNormSpace; ::_thesis: for x0 being Point of S for g being Real st 0 < g holds { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 let x0 be Point of S; ::_thesis: for g being Real st 0 < g holds { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 let g be Real; ::_thesis: ( 0 < g implies { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 ) assume A1: g > 0 ; ::_thesis: { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 set N = { y where y is Point of S : ||.(y - x0).|| < g } ; { y where y is Point of S : ||.(y - x0).|| < g } c= the carrier of S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of S : ||.(y - x0).|| < g } or x in the carrier of S ) assume x in { y where y is Point of S : ||.(y - x0).|| < g } ; ::_thesis: x in the carrier of S then ex y being Point of S st ( x = y & ||.(y - x0).|| < g ) ; hence x in the carrier of S ; ::_thesis: verum end; hence { y where y is Point of S : ||.(y - x0).|| < g } is Neighbourhood of x0 by A1, Def1; ::_thesis: verum end; theorem Th4: :: NFCONT_1:4 for S being RealNormSpace for x0 being Point of S for N being Neighbourhood of x0 holds x0 in N proof let S be RealNormSpace; ::_thesis: for x0 being Point of S for N being Neighbourhood of x0 holds x0 in N let x0 be Point of S; ::_thesis: for N being Neighbourhood of x0 holds x0 in N let N be Neighbourhood of x0; ::_thesis: x0 in N consider g being Real such that A1: 0 < g and A2: { z where z is Point of S : ||.(z - x0).|| < g } c= N by Def1; ||.(x0 - x0).|| = ||.(0. S).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; then x0 in { z where z is Point of S : ||.(z - x0).|| < g } by A1; hence x0 in N by A2; ::_thesis: verum end; definition let S be RealNormSpace; let X be Subset of S; attrX is compact means :Def2: :: NFCONT_1:def 2 for s1 being sequence of S st rng s1 c= X holds ex s2 being sequence of S st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ); end; :: deftheorem Def2 defines compact NFCONT_1:def_2_:_ for S being RealNormSpace for X being Subset of S holds ( X is compact iff for s1 being sequence of S st rng s1 c= X holds ex s2 being sequence of S st ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ); definition let S be RealNormSpace; let X be Subset of S; attrX is closed means :: NFCONT_1:def 3 for s1 being sequence of S st rng s1 c= X & s1 is convergent holds lim s1 in X; end; :: deftheorem defines closed NFCONT_1:def_3_:_ for S being RealNormSpace for X being Subset of S holds ( X is closed iff for s1 being sequence of S st rng s1 c= X & s1 is convergent holds lim s1 in X ); definition let S be RealNormSpace; let X be Subset of S; attrX is open means :: NFCONT_1:def 4 X ` is closed ; end; :: deftheorem defines open NFCONT_1:def_4_:_ for S being RealNormSpace for X being Subset of S holds ( X is open iff X ` is closed ); definition let S, T be RealNormSpace; let f be PartFunc of S,T; let x0 be Point of S; predf is_continuous_in x0 means :Def5: :: NFCONT_1:def 5 ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ); end; :: deftheorem Def5 defines is_continuous_in NFCONT_1:def_5_:_ for S, T being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ); definition let S be RealNormSpace; let f be PartFunc of the carrier of S,REAL; let x0 be Point of S; predf is_continuous_in x0 means :Def6: :: NFCONT_1:def 6 ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ); end; :: deftheorem Def6 defines is_continuous_in NFCONT_1:def_6_:_ for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for s1 being sequence of S st rng s1 c= dom f & s1 is convergent & lim s1 = x0 holds ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) ) ); theorem Th5: :: NFCONT_1:5 for n being Element of NAT for S, T being RealNormSpace for seq being sequence of S for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h proof let n be Element of NAT ; ::_thesis: for S, T being RealNormSpace for seq being sequence of S for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h let S, T be RealNormSpace; ::_thesis: for seq being sequence of S for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h let seq be sequence of S; ::_thesis: for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h dom seq = NAT by FUNCT_2:def_1; then seq . n in rng seq by FUNCT_1:def_3; hence for h being PartFunc of S,T st rng seq c= dom h holds seq . n in dom h ; ::_thesis: verum end; theorem Th6: :: NFCONT_1:6 for S being RealNormSpace for seq being sequence of S for x being set holds ( x in rng seq iff ex n being Element of NAT st x = seq . n ) proof let S be RealNormSpace; ::_thesis: for seq being sequence of S for x being set holds ( x in rng seq iff ex n being Element of NAT st x = seq . n ) let seq be sequence of S; ::_thesis: for x being set holds ( x in rng seq iff ex n being Element of NAT st x = seq . n ) let x be set ; ::_thesis: ( x in rng seq iff ex n being Element of NAT st x = seq . n ) thus ( x in rng seq implies ex n being Element of NAT st x = seq . n ) ::_thesis: ( ex n being Element of NAT st x = seq . n implies x in rng seq ) proof assume x in rng seq ; ::_thesis: ex n being Element of NAT st x = seq . n then consider y being set such that A1: y in dom seq and A2: x = seq . y by FUNCT_1:def_3; reconsider m = y as Element of NAT by A1; take m ; ::_thesis: x = seq . m thus x = seq . m by A2; ::_thesis: verum end; given n being Element of NAT such that A3: x = seq . n ; ::_thesis: x in rng seq n in NAT ; then n in dom seq by FUNCT_2:def_1; hence x in rng seq by A3, FUNCT_1:def_3; ::_thesis: verum end; theorem Th7: :: NFCONT_1:7 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) let x0 be Point 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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) hence x0 in dom f by Def5; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) given r being Real such that A2: 0 < r and A3: for s being Real holds ( not 0 < s or ex x1 being Point of S st ( x1 in dom f & ||.(x1 - x0).|| < s & not ||.((f /. x1) - (f /. x0)).|| < r ) ) ; ::_thesis: contradiction defpred S1[ Element of NAT , Point of S] means ( \$2 in dom f & ||.(\$2 - x0).|| < 1 / (\$1 + 1) & not ||.((f /. \$2) - (f /. x0)).|| < r ); A4: for n being Element of NAT ex p being Point of S st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Point of S st S1[n,p] 0 < n + 1 by NAT_1:3; then 0 < (n + 1) " by XREAL_1:122; then 0 < 1 / (n + 1) by XCMPLX_1:215; then consider p being Point of S such that A5: ( p in dom f & ||.(p - x0).|| < 1 / (n + 1) & not ||.((f /. p) - (f /. x0)).|| < r ) by A3; take p ; ::_thesis: S1[n,p] thus S1[n,p] by A5; ::_thesis: verum end; consider s1 being Function of NAT, the carrier of S such that A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A4); reconsider s1 = s1 as sequence of S ; A7: rng s1 c= dom f proof A8: dom s1 = NAT by FUNCT_2:def_1; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng s1 or v in dom f ) assume v in rng s1 ; ::_thesis: v in dom f then ex n being set st ( n in NAT & v = s1 . n ) by A8, FUNCT_1:def_3; hence v in dom f by A6; ::_thesis: verum end; A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_||.(((f_/*_s1)_._n)_-_(f_/._x0)).||_<_r let n be Element of NAT ; ::_thesis: not ||.(((f /* s1) . n) - (f /. x0)).|| < r not ||.((f /. (s1 . n)) - (f /. x0)).|| < r by A6; hence not ||.(((f /* s1) . n) - (f /. x0)).|| < r by A7, FUNCT_2:109; ::_thesis: verum end; A10: now__::_thesis:_for_s_being_Real_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ ||.((s1_._m)_-_x0).||_<_s let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s ) consider n being Element of NAT such that A11: s " < n by SEQ_4:3; assume 0 < s ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s then A12: 0 < s " by XREAL_1:122; (s ") + 0 < n + 1 by A11, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76; then A13: 1 / (n + 1) < s by XCMPLX_1:216; take k = n; ::_thesis: for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s let m be Element of NAT ; ::_thesis: ( k <= m implies ||.((s1 . m) - x0).|| < s ) assume k <= m ; ::_thesis: ||.((s1 . m) - x0).|| < s then k + 1 <= m + 1 by XREAL_1:6; then 1 / (m + 1) <= 1 / (k + 1) by NAT_1:3, XREAL_1:118; then 1 / (m + 1) < s by A13, XXREAL_0:2; hence ||.((s1 . m) - x0).|| < s by A6, XXREAL_0:2; ::_thesis: verum end; then A14: s1 is convergent by NORMSP_1:def_6; then lim s1 = x0 by A10, NORMSP_1:def_7; then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A14, Def5; then consider n being Element of NAT such that A15: 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 A15; hence contradiction by A9; ::_thesis: verum end; assume that A16: x0 in dom f and A17: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ; ::_thesis: f is_continuous_in x0 now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) assume that A18: rng s1 c= dom f and A19: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) A20: 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 such that A21: 0 < s and A22: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < p by A17; consider n being Element of NAT such that A23: for m being Element of NAT st n <= m holds ||.((s1 . m) - x0).|| < s by A19, A21, NORMSP_1: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 A24: ||.((s1 . m) - x0).|| < s by A23; dom s1 = NAT by FUNCT_2:def_1; then s1 . m in rng s1 by FUNCT_1:3; then ||.((f /. (s1 . m)) - (f /. x0)).|| < p by A18, A22, A24; hence ||.(((f /* s1) . m) - (f /. x0)).|| < p by A18, 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 A20, NORMSP_1:def_7; ::_thesis: verum end; hence f is_continuous_in x0 by A16, Def5; ::_thesis: verum end; theorem Th8: :: NFCONT_1:8 for S being RealNormSpace for x0 being Point of S for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) proof let S be RealNormSpace; ::_thesis: for x0 being Point of S for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) let x0 be Point of S; ::_thesis: for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) let f be PartFunc of the carrier of S,REAL; ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((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 st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) hence x0 in dom f by Def6; ::_thesis: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) given r being Real such that A2: 0 < r and A3: for s being Real holds ( not 0 < s or ex x1 being Point of S st ( x1 in dom f & ||.(x1 - x0).|| < s & not abs ((f /. x1) - (f /. x0)) < r ) ) ; ::_thesis: contradiction defpred S1[ Element of NAT , Point of S] means ( \$2 in dom f & ||.(\$2 - x0).|| < 1 / (\$1 + 1) & not abs ((f /. \$2) - (f /. x0)) < r ); A4: for n being Element of NAT ex p being Point of S st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Point of S st S1[n,p] 0 < n + 1 by NAT_1:3; then 0 < (n + 1) " by XREAL_1:122; then 0 < 1 / (n + 1) by XCMPLX_1:215; then consider p being Point of S such that A5: ( p in dom f & ||.(p - x0).|| < 1 / (n + 1) & abs ((f /. p) - (f /. x0)) >= r ) by A3; take p ; ::_thesis: S1[n,p] thus S1[n,p] by A5; ::_thesis: verum end; consider s1 being Function of NAT, the carrier of S such that A6: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A4); reconsider s1 = s1 as sequence of S ; A7: rng s1 c= dom f proof A8: dom s1 = NAT by FUNCT_2:def_1; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng s1 or v in dom f ) assume v in rng s1 ; ::_thesis: v in dom f then ex n being set st ( n in NAT & v = s1 . n ) by A8, FUNCT_1:def_3; hence v in dom f by A6; ::_thesis: verum end; A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_abs_(((f_/*_s1)_._n)_-_(f_/._x0))_>=_r let n be Element of NAT ; ::_thesis: abs (((f /* s1) . n) - (f /. x0)) >= r abs ((f /. (s1 . n)) - (f /. x0)) >= r by A6; hence abs (((f /* s1) . n) - (f /. x0)) >= r by A7, FUNCT_2:109; ::_thesis: verum end; A10: now__::_thesis:_for_s_being_Real_st_0_<_s_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ ||.((s1_._m)_-_x0).||_<_s let s be Real; ::_thesis: ( 0 < s implies ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s ) consider n being Element of NAT such that A11: s " < n by SEQ_4:3; assume 0 < s ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s then A12: 0 < s " by XREAL_1:122; (s ") + 0 < n + 1 by A11, XREAL_1:8; then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76; then A13: 1 / (n + 1) < s by XCMPLX_1:216; take k = n; ::_thesis: for m being Element of NAT st k <= m holds ||.((s1 . m) - x0).|| < s let m be Element of NAT ; ::_thesis: ( k <= m implies ||.((s1 . m) - x0).|| < s ) assume k <= m ; ::_thesis: ||.((s1 . m) - x0).|| < s then k + 1 <= m + 1 by XREAL_1:6; then 1 / (m + 1) <= 1 / (k + 1) by NAT_1:3, XREAL_1:118; then 1 / (m + 1) < s by A13, XXREAL_0:2; hence ||.((s1 . m) - x0).|| < s by A6, XXREAL_0:2; ::_thesis: verum end; then A14: s1 is convergent by NORMSP_1:def_6; then lim s1 = x0 by A10, NORMSP_1:def_7; then ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A1, A7, A14, Def6; then consider n being Element of NAT such that A15: for m being Element of NAT st n <= m holds abs (((f /* s1) . m) - (f /. x0)) < r by A2, SEQ_2:def_7; abs (((f /* s1) . n) - (f /. x0)) < r by A15; hence contradiction by A9; ::_thesis: verum end; assume that A16: x0 in dom f and A17: for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ; ::_thesis: f is_continuous_in x0 now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) ) assume that A18: rng s1 c= dom f and A19: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) A20: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_ ex_k_being_Element_of_NAT_st_ for_m_being_Element_of_NAT_st_k_<=_m_holds_ abs_(((f_/*_s1)_._m)_-_(f_/._x0))_<_p let p be real number ; ::_thesis: ( 0 < p implies ex k being Element of NAT st for m being Element of NAT st k <= m holds abs (((f /* s1) . m) - (f /. x0)) < p ) reconsider pp = p as Real by XREAL_0:def_1; assume 0 < p ; ::_thesis: ex k being Element of NAT st for m being Element of NAT st k <= m holds abs (((f /* s1) . m) - (f /. x0)) < p then consider s being Real such that A21: 0 < s and A22: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < pp by A17; consider n being Element of NAT such that A23: for m being Element of NAT st n <= m holds ||.((s1 . m) - x0).|| < s by A19, A21, NORMSP_1:def_7; take k = n; ::_thesis: for m being Element of NAT st k <= m holds abs (((f /* s1) . m) - (f /. x0)) < p let m be Element of NAT ; ::_thesis: ( k <= m implies abs (((f /* s1) . m) - (f /. x0)) < p ) assume k <= m ; ::_thesis: abs (((f /* s1) . m) - (f /. x0)) < p then A24: ||.((s1 . m) - x0).|| < s by A23; dom s1 = NAT by FUNCT_2:def_1; then s1 . m in rng s1 by FUNCT_1:3; then abs ((f /. (s1 . m)) - (f /. x0)) < p by A18, A22, A24; hence abs (((f /* s1) . m) - (f /. x0)) < p by A18, FUNCT_2:109; ::_thesis: verum end; then f /* s1 is convergent by SEQ_2:def_6; hence ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) by A20, SEQ_2:def_7; ::_thesis: verum end; hence f is_continuous_in x0 by A16, Def6; ::_thesis: verum end; theorem Th9: :: NFCONT_1:9 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S 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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S 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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S 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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) let x0 be Point of S; ::_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 Point of S 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 Point of S 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 Point of S 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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) hence x0 in dom f by Def5; ::_thesis: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st for x1 being Point of S 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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 consider r being Real such that A2: 0 < r and A3: { y where y is Point of T : ||.(y - (f /. x0)).|| < r } c= N1 by Def1; consider s being Real such that A4: 0 < s and A5: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A1, A2, Th7; reconsider N = { z where z is Point of S : ||.(z - x0).|| < s } as Neighbourhood of x0 by A4, Th3; take N ; ::_thesis: for x1 being Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 let x1 be Point of S; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N1 ) assume that A6: x1 in dom f and A7: x1 in N ; ::_thesis: f /. x1 in N1 ex z being Point of S st ( x1 = z & ||.(z - x0).|| < s ) by A7; then ||.((f /. x1) - (f /. x0)).|| < r by A5, A6; then f /. x1 in { y where y is Point of T : ||.(y - (f /. x0)).|| < r } ; hence f /. x1 in N1 by A3; ::_thesis: verum end; assume that A8: x0 in dom f and A9: for N1 being Neighbourhood of f /. x0 ex N being Neighbourhood of x0 st for x1 being Point of S 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_st_ (_0_<_s_&_(_for_x1_being_Point_of_S_st_x1_in_dom_f_&_||.(x1_-_x0).||_<_s_holds_ ||.((f_/._x1)_-_(f_/._x0)).||_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) then reconsider N1 = { y where y is Point of T : ||.(y - (f /. x0)).|| < r } as Neighbourhood of f /. x0 by Th3; consider N2 being Neighbourhood of x0 such that A10: for x1 being Point of S st x1 in dom f & x1 in N2 holds f /. x1 in N1 by A9; consider s being Real such that A11: 0 < s and A12: { z where z is Point of S : ||.(z - x0).|| < s } c= N2 by Def1; take s = s; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r proof let x1 be Point of S; ::_thesis: ( x1 in dom f & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r ) assume that A13: x1 in dom f and A14: ||.(x1 - x0).|| < s ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r x1 in { z where z is Point of S : ||.(z - x0).|| < s } by A14; then f /. x1 in N1 by A10, A12, A13; then ex y being Point of T st ( f /. x1 = y & ||.(y - (f /. x0)).|| < r ) ; hence ||.((f /. x1) - (f /. x0)).|| < r ; ::_thesis: verum end; hence ( 0 < s & ( for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) by A11; ::_thesis: verum end; hence f is_continuous_in x0 by A8, Th7; ::_thesis: verum end; theorem Th10: :: NFCONT_1:10 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S 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 T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S 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 S,T; ::_thesis: for x0 being Point of S 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 Point of S; ::_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 Def5; ::_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 Point of S 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 Point of S such that A3: x in dom f and A4: x in N and A5: r = f . x by PARTFUN2:59; r = f /. x by A3, A5, PARTFUN1:def_6; hence r in N1 by A2, A3, A4; ::_thesis: verum end; hence f .: N c= N1 by TARSKI:def_3; ::_thesis: verum end; assume that A6: x0 in dom f and A7: 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_Point_of_S_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 Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 consider N being Neighbourhood of x0 such that A8: f .: N c= N1 by A7; take N = N; ::_thesis: for x1 being Point of S st x1 in dom f & x1 in N holds f /. x1 in N1 let x1 be Point of S; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N1 ) assume that A9: x1 in dom f and A10: x1 in N ; ::_thesis: f /. x1 in N1 f . x1 in f .: N by A9, A10, FUNCT_1:def_6; then f . x1 in N1 by A8; hence f /. x1 in N1 by A9, PARTFUN1:def_6; ::_thesis: verum end; hence f is_continuous_in x0 by A6, Th9; ::_thesis: verum end; theorem :: NFCONT_1:11 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 let x0 be Point of S; ::_thesis: ( x0 in dom f & ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 ) assume A1: x0 in dom f ; ::_thesis: ( for N being Neighbourhood of x0 holds not (dom f) /\ N = {x0} or f is_continuous_in x0 ) given N being Neighbourhood of x0 such that A2: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0 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 Th4; f .: N = Im (f,x0) by A2, RELAT_1:112 .= {(f . x0)} by A1, FUNCT_1:59 .= {(f /. x0)} by A1, PARTFUN1:def_6 ; hence f .: N c= N1 by A3, ZFMISC_1:31; ::_thesis: verum end; hence f is_continuous_in x0 by A1, Th10; ::_thesis: verum end; theorem Th12: :: NFCONT_1:12 for S, T being RealNormSpace for h1, h2 being PartFunc of S,T for seq being sequence of S 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, T be RealNormSpace; ::_thesis: for h1, h2 being PartFunc of S,T for seq being sequence of S 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 S,T; ::_thesis: for seq being sequence of S 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 sequence of S; ::_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 by XBOOLE_1:17; A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17; assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) ) then A4: rng seq c= dom (h1 + h2) by VFUNCT_1:def_1; 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) A5: seq . n in dom (h1 + h2) by A4, Th5; thus ((h1 + h2) /* seq) . n = (h1 + h2) /. (seq . n) by A4, FUNCT_2:109 .= (h1 /. (seq . n)) + (h2 /. (seq . n)) by A5, VFUNCT_1:def_1 .= ((h1 /* seq) . n) + (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1: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) A6: rng seq c= dom (h1 - h2) by A3, VFUNCT_1:def_2; 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) A7: seq . n in dom (h1 - h2) by A6, Th5; thus ((h1 - h2) /* seq) . n = (h1 - h2) /. (seq . n) by A6, FUNCT_2:109 .= (h1 /. (seq . n)) - (h2 /. (seq . n)) by A7, VFUNCT_1:def_2 .= ((h1 /* seq) . n) - (h2 /. (seq . n)) by A3, A1, FUNCT_2:109, XBOOLE_1:1 .= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by NORMSP_1:def_3; ::_thesis: verum end; theorem Th13: :: NFCONT_1:13 for S, T being RealNormSpace for h being PartFunc of S,T for seq being sequence of S for r being Real st rng seq c= dom h holds (r (#) h) /* seq = r * (h /* seq) proof let S, T be RealNormSpace; ::_thesis: for h being PartFunc of S,T for seq being sequence of S for r being Real st rng seq c= dom h holds (r (#) h) /* seq = r * (h /* seq) let h be PartFunc of S,T; ::_thesis: for seq being sequence of S for r being Real st rng seq c= dom h holds (r (#) h) /* seq = r * (h /* seq) let seq be sequence of S; ::_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, Th5; 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 Th14: :: NFCONT_1:14 for S, T being RealNormSpace for h being PartFunc of S,T for seq being sequence of S st rng seq c= dom h holds ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) proof let S, T be RealNormSpace; ::_thesis: for h being PartFunc of S,T for seq being sequence of S st rng seq c= dom h holds ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) let h be PartFunc of S,T; ::_thesis: for seq being sequence of S st rng seq c= dom h holds ( ||.(h /* seq).|| = ||.h.|| /* seq & - (h /* seq) = (- h) /* seq ) let seq be sequence of S; ::_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 Th6; 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 thus - (h /* seq) = (- 1) * (h /* seq) by Th2 .= ((- 1) (#) h) /* seq by A1, Th13 .= (- h) /* seq by VFUNCT_1:23 ; ::_thesis: verum end; theorem :: NFCONT_1:15 for T, S being RealNormSpace for f1, f2 being PartFunc of S,T for x0 being Point of S st 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 T, S be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T for x0 being Point of S st 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 S,T; ::_thesis: for x0 being Point of S st f1 is_continuous_in x0 & f2 is_continuous_in x0 holds ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) let x0 be Point of S; ::_thesis: ( f1 is_continuous_in x0 & f2 is_continuous_in x0 implies ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) ) assume that A1: f1 is_continuous_in x0 and A2: f2 is_continuous_in x0 ; ::_thesis: ( f1 + f2 is_continuous_in x0 & f1 - f2 is_continuous_in x0 ) A3: ( x0 in dom f1 & x0 in dom f2 ) by A1, A2, Def5; now__::_thesis:_(_x0_in_dom_(f1_+_f2)_&_(_for_s1_being_sequence_of_S_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)_)_)_) x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4; hence A4: x0 in dom (f1 + f2) by VFUNCT_1:def_1; ::_thesis: for s1 being sequence of S 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 sequence of S; ::_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) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1; then dom (f1 + f2) c= dom f2 by XBOOLE_1:17; then A8: rng s1 c= dom f2 by A5, XBOOLE_1:1; then A9: f2 /* s1 is convergent by A2, A6, Def5; dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1; then dom (f1 + f2) c= dom f1 by XBOOLE_1:17; then A10: rng s1 c= dom f1 by A5, XBOOLE_1:1; then A11: f1 /* s1 is convergent by A1, A6, Def5; then (f1 /* s1) + (f2 /* s1) is convergent by A9, NORMSP_1:19; hence (f1 + f2) /* s1 is convergent by A7, Th12; ::_thesis: (f1 + f2) /. x0 = lim ((f1 + f2) /* s1) A12: f1 /. x0 = lim (f1 /* s1) by A1, A6, A10, Def5; A13: f2 /. x0 = lim (f2 /* s1) by A2, A6, A8, Def5; thus (f1 + f2) /. x0 = (f1 /. x0) + (f2 /. x0) by A4, VFUNCT_1:def_1 .= lim ((f1 /* s1) + (f2 /* s1)) by A11, A12, A9, A13, NORMSP_1:25 .= lim ((f1 + f2) /* s1) by A7, Th12 ; ::_thesis: verum end; hence f1 + f2 is_continuous_in x0 by Def5; ::_thesis: f1 - f2 is_continuous_in x0 now__::_thesis:_(_x0_in_dom_(f1_-_f2)_&_(_for_s1_being_sequence_of_S_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)_)_)_) x0 in (dom f1) /\ (dom f2) by A3, XBOOLE_0:def_4; hence A14: x0 in dom (f1 - f2) by VFUNCT_1:def_2; ::_thesis: for s1 being sequence of S 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 sequence of S; ::_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 A15: rng s1 c= dom (f1 - f2) and A16: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) ) A17: rng s1 c= (dom f1) /\ (dom f2) by A15, VFUNCT_1:def_2; dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2; then dom (f1 - f2) c= dom f2 by XBOOLE_1:17; then A18: rng s1 c= dom f2 by A15, XBOOLE_1:1; then A19: f2 /* s1 is convergent by A2, A16, Def5; dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2; then dom (f1 - f2) c= dom f1 by XBOOLE_1:17; then A20: rng s1 c= dom f1 by A15, XBOOLE_1:1; then A21: f1 /* s1 is convergent by A1, A16, Def5; then (f1 /* s1) - (f2 /* s1) is convergent by A19, NORMSP_1:20; hence (f1 - f2) /* s1 is convergent by A17, Th12; ::_thesis: (f1 - f2) /. x0 = lim ((f1 - f2) /* s1) A22: f1 /. x0 = lim (f1 /* s1) by A1, A16, A20, Def5; A23: f2 /. x0 = lim (f2 /* s1) by A2, A16, A18, Def5; thus (f1 - f2) /. x0 = (f1 /. x0) - (f2 /. x0) by A14, VFUNCT_1:def_2 .= lim ((f1 /* s1) - (f2 /* s1)) by A21, A22, A19, A23, NORMSP_1:26 .= lim ((f1 - f2) /* s1) by A17, Th12 ; ::_thesis: verum end; hence f1 - f2 is_continuous_in x0 by Def5; ::_thesis: verum end; theorem Th16: :: NFCONT_1:16 for r being Real for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds r (#) f is_continuous_in x0 proof let r be Real; ::_thesis: for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let x0 be Point 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 Def5; hence A2: x0 in dom (r (#) f) by VFUNCT_1:def_4; :: according to NFCONT_1:def_5 ::_thesis: for s1 being sequence of S 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 sequence of S; ::_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, Def5; A7: f /* s1 is convergent by A1, A4, A5, Def5; then r * (f /* s1) is convergent by NORMSP_1:22; hence (r (#) f) /* s1 is convergent by A5, Th13; ::_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, Th13 ; ::_thesis: verum end; theorem :: NFCONT_1:17 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S st f is_continuous_in x0 holds ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st f is_continuous_in x0 holds ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) let x0 be Point of S; ::_thesis: ( f is_continuous_in x0 implies ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) ) assume A1: f is_continuous_in x0 ; ::_thesis: ( ||.f.|| is_continuous_in x0 & - f is_continuous_in x0 ) then A2: x0 in dom f by Def5; now__::_thesis:_(_x0_in_dom_||.f.||_&_(_for_s1_being_sequence_of_S_st_rng_s1_c=_dom_||.f.||_&_s1_is_convergent_&_lim_s1_=_x0_holds_ (_||.f.||_/*_s1_is_convergent_&_||.f.||_/._x0_=_lim_(||.f.||_/*_s1)_)_)_) thus A3: x0 in dom ||.f.|| by A2, NORMSP_0:def_3; ::_thesis: for s1 being sequence of S 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 sequence of S; ::_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 A1, A5, Def5; A8: f /* s1 is convergent by A1, A5, A6, Def5; then ||.(f /* s1).|| is convergent by NORMSP_1:23; hence ||.f.|| /* s1 is convergent by A6, Th14; ::_thesis: ||.f.|| /. x0 = lim (||.f.|| /* s1) thus ||.f.|| /. x0 = ||.f.|| . x0 by A3, PARTFUN1:def_6 .= ||.(f /. x0).|| by A3, NORMSP_0:def_3 .= lim ||.(f /* s1).|| by A8, A7, LOPBAN_1:41 .= lim (||.f.|| /* s1) by A6, Th14 ; ::_thesis: verum end; hence ||.f.|| is_continuous_in x0 by Def6; ::_thesis: - f is_continuous_in x0 - f = (- 1) (#) f by VFUNCT_1:23; hence - f is_continuous_in x0 by A1, Th16; ::_thesis: verum end; definition let S, T be RealNormSpace; let f be PartFunc of S,T; let X be set ; predf is_continuous_on X means :Def7: :: NFCONT_1:def 7 ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ); end; :: deftheorem Def7 defines is_continuous_on NFCONT_1:def_7_:_ for S, T being RealNormSpace for f being PartFunc of S,T for X being set holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ) ); definition let S be RealNormSpace; let f be PartFunc of the carrier of S,REAL; let X be set ; predf is_continuous_on X means :Def8: :: NFCONT_1:def 8 ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ); end; :: deftheorem Def8 defines is_continuous_on NFCONT_1:def_8_:_ for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for X being set holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 ) ) ); theorem Th18: :: NFCONT_1:18 for T, S being RealNormSpace for X being set for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 T, S be RealNormSpace; ::_thesis: for X being set for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 S,T; ::_thesis: ( f is_continuous_on X iff ( X c= dom f & ( for s1 being sequence of S 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 is_continuous_on X implies ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) ) ::_thesis: ( X c= dom f & ( for s1 being sequence of S 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 is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) then A2: X c= dom f by Def7; now__::_thesis:_for_s1_being_sequence_of_S_st_rng_s1_c=_X_&_s1_is_convergent_&_lim_s1_in_X_holds_ (_f_/*_s1_is_convergent_&_f_/._(lim_s1)_=_lim_(f_/*_s1)_) let s1 be sequence of S; ::_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: f | X is_continuous_in lim s1 by A1, A5, Def7; A7: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A2, XBOOLE_1:28 ; 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 dom s1 = NAT by FUNCT_2:def_1; then A8: s1 . n in rng s1 by FUNCT_1:3; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A3, A7, FUNCT_2:109 .= f /. (s1 . n) by A3, A7, A8, PARTFUN2:15 .= (f /* s1) . n by A2, 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, A7, PARTFUN2:15 .= lim (f /* s1) by A3, A4, A7, A6, A9, Def5 ; hence ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) by A3, A4, A7, A6, A9, Def5; ::_thesis: verum end; hence ( X c= dom f & ( for s1 being sequence of S st rng s1 c= X & s1 is convergent & lim s1 in X holds ( f /* s1 is convergent & f /. (lim s1) = lim (f /* s1) ) ) ) by A1, Def7; ::_thesis: verum end; assume that A10: X c= dom f and A11: for s1 being sequence of S 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 is_continuous_on X now__::_thesis:_for_x1_being_Point_of_S_st_x1_in_X_holds_ f_|_X_is_continuous_in_x1 A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A10, XBOOLE_1:28 ; let x1 be Point of S; ::_thesis: ( x1 in X implies f | X is_continuous_in x1 ) assume A13: x1 in X ; ::_thesis: f | X is_continuous_in x1 now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_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 A14: rng s1 c= dom (f | X) and A15: s1 is convergent and A16: 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 dom s1 = NAT by FUNCT_2:def_1; then A17: s1 . n in rng s1 by FUNCT_1:3; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A14, FUNCT_2:109 .= f /. (s1 . n) by A14, A17, PARTFUN2:15 .= (f /* s1) . n by A10, A12, A14, FUNCT_2:109, XBOOLE_1:1 ; ::_thesis: verum end; then A18: (f | X) /* s1 = f /* s1 by FUNCT_2:63; (f | X) /. (lim s1) = f /. (lim s1) by A13, A12, A16, PARTFUN2:15 .= lim ((f | X) /* s1) by A11, A13, A12, A14, A15, A16, A18 ; hence ( (f | X) /* s1 is convergent & (f | X) /. x1 = lim ((f | X) /* s1) ) by A11, A13, A12, A14, A15, A16, A18; ::_thesis: verum end; hence f | X is_continuous_in x1 by A13, A12, Def5; ::_thesis: verum end; hence f is_continuous_on X by A10, Def7; ::_thesis: verum end; theorem Th19: :: NFCONT_1:19 for X being set for T, S being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) proof let X be set ; ::_thesis: for T, S being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) let f be PartFunc of S,T; ::_thesis: ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) thus ( f is_continuous_on X implies ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) ) ::_thesis: ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) ) hence X c= dom f by Def7; ::_thesis: for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) A2: X c= dom f by A1, Def7; let x0 be Point of S; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) f | X is_continuous_in x0 by A1, A3, Def7; then consider s being Real such that A5: 0 < s and A6: for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r by A4, Th7; take s ; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) thus 0 < s by A5; ::_thesis: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r let x1 be Point of S; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies ||.((f /. x1) - (f /. x0)).|| < r ) assume that A7: x1 in X and A8: ||.(x1 - x0).|| < s ; ::_thesis: ||.((f /. x1) - (f /. x0)).|| < r A9: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A2, XBOOLE_1:28 ; then ||.((f /. x1) - (f /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A7, PARTFUN2:15 .= ||.(((f | X) /. x1) - ((f | X) /. x0)).|| by A3, A9, PARTFUN2:15 ; hence ||.((f /. x1) - (f /. x0)).|| < r by A6, A9, A7, A8; ::_thesis: verum end; assume that A10: X c= dom f and A11: for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r ) ) ; ::_thesis: f is_continuous_on X A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A10, XBOOLE_1:28 ; now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_X_holds_ f_|_X_is_continuous_in_x0 let x0 be Point of S; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 ) assume A13: x0 in X ; ::_thesis: f | X is_continuous_in x0 for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) then consider s being Real such that A14: 0 < s and A15: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A11, A13; take s ; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) ) thus 0 < s by A14; ::_thesis: for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r let x1 be Point of S; ::_thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ) assume that A16: x1 in dom (f | X) and A17: ||.(x1 - x0).|| < s ; ::_thesis: ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r ||.(((f | X) /. x1) - ((f | X) /. x0)).|| = ||.(((f | X) /. x1) - (f /. x0)).|| by A12, A13, PARTFUN2:15 .= ||.((f /. x1) - (f /. x0)).|| by A16, PARTFUN2:15 ; hence ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < r by A12, A15, A16, A17; ::_thesis: verum end; hence f | X is_continuous_in x0 by A12, A13, Th7; ::_thesis: verum end; hence f is_continuous_on X by A10, Def7; ::_thesis: verum end; theorem :: NFCONT_1:20 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) let f be PartFunc of the carrier of S,REAL; ::_thesis: ( f is_continuous_on X iff ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) thus ( f is_continuous_on X implies ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) ) ::_thesis: ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: ( X c= dom f & ( for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) ) hence X c= dom f by Def8; ::_thesis: for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) A2: X c= dom f by A1, Def8; let x0 be Point of S; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) f | X is_continuous_in x0 by A1, A3, Def8; then consider s being Real such that A5: 0 < s and A6: for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r by A4, Th8; take s ; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) thus 0 < s by A5; ::_thesis: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r let x1 be Point of S; ::_thesis: ( x1 in X & ||.(x1 - x0).|| < s implies abs ((f /. x1) - (f /. x0)) < r ) assume that A7: x1 in X and A8: ||.(x1 - x0).|| < s ; ::_thesis: abs ((f /. x1) - (f /. x0)) < r A9: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A2, XBOOLE_1:28 ; then abs ((f /. x1) - (f /. x0)) = abs (((f | X) /. x1) - (f /. x0)) by A7, PARTFUN2:15 .= abs (((f | X) /. x1) - ((f | X) /. x0)) by A3, A9, PARTFUN2:15 ; hence abs ((f /. x1) - (f /. x0)) < r by A6, A9, A7, A8; ::_thesis: verum end; assume that A10: X c= dom f and A11: for x0 being Point of S for r being Real st x0 in X & 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r ) ) ; ::_thesis: f is_continuous_on X A12: dom (f | X) = (dom f) /\ X by PARTFUN2:15 .= X by A10, XBOOLE_1:28 ; now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_X_holds_ f_|_X_is_continuous_in_x0 let x0 be Point of S; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 ) assume A13: x0 in X ; ::_thesis: f | X is_continuous_in x0 for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r ) ) then consider s being Real such that A14: 0 < s and A15: for x1 being Point of S st x1 in X & ||.(x1 - x0).|| < s holds abs ((f /. x1) - (f /. x0)) < r by A11, A13; take s ; ::_thesis: ( 0 < s & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r ) ) thus 0 < s by A14; ::_thesis: for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s holds abs (((f | X) /. x1) - ((f | X) /. x0)) < r let x1 be Point of S; ::_thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < s implies abs (((f | X) /. x1) - ((f | X) /. x0)) < r ) assume that A16: x1 in dom (f | X) and A17: ||.(x1 - x0).|| < s ; ::_thesis: abs (((f | X) /. x1) - ((f | X) /. x0)) < r abs (((f | X) /. x1) - ((f | X) /. x0)) = abs (((f | X) /. x1) - (f /. x0)) by A12, A13, PARTFUN2:15 .= abs ((f /. x1) - (f /. x0)) by A16, PARTFUN2:15 ; hence abs (((f | X) /. x1) - ((f | X) /. x0)) < r by A12, A15, A16, A17; ::_thesis: verum end; hence f | X is_continuous_in x0 by A12, A13, Th8; ::_thesis: verum end; hence f is_continuous_on X by A10, Def8; ::_thesis: verum end; theorem :: NFCONT_1:21 for X being set for S, T being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff f | X is_continuous_on X ) proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T holds ( f is_continuous_on X iff f | X is_continuous_on X ) let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T holds ( f is_continuous_on X iff f | X is_continuous_on X ) let f be PartFunc of S,T; ::_thesis: ( f is_continuous_on X iff f | X is_continuous_on X ) thus ( f is_continuous_on X implies f | X is_continuous_on X ) ::_thesis: ( f | X is_continuous_on X implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: f | X is_continuous_on X then X c= dom f by Def7; then X c= (dom f) /\ X by XBOOLE_1:28; hence X c= dom (f | X) by RELAT_1:61; :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in X holds (f | X) | X is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X implies (f | X) | X is_continuous_in r ) assume r in X ; ::_thesis: (f | X) | X is_continuous_in r then f | X is_continuous_in r by A1, Def7; hence (f | X) | X is_continuous_in r by RELAT_1:72; ::_thesis: verum end; assume A2: f | X is_continuous_on X ; ::_thesis: f is_continuous_on X then X c= dom (f | X) by Def7; then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17; hence X c= dom f by XBOOLE_1:1; :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X implies f | X is_continuous_in r ) assume r in X ; ::_thesis: f | X is_continuous_in r then (f | X) | X is_continuous_in r by A2, Def7; hence f | X is_continuous_in r by RELAT_1:72; ::_thesis: verum end; theorem Th22: :: NFCONT_1:22 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff f | X is_continuous_on X ) proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff f | X is_continuous_on X ) let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL holds ( f is_continuous_on X iff f | X is_continuous_on X ) let f be PartFunc of the carrier of S,REAL; ::_thesis: ( f is_continuous_on X iff f | X is_continuous_on X ) thus ( f is_continuous_on X implies f | X is_continuous_on X ) ::_thesis: ( f | X is_continuous_on X implies f is_continuous_on X ) proof assume A1: f is_continuous_on X ; ::_thesis: f | X is_continuous_on X then X c= dom f by Def8; then X c= (dom f) /\ X by XBOOLE_1:28; hence X c= dom (f | X) by RELAT_1:61; :: according to NFCONT_1:def_8 ::_thesis: for x0 being Point of S st x0 in X holds (f | X) | X is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X implies (f | X) | X is_continuous_in r ) assume r in X ; ::_thesis: (f | X) | X is_continuous_in r then f | X is_continuous_in r by A1, Def8; hence (f | X) | X is_continuous_in r by RELAT_1:72; ::_thesis: verum end; assume A2: f | X is_continuous_on X ; ::_thesis: f is_continuous_on X then X c= dom (f | X) by Def8; then ( (dom f) /\ X c= dom f & X c= (dom f) /\ X ) by RELAT_1:61, XBOOLE_1:17; hence X c= dom f by XBOOLE_1:1; :: according to NFCONT_1:def_8 ::_thesis: for x0 being Point of S st x0 in X holds f | X is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X implies f | X is_continuous_in r ) assume r in X ; ::_thesis: f | X is_continuous_in r then (f | X) | X is_continuous_in r by A2, Def8; hence f | X is_continuous_in r by RELAT_1:72; ::_thesis: verum end; theorem Th23: :: NFCONT_1:23 for X, X1 being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_continuous_on X & X1 c= X holds f is_continuous_on X1 let f be PartFunc of S,T; ::_thesis: ( f is_continuous_on X & X1 c= X implies f is_continuous_on X1 ) assume that A1: f is_continuous_on X and A2: X1 c= X ; ::_thesis: f is_continuous_on X1 X c= dom f by A1, Def7; hence A3: X1 c= dom f by A2, XBOOLE_1:1; :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in X1 holds f | X1 is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X1 implies f | X1 is_continuous_in r ) assume A4: r in X1 ; ::_thesis: f | X1 is_continuous_in r then A5: f | X is_continuous_in r by A1, A2, Def7; thus f | X1 is_continuous_in r ::_thesis: verum proof (dom f) /\ X1 c= (dom f) /\ X by A2, XBOOLE_1:26; then dom (f | X1) c= (dom f) /\ X by RELAT_1:61; then A6: dom (f | X1) c= dom (f | X) by RELAT_1:61; r in (dom f) /\ X1 by A3, A4, XBOOLE_0:def_4; hence A7: r in dom (f | X1) by RELAT_1:61; :: according to NFCONT_1:def_5 ::_thesis: for s1 being sequence of S st rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = r holds ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) then A8: (f | X) /. r = f /. r by A6, PARTFUN2:15 .= (f | X1) /. r by A7, PARTFUN2:15 ; let s1 be sequence of S; ::_thesis: ( rng s1 c= dom (f | X1) & s1 is convergent & lim s1 = r implies ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) ) assume that A9: rng s1 c= dom (f | X1) and A10: ( s1 is convergent & lim s1 = r ) ; ::_thesis: ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) A11: rng s1 c= dom (f | X) by A9, A6, XBOOLE_1:1; A12: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f_|_X)_/*_s1)_._n_=_((f_|_X1)_/*_s1)_._n let n be Element of NAT ; ::_thesis: ((f | X) /* s1) . n = ((f | X1) /* s1) . n dom s1 = NAT by FUNCT_2:def_1; then A13: s1 . n in rng s1 by FUNCT_1:3; thus ((f | X) /* s1) . n = (f | X) /. (s1 . n) by A9, A6, FUNCT_2:109, XBOOLE_1:1 .= f /. (s1 . n) by A11, A13, PARTFUN2:15 .= (f | X1) /. (s1 . n) by A9, A13, PARTFUN2:15 .= ((f | X1) /* s1) . n by A9, FUNCT_2:109 ; ::_thesis: verum end; ( (f | X) /* s1 is convergent & (f | X) /. r = lim ((f | X) /* s1) ) by A5, A10, A11, Def5; hence ( (f | X1) /* s1 is convergent & (f | X1) /. r = lim ((f | X1) /* s1) ) by A8, A12, FUNCT_2:63; ::_thesis: verum end; end; theorem :: NFCONT_1:24 for T, S being RealNormSpace for f being PartFunc of S,T for x0 being Point of S st x0 in dom f holds f is_continuous_on {x0} proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for x0 being Point of S st x0 in dom f holds f is_continuous_on {x0} let f be PartFunc of S,T; ::_thesis: for x0 being Point of S st x0 in dom f holds f is_continuous_on {x0} let x0 be Point of S; ::_thesis: ( x0 in dom f implies f is_continuous_on {x0} ) assume A1: x0 in dom f ; ::_thesis: f is_continuous_on {x0} thus {x0} c= dom f :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in {x0} holds f | {x0} is_continuous_in x0 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {x0} or x in dom f ) assume x in {x0} ; ::_thesis: x in dom f hence x in dom f by A1, TARSKI:def_1; ::_thesis: verum end; let p be Point of S; ::_thesis: ( p in {x0} implies f | {x0} is_continuous_in p ) assume A2: p in {x0} ; ::_thesis: f | {x0} is_continuous_in p thus f | {x0} is_continuous_in p ::_thesis: verum proof p in dom f by A1, A2, TARSKI:def_1; then p in (dom f) /\ {x0} by A2, XBOOLE_0:def_4; hence p in dom (f | {x0}) by RELAT_1:61; :: according to NFCONT_1:def_5 ::_thesis: for s1 being sequence of S st rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = p holds ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* s1) ) let s1 be sequence of S; ::_thesis: ( rng s1 c= dom (f | {x0}) & s1 is convergent & lim s1 = p implies ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* s1) ) ) assume that A3: rng s1 c= dom (f | {x0}) and s1 is convergent and lim s1 = p ; ::_thesis: ( (f | {x0}) /* s1 is convergent & (f | {x0}) /. p = lim ((f | {x0}) /* s1) ) A4: (dom f) /\ {x0} c= {x0} by XBOOLE_1:17; rng s1 c= (dom f) /\ {x0} by A3, RELAT_1:61; then A5: rng s1 c= {x0} by A4, XBOOLE_1:1; A6: now__::_thesis:_for_n_being_Element_of_NAT_holds_s1_._n_=_x0 let n be Element of NAT ; ::_thesis: s1 . n = x0 dom s1 = NAT by FUNCT_2:def_1; then s1 . n in rng s1 by FUNCT_1:3; hence s1 . n = x0 by A5, TARSKI:def_1; ::_thesis: verum end; A7: p = x0 by A2, TARSKI:def_1; A8: 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 A9: 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 A7, A3, FUNCT_2:109 .= ||.(((f | {x0}) /. x0) - ((f | {x0}) /. x0)).|| by A6 .= ||.(0. T).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.((((f | {x0}) /* s1) . m) - ((f | {x0}) /. p)).|| < g by A9; ::_thesis: verum end; hence (f | {x0}) /* s1 is convergent by NORMSP_1:def_6; ::_thesis: (f | {x0}) /. p = lim ((f | {x0}) /* s1) hence (f | {x0}) /. p = lim ((f | {x0}) /* s1) by A8, NORMSP_1:def_7; ::_thesis: verum end; end; theorem Th25: :: NFCONT_1:25 for T, S being RealNormSpace for X being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) proof let T, S be RealNormSpace; ::_thesis: for X being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) let X be set ; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X holds ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X implies ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) ) assume A1: ( f1 is_continuous_on X & f2 is_continuous_on X ) ; ::_thesis: ( f1 + f2 is_continuous_on X & f1 - f2 is_continuous_on X ) then ( X c= dom f1 & X c= dom f2 ) by Th18; then A2: X c= (dom f1) /\ (dom f2) by XBOOLE_1:19; then A3: X c= dom (f1 + f2) by VFUNCT_1:def_1; now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_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 A4: rng s1 c= X and A5: 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 A1, A4, A5, A6, Th18; then A8: (f1 /* s1) + (f2 /* s1) is convergent by NORMSP_1:19; A9: rng s1 c= (dom f1) /\ (dom f2) by A2, A4, XBOOLE_1:1; ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A4, A5, A6, Th18; then (f1 + f2) /. (lim s1) = (lim (f1 /* s1)) + (lim (f2 /* s1)) by A3, A6, VFUNCT_1:def_1 .= lim ((f1 /* s1) + (f2 /* s1)) by A7, NORMSP_1:25 .= lim ((f1 + f2) /* s1) by A9, Th12 ; hence ( (f1 + f2) /* s1 is convergent & (f1 + f2) /. (lim s1) = lim ((f1 + f2) /* s1) ) by A9, A8, Th12; ::_thesis: verum end; hence f1 + f2 is_continuous_on X by A3, Th18; ::_thesis: f1 - f2 is_continuous_on X A10: X c= dom (f1 - f2) by A2, VFUNCT_1:def_2; now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_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 A11: rng s1 c= X and A12: s1 is convergent and A13: lim s1 in X ; ::_thesis: ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) A14: ( f1 /* s1 is convergent & f2 /* s1 is convergent ) by A1, A11, A12, A13, Th18; then A15: (f1 /* s1) - (f2 /* s1) is convergent by NORMSP_1:20; A16: rng s1 c= (dom f1) /\ (dom f2) by A2, A11, XBOOLE_1:1; ( f1 /. (lim s1) = lim (f1 /* s1) & f2 /. (lim s1) = lim (f2 /* s1) ) by A1, A11, A12, A13, Th18; then (f1 - f2) /. (lim s1) = (lim (f1 /* s1)) - (lim (f2 /* s1)) by A10, A13, VFUNCT_1:def_2 .= lim ((f1 /* s1) - (f2 /* s1)) by A14, NORMSP_1:26 .= lim ((f1 - f2) /* s1) by A16, Th12 ; hence ( (f1 - f2) /* s1 is convergent & (f1 - f2) /. (lim s1) = lim ((f1 - f2) /* s1) ) by A16, A15, Th12; ::_thesis: verum end; hence f1 - f2 is_continuous_on X by A10, Th18; ::_thesis: verum end; theorem :: NFCONT_1:26 for T, S being RealNormSpace for X, X1 being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) proof let T, S be RealNormSpace; ::_thesis: for X, X1 being set for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_continuous_on X & f2 is_continuous_on X1 holds ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_continuous_on X & f2 is_continuous_on X1 implies ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) ) assume ( f1 is_continuous_on X & f2 is_continuous_on X1 ) ; ::_thesis: ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) then ( f1 is_continuous_on X /\ X1 & f2 is_continuous_on X /\ X1 ) by Th23, XBOOLE_1:17; hence ( f1 + f2 is_continuous_on X /\ X1 & f1 - f2 is_continuous_on X /\ X1 ) by Th25; ::_thesis: verum end; theorem Th27: :: NFCONT_1:27 for T, S being RealNormSpace for r being Real for X being set for f being PartFunc of S,T st f is_continuous_on X holds r (#) f is_continuous_on X proof let T, S be RealNormSpace; ::_thesis: for r being Real for X being set for f being PartFunc of S,T st f is_continuous_on X holds r (#) f is_continuous_on X let r be Real; ::_thesis: for X being set for f being PartFunc of S,T st f is_continuous_on X holds r (#) f is_continuous_on X let X be set ; ::_thesis: for f being PartFunc of S,T st f is_continuous_on X holds r (#) f is_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_continuous_on X implies r (#) f is_continuous_on X ) assume A1: f is_continuous_on X ; ::_thesis: r (#) f is_continuous_on X then A2: X c= dom f by Th18; then A3: X c= dom (r (#) f) by VFUNCT_1:def_4; now__::_thesis:_for_s1_being_sequence_of_S_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 sequence of S; ::_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 and A5: s1 is convergent and A6: lim s1 in X ; ::_thesis: ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) A7: f /* s1 is convergent by A1, A4, A5, A6, Th18; then A8: r * (f /* s1) is convergent by NORMSP_1:22; f /. (lim s1) = lim (f /* s1) by A1, A4, A5, A6, Th18; then (r (#) f) /. (lim s1) = r * (lim (f /* s1)) by A3, A6, VFUNCT_1:def_4 .= lim (r * (f /* s1)) by A7, NORMSP_1:28 .= lim ((r (#) f) /* s1) by A2, A4, Th13, XBOOLE_1:1 ; hence ( (r (#) f) /* s1 is convergent & (r (#) f) /. (lim s1) = lim ((r (#) f) /* s1) ) by A2, A4, A8, Th13, XBOOLE_1:1; ::_thesis: verum end; hence r (#) f is_continuous_on X by A3, Th18; ::_thesis: verum end; theorem Th28: :: NFCONT_1:28 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X holds ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_continuous_on X holds ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_continuous_on X holds ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) let f be PartFunc of S,T; ::_thesis: ( f is_continuous_on X implies ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) ) assume A1: f is_continuous_on X ; ::_thesis: ( ||.f.|| is_continuous_on X & - f is_continuous_on X ) thus ||.f.|| is_continuous_on X ::_thesis: - f is_continuous_on X proof A2: X c= dom f by A1, Def7; hence A3: X c= dom ||.f.|| by NORMSP_0:def_3; :: according to NFCONT_1:def_8 ::_thesis: for x0 being Point of S st x0 in X holds ||.f.|| | X is_continuous_in x0 let r be Point of S; ::_thesis: ( r in X implies ||.f.|| | X is_continuous_in r ) assume A4: r in X ; ::_thesis: ||.f.|| | X is_continuous_in r then A5: f | X is_continuous_in r by A1, Def7; thus ||.f.|| | X is_continuous_in r ::_thesis: verum proof A6: r in (dom ||.f.||) /\ X by A3, A4, XBOOLE_0:def_4; hence r in dom (||.f.|| | X) by RELAT_1:61; :: according to NFCONT_1:def_6 ::_thesis: for s1 being sequence of S st rng s1 c= dom (||.f.|| | X) & s1 is convergent & lim s1 = r holds ( (||.f.|| | X) /* s1 is convergent & (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) ) let s1 be sequence of S; ::_thesis: ( rng s1 c= dom (||.f.|| | X) & s1 is convergent & lim s1 = r implies ( (||.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; then A10: (f | X) /. r = lim ((f | X) /* s1) by A5, A8, Def5; 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 dom s1 = NAT by FUNCT_2:def_1; then A11: s1 . n in rng s1 by FUNCT_1:3; then s1 . n in dom (f | X) by A9; then A12: s1 . n in (dom f) /\ X by RELAT_1:61; then A13: s1 . n in X by XBOOLE_0:def_4; s1 . n in dom f by A12, XBOOLE_0:def_4; then A14: 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, A11, PARTFUN2:15 .= ||.f.|| . (s1 . n) by A14, NORMSP_0:def_3 .= (||.f.|| | X) . (s1 . n) by A13, FUNCT_1:49 .= (||.f.|| | X) /. (s1 . n) by A7, A11, PARTFUN1:def_6 .= ((||.f.|| | X) /* s1) . n by A7, FUNCT_2:109 ; ::_thesis: verum end; then A15: ||.((f | X) /* s1).|| = (||.f.|| | X) /* s1 by FUNCT_2:63; A16: (f | X) /* s1 is convergent by A5, A8, A9, Def5; hence (||.f.|| | X) /* s1 is convergent by A15, NORMSP_1:23; ::_thesis: (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) ||.((f | X) /. r).|| = ||.(f /. r).|| by A2, A4, PARTFUN2:17 .= ||.f.|| . r by A3, A4, NORMSP_0:def_3 .= ||.f.|| /. r by A3, A4, PARTFUN1:def_6 .= (||.f.|| | X) /. r by A6, PARTFUN2:16 ; hence (||.f.|| | X) /. r = lim ((||.f.|| | X) /* s1) by A16, A10, A15, LOPBAN_1:20; ::_thesis: verum end; end; (- 1) (#) f is_continuous_on X by A1, Th27; hence - f is_continuous_on X by VFUNCT_1:23; ::_thesis: verum end; theorem :: NFCONT_1:29 for T, S being RealNormSpace for f being PartFunc of S,T st f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 holds f is_continuous_on the carrier of S proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 holds f is_continuous_on the carrier of S let f be PartFunc of S,T; ::_thesis: ( f is total & ( for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of S st f is_continuous_in x0 implies f is_continuous_on the carrier of S ) assume that A1: f is total and A2: for x1, x2 being Point of S holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ; ::_thesis: ( for x0 being Point of S holds not f is_continuous_in x0 or f is_continuous_on the carrier of S ) A3: dom f = the carrier of S by A1, PARTFUN1:def_2; given x0 being Point of S such that A4: f is_continuous_in x0 ; ::_thesis: f is_continuous_on the carrier of S (f /. x0) + (0. T) = f /. x0 by RLVECT_1:4 .= f /. (x0 + (0. S)) by RLVECT_1:4 .= (f /. x0) + (f /. (0. S)) by A2 ; then A5: f /. (0. S) = 0. T by RLVECT_1:8; A6: now__::_thesis:_for_x1_being_Point_of_S_holds_-_(f_/._x1)_=_f_/._(-_x1) let x1 be Point of S; ::_thesis: - (f /. x1) = f /. (- x1) 0. T = f /. (x1 + (- x1)) by A5, RLVECT_1:5 .= (f /. x1) + (f /. (- x1)) by A2 ; hence - (f /. x1) = f /. (- x1) by RLVECT_1:6; ::_thesis: verum end; A7: now__::_thesis:_for_x1,_x2_being_Point_of_S_holds_f_/._(x1_-_x2)_=_(f_/._x1)_-_(f_/._x2) let x1, x2 be Point of S; ::_thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2) thus f /. (x1 - x2) = (f /. x1) + (f /. (- x2)) by A2 .= (f /. x1) - (f /. x2) by A6 ; ::_thesis: verum end; now__::_thesis:_for_x1_being_Point_of_S for_r_being_Real_st_x1_in_the_carrier_of_S_&_r_>_0_holds_ ex_s_being_Real_st_ (_s_>_0_&_(_for_x2_being_Point_of_S_st_x2_in_the_carrier_of_S_&_||.(x2_-_x1).||_<_s_holds_ ||.((f_/._x2)_-_(f_/._x1)).||_<_r_)_) let x1 be Point of S; ::_thesis: for r being Real st x1 in the carrier of S & r > 0 holds ex s being Real st ( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds ||.((f /. x2) - (f /. x1)).|| < r ) ) let r be Real; ::_thesis: ( x1 in the carrier of S & r > 0 implies ex s being Real st ( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds ||.((f /. x2) - (f /. x1)).|| < r ) ) ) assume that x1 in the carrier of S and A8: r > 0 ; ::_thesis: ex s being Real st ( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds ||.((f /. x2) - (f /. x1)).|| < r ) ) set y = x1 - x0; consider s being Real such that A9: 0 < s and A10: for x1 being Point of S st x1 in dom f & ||.(x1 - x0).|| < s holds ||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th7; take s = s; ::_thesis: ( s > 0 & ( for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds ||.((f /. x2) - (f /. x1)).|| < r ) ) thus s > 0 by A9; ::_thesis: for x2 being Point of S st x2 in the carrier of S & ||.(x2 - x1).|| < s holds ||.((f /. x2) - (f /. x1)).|| < r let x2 be Point of S; ::_thesis: ( x2 in the carrier of S & ||.(x2 - x1).|| < s implies ||.((f /. x2) - (f /. x1)).|| < r ) assume that x2 in the carrier of S and A11: ||.(x2 - x1).|| < s ; ::_thesis: ||.((f /. x2) - (f /. x1)).|| < r A12: (x1 - x0) + x0 = x1 - (x0 - x0) by RLVECT_1:29 .= x1 - (0. S) by RLVECT_1:15 .= x1 by RLVECT_1:13 ; then A13: ||.((x2 - (x1 - x0)) - x0).|| = ||.(x2 - x1).|| by RLVECT_1:27; ||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).|| by A2, A12 .= ||.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|| by RLVECT_1:27 .= ||.((f /. (x2 - (x1 - x0))) - (f /. x0)).|| by A7 ; hence ||.((f /. x2) - (f /. x1)).|| < r by A3, A10, A11, A13; ::_thesis: verum end; hence f is_continuous_on the carrier of S by A3, Th19; ::_thesis: verum end; theorem Th30: :: NFCONT_1:30 for T, S being RealNormSpace for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds rng f is compact proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T st dom f is compact & f is_continuous_on dom f holds rng f is compact let f be PartFunc of S,T; ::_thesis: ( dom f is compact & f is_continuous_on dom f implies rng f is compact ) assume that A1: dom f is compact and A2: f is_continuous_on dom f ; ::_thesis: rng f is compact now__::_thesis:_for_s1_being_sequence_of_T_st_rng_s1_c=_rng_f_holds_ ex_q2_being_Element_of_K6(K7(NAT,_the_carrier_of_T))_st_ (_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_) let s1 be sequence of T; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of K6(K7(NAT, the carrier of T)) 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 K6(K7(NAT, the carrier of T)) 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 Point of S st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Point of S 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 Point of S 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 sequence of S 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 Th6; 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 sequence of S such that A8: s2 is subsequence of q1 and A9: s2 is convergent and A10: lim s2 in dom f by A1, Def2; 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; f | (dom f) is_continuous_in lim s2 by A2, A10, Def7; then A13: f is_continuous_in lim s2 by RELAT_1:68; then f /. (lim s2) = lim (f /* s2) by A9, A11, Def5; hence ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A12, A8, A9, A10, A13, A11, Def5, PARTFUN2:2, VALUED_0:22; ::_thesis: verum end; hence rng f is compact by Def2; ::_thesis: verum end; theorem Th31: :: NFCONT_1:31 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds rng f is compact proof let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st dom f is compact & f is_continuous_on dom f holds rng f is compact let f be PartFunc of the carrier of S,REAL; ::_thesis: ( dom f is compact & f is_continuous_on dom f implies rng f is compact ) assume that A1: dom f is compact and A2: f is_continuous_on dom f ; ::_thesis: rng f is compact now__::_thesis:_for_s1_being_Real_Sequence_st_rng_s1_c=_rng_f_holds_ ex_q2_being_Element_of_K6(K7(NAT,REAL))_st_ (_q2_is_subsequence_of_s1_&_q2_is_convergent_&_lim_q2_in_rng_f_) let s1 be Real_Sequence; ::_thesis: ( rng s1 c= rng f implies ex q2 being Element of K6(K7(NAT,REAL)) 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 K6(K7(NAT,REAL)) 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 Point of S st S1[n,p] proof let n be Element of NAT ; ::_thesis: ex p being Point of S 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 Point of S 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 sequence of S 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 Th6; 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 sequence of S such that A8: s2 is subsequence of q1 and A9: s2 is convergent and A10: lim s2 in dom f by A1, Def2; 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; f | (dom f) is_continuous_in lim s2 by A2, A10, Def8; then A13: f is_continuous_in lim s2 by RELAT_1:68; then f /. (lim s2) = lim (f /* s2) by A9, A11, Def6; hence ( q2 is subsequence of s1 & q2 is convergent & lim q2 in rng f ) by A7, A12, A8, A9, A10, A13, A11, Def6, PARTFUN2:2, VALUED_0:22; ::_thesis: verum end; hence rng f is compact by RCOMP_1:def_3; ::_thesis: verum end; theorem :: NFCONT_1:32 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact let f be PartFunc of S,T; ::_thesis: for Y being Subset of S st Y c= dom f & Y is compact & f is_continuous_on Y holds f .: Y is compact let Y be Subset of S; ::_thesis: ( Y c= dom f & Y is compact & f is_continuous_on Y implies f .: Y is compact ) assume that A1: Y c= dom f and A2: Y is compact and A3: f is_continuous_on Y ; ::_thesis: f .: Y is compact A4: dom (f | Y) = (dom f) /\ Y by RELAT_1:61 .= Y by A1, XBOOLE_1:28 ; f | Y is_continuous_on Y proof thus Y c= dom (f | Y) by A4; :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in Y holds (f | Y) | Y is_continuous_in x0 let r be Point of S; ::_thesis: ( r in Y implies (f | Y) | Y is_continuous_in r ) assume r in Y ; ::_thesis: (f | Y) | Y is_continuous_in r then f | Y is_continuous_in r by A3, Def7; hence (f | Y) | Y is_continuous_in r by RELAT_1:72; ::_thesis: verum end; then rng (f | Y) is compact by A2, A4, Th30; hence f .: Y is compact by RELAT_1:115; ::_thesis: verum end; theorem Th33: :: NFCONT_1:33 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) proof let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) let f be PartFunc of the carrier of S,REAL; ::_thesis: ( dom f <> {} & dom f is compact & f is_continuous_on dom f implies ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) ) assume ( dom f <> {} & dom f is compact & f is_continuous_on dom f ) ; ::_thesis: ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & f /. x1 = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) then A1: ( rng f <> {} & rng f is compact ) by Th31, RELAT_1:42; then consider x being Element of S such that A2: ( x in dom f & upper_bound (rng f) = f . x ) by PARTFUN1:3, RCOMP_1:14; take x ; ::_thesis: ex x2 being Point of S st ( x in dom f & x2 in dom f & f /. x = upper_bound (rng f) & f /. x2 = lower_bound (rng f) ) consider y being Element of S such that A3: ( y in dom f & lower_bound (rng f) = f . y ) by A1, PARTFUN1:3, RCOMP_1:14; take y ; ::_thesis: ( x in dom f & y in dom f & f /. x = upper_bound (rng f) & f /. y = lower_bound (rng f) ) thus ( x in dom f & y in dom f & f /. x = upper_bound (rng f) & f /. y = lower_bound (rng f) ) by A2, A3, PARTFUN1:def_6; ::_thesis: verum end; theorem Th34: :: NFCONT_1:34 for T, S being RealNormSpace for f being PartFunc of S,T st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T st dom f <> {} & dom f is compact & f is_continuous_on dom f holds ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) let f be PartFunc of S,T; ::_thesis: ( dom f <> {} & dom f is compact & f is_continuous_on dom f implies ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) ) assume that A1: dom f <> {} and A2: dom f is compact and A3: f is_continuous_on dom f ; ::_thesis: ex x1, x2 being Point of S st ( x1 in dom f & x2 in dom f & ||.f.|| /. x1 = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) A4: dom f = dom ||.f.|| by NORMSP_0:def_3; dom ||.f.|| is compact by A2, NORMSP_0:def_3; then A5: rng ||.f.|| is compact by A3, A4, Th28, Th31; A6: rng ||.f.|| <> {} by A1, A4, RELAT_1:42; then consider x being Element of S such that A7: ( x in dom ||.f.|| & upper_bound (rng ||.f.||) = ||.f.|| . x ) by A5, PARTFUN1:3, RCOMP_1:14; consider y being Element of S such that A8: ( y in dom ||.f.|| & lower_bound (rng ||.f.||) = ||.f.|| . y ) by A6, A5, PARTFUN1:3, RCOMP_1:14; take x ; ::_thesis: ex x2 being Point of S st ( x in dom f & x2 in dom f & ||.f.|| /. x = upper_bound (rng ||.f.||) & ||.f.|| /. x2 = lower_bound (rng ||.f.||) ) take y ; ::_thesis: ( x in dom f & y in dom f & ||.f.|| /. x = upper_bound (rng ||.f.||) & ||.f.|| /. y = lower_bound (rng ||.f.||) ) thus ( x in dom f & y in dom f & ||.f.|| /. x = upper_bound (rng ||.f.||) & ||.f.|| /. y = lower_bound (rng ||.f.||) ) by A7, A8, NORMSP_0:def_3, PARTFUN1:def_6; ::_thesis: verum end; theorem Th35: :: NFCONT_1:35 for X being set for S, T being RealNormSpace for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).|| proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).|| let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T holds ||.f.|| | X = ||.(f | X).|| let f be PartFunc of S,T; ::_thesis: ||.f.|| | X = ||.(f | X).|| A1: dom (||.f.|| | X) = (dom ||.f.||) /\ X by RELAT_1:61 .= (dom f) /\ X by NORMSP_0:def_3 .= dom (f | X) by RELAT_1:61 .= dom ||.(f | X).|| by NORMSP_0:def_3 ; now__::_thesis:_for_c_being_Point_of_S_st_c_in_dom_(||.f.||_|_X)_holds_ (||.f.||_|_X)_._c_=_||.(f_|_X).||_._c let c be Point of S; ::_thesis: ( c in dom (||.f.|| | X) implies (||.f.|| | X) . c = ||.(f | X).|| . c ) assume A2: c in dom (||.f.|| | X) ; ::_thesis: (||.f.|| | X) . c = ||.(f | X).|| . c then A3: c in dom (f | X) by A1, NORMSP_0:def_3; c in (dom ||.f.||) /\ X by A2, RELAT_1:61; then A4: c in dom ||.f.|| by XBOOLE_0:def_4; thus (||.f.|| | X) . c = ||.f.|| . c by A2, FUNCT_1:47 .= ||.(f /. c).|| by A4, NORMSP_0:def_3 .= ||.((f | X) /. c).|| by A3, PARTFUN2:15 .= ||.(f | X).|| . c by A1, A2, NORMSP_0:def_3 ; ::_thesis: verum end; hence ||.f.|| | X = ||.(f | X).|| by A1, PARTFUN1:5; ::_thesis: verum end; theorem :: NFCONT_1:36 for T, S being RealNormSpace for f being PartFunc of S,T for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) let f be PartFunc of S,T; ::_thesis: for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) let Y be Subset of S; ::_thesis: ( Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y implies ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) ) assume that A1: Y <> {} and A2: Y c= dom f and A3: Y is compact and A4: f is_continuous_on Y ; ::_thesis: ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) A5: dom (f | Y) = (dom f) /\ Y by RELAT_1:61 .= Y by A2, XBOOLE_1:28 ; f | Y is_continuous_on Y proof thus Y c= dom (f | Y) by A5; :: according to NFCONT_1:def_7 ::_thesis: for x0 being Point of S st x0 in Y holds (f | Y) | Y is_continuous_in x0 let r be Point of S; ::_thesis: ( r in Y implies (f | Y) | Y is_continuous_in r ) assume r in Y ; ::_thesis: (f | Y) | Y is_continuous_in r then f | Y is_continuous_in r by A4, Def7; hence (f | Y) | Y is_continuous_in r by RELAT_1:72; ::_thesis: verum end; then consider x1, x2 being Point of S such that A6: x1 in dom (f | Y) and A7: x2 in dom (f | Y) and A8: ( ||.(f | Y).|| /. x1 = upper_bound (rng ||.(f | Y).||) & ||.(f | Y).|| /. x2 = lower_bound (rng ||.(f | Y).||) ) by A1, A3, A5, Th34; A9: dom f = dom ||.f.|| by NORMSP_0:def_3; take x1 ; ::_thesis: ex x2 being Point of S st ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) take x2 ; ::_thesis: ( x1 in Y & x2 in Y & ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) thus ( x1 in Y & x2 in Y ) by A5, A6, A7; ::_thesis: ( ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) A10: ||.f.|| .: Y = rng (||.f.|| | Y) by RELAT_1:115 .= rng ||.(f | Y).|| by Th35 ; A11: x2 in dom ||.(f | Y).|| by A7, NORMSP_0:def_3; then A12: ||.(f | Y).|| /. x2 = ||.(f | Y).|| . x2 by PARTFUN1:def_6 .= ||.((f | Y) /. x2).|| by A11, NORMSP_0:def_3 .= ||.(f /. x2).|| by A7, PARTFUN2:15 .= ||.f.|| . x2 by A2, A5, A7, A9, NORMSP_0:def_3 .= ||.f.|| /. x2 by A2, A5, A7, A9, PARTFUN1:def_6 ; A13: x1 in dom ||.(f | Y).|| by A6, NORMSP_0:def_3; then ||.(f | Y).|| /. x1 = ||.(f | Y).|| . x1 by PARTFUN1:def_6 .= ||.((f | Y) /. x1).|| by A13, NORMSP_0:def_3 .= ||.(f /. x1).|| by A6, PARTFUN2:15 .= ||.f.|| . x1 by A2, A5, A6, A9, NORMSP_0:def_3 .= ||.f.|| /. x1 by A2, A5, A6, A9, PARTFUN1:def_6 ; hence ( ||.f.|| /. x1 = upper_bound (||.f.|| .: Y) & ||.f.|| /. x2 = lower_bound (||.f.|| .: Y) ) by A8, A12, A10; ::_thesis: verum end; theorem :: NFCONT_1:37 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) proof let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) let f be PartFunc of the carrier of S,REAL; ::_thesis: for Y being Subset of S st Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y holds ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) let Y be Subset of S; ::_thesis: ( Y <> {} & Y c= dom f & Y is compact & f is_continuous_on Y implies ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) ) assume that A1: Y <> {} and A2: Y c= dom f and A3: Y is compact and A4: f is_continuous_on Y ; ::_thesis: ex x1, x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) A5: dom (f | Y) = (dom f) /\ Y by RELAT_1:61 .= Y by A2, XBOOLE_1:28 ; f | Y is_continuous_on Y proof thus Y c= dom (f | Y) by A5; :: according to NFCONT_1:def_8 ::_thesis: for x0 being Point of S st x0 in Y holds (f | Y) | Y is_continuous_in x0 let r be Point of S; ::_thesis: ( r in Y implies (f | Y) | Y is_continuous_in r ) assume r in Y ; ::_thesis: (f | Y) | Y is_continuous_in r then f | Y is_continuous_in r by A4, Def8; hence (f | Y) | Y is_continuous_in r by RELAT_1:72; ::_thesis: verum end; then consider x1, x2 being Point of S such that A6: ( x1 in dom (f | Y) & x2 in dom (f | Y) ) and A7: ( (f | Y) /. x1 = upper_bound (rng (f | Y)) & (f | Y) /. x2 = lower_bound (rng (f | Y)) ) by A1, A3, A5, Th33; take x1 ; ::_thesis: ex x2 being Point of S st ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) take x2 ; ::_thesis: ( x1 in Y & x2 in Y & f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) thus ( x1 in Y & x2 in Y ) by A5, A6; ::_thesis: ( f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) ( (f | Y) /. x1 = f /. x1 & (f | Y) /. x2 = f /. x2 ) by A6, PARTFUN2:15; hence ( f /. x1 = upper_bound (f .: Y) & f /. x2 = lower_bound (f .: Y) ) by A7, RELAT_1:115; ::_thesis: verum end; definition let S, T be RealNormSpace; let X be set ; let f be PartFunc of S,T; predf is_Lipschitzian_on X means :Def9: :: NFCONT_1:def 9 ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ); end; :: deftheorem Def9 defines is_Lipschitzian_on NFCONT_1:def_9_:_ for S, T being RealNormSpace for X being set for f being PartFunc of S,T holds ( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ) ); definition let S be RealNormSpace; let X be set ; let f be PartFunc of the carrier of S,REAL; predf is_Lipschitzian_on X means :Def10: :: NFCONT_1:def 10 ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ); end; :: deftheorem Def10 defines is_Lipschitzian_on NFCONT_1:def_10_:_ for S being RealNormSpace for X being set for f being PartFunc of the carrier of S,REAL holds ( f is_Lipschitzian_on X iff ( X c= dom f & ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| ) ) ) ); theorem Th38: :: NFCONT_1:38 for X, X1 being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds f is_Lipschitzian_on X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds f is_Lipschitzian_on X1 let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_Lipschitzian_on X & X1 c= X holds f is_Lipschitzian_on X1 let f be PartFunc of S,T; ::_thesis: ( f is_Lipschitzian_on X & X1 c= X implies f is_Lipschitzian_on X1 ) assume that A1: f is_Lipschitzian_on X and A2: X1 c= X ; ::_thesis: f is_Lipschitzian_on X1 X c= dom f by A1, Def9; hence X1 c= dom f by A2, XBOOLE_1:1; :: according to NFCONT_1:def_9 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| ) ) consider s being Real such that A3: 0 < s and A4: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| by A1, Def9; take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X1 & x2 in X1 holds ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| ) ) thus 0 < s by A3; ::_thesis: for x1, x2 being Point of S st x1 in X1 & x2 in X1 holds ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X1 & x2 in X1 implies ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| ) assume ( x1 in X1 & x2 in X1 ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| hence ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| by A2, A4; ::_thesis: verum end; theorem :: NFCONT_1:39 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 + f2 is_Lipschitzian_on X /\ X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 + f2 is_Lipschitzian_on X /\ X1 let S, T be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 + f2 is_Lipschitzian_on X /\ X1 let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1 + f2 is_Lipschitzian_on X /\ X1 ) assume that A1: f1 is_Lipschitzian_on X and A2: f2 is_Lipschitzian_on X1 ; ::_thesis: f1 + f2 is_Lipschitzian_on X /\ X1 A3: f1 is_Lipschitzian_on X /\ X1 by A1, Th38, XBOOLE_1:17; then consider s being Real such that A4: 0 < s and A5: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| by Def9; A6: f2 is_Lipschitzian_on X /\ X1 by A2, Th38, XBOOLE_1:17; then A7: X /\ X1 c= dom f2 by Def9; X /\ X1 c= dom f1 by A3, Def9; then X /\ X1 c= (dom f1) /\ (dom f2) by A7, XBOOLE_1:19; hence A8: X /\ X1 c= dom (f1 + f2) by VFUNCT_1:def_1; :: according to NFCONT_1:def_9 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) consider g being Real such that A9: 0 < g and A10: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| by A6, Def9; take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) ) 0 + 0 < s + g by A4, A9, XREAL_1:8; hence 0 < p ; ::_thesis: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 implies ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) assume that A11: x1 in X /\ X1 and A12: x2 in X /\ X1 ; ::_thesis: ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| A13: ||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| by A10, A11, A12; ||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| by A5, A11, A12; then A14: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||) by A13, XREAL_1:7; ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| = ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 + f2) /. x2)).|| by A8, A11, VFUNCT_1:def_1 .= ||.(((f1 /. x1) + (f2 /. x1)) - ((f1 /. x2) + (f2 /. x2))).|| by A8, A12, VFUNCT_1:def_1 .= ||.((f1 /. x1) + ((f2 /. x1) - ((f1 /. x2) + (f2 /. x2)))).|| by RLVECT_1:def_3 .= ||.((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:def_3 .= ||.(((f1 /. x1) - (f1 /. x2)) + ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:def_3 ; then ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:def_1; hence ||.(((f1 + f2) /. x1) - ((f1 + f2) /. x2)).|| <= p * ||.(x1 - x2).|| by A14, XXREAL_0:2; ::_thesis: verum end; theorem :: NFCONT_1:40 for X, X1 being set for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 - f2 is_Lipschitzian_on X /\ X1 proof let X, X1 be set ; ::_thesis: for S, T being RealNormSpace for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 - f2 is_Lipschitzian_on X /\ X1 let S, T be RealNormSpace; ::_thesis: for f1, f2 being PartFunc of S,T st f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 holds f1 - f2 is_Lipschitzian_on X /\ X1 let f1, f2 be PartFunc of S,T; ::_thesis: ( f1 is_Lipschitzian_on X & f2 is_Lipschitzian_on X1 implies f1 - f2 is_Lipschitzian_on X /\ X1 ) assume that A1: f1 is_Lipschitzian_on X and A2: f2 is_Lipschitzian_on X1 ; ::_thesis: f1 - f2 is_Lipschitzian_on X /\ X1 A3: f1 is_Lipschitzian_on X /\ X1 by A1, Th38, XBOOLE_1:17; then consider s being Real such that A4: 0 < s and A5: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| by Def9; A6: f2 is_Lipschitzian_on X /\ X1 by A2, Th38, XBOOLE_1:17; then A7: X /\ X1 c= dom f2 by Def9; X /\ X1 c= dom f1 by A3, Def9; then X /\ X1 c= (dom f1) /\ (dom f2) by A7, XBOOLE_1:19; hence A8: X /\ X1 c= dom (f1 - f2) by VFUNCT_1:def_2; :: according to NFCONT_1:def_9 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) consider g being Real such that A9: 0 < g and A10: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| by A6, Def9; take p = s + g; ::_thesis: ( 0 < p & ( for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) ) 0 + 0 < s + g by A4, A9, XREAL_1:8; hence 0 < p ; ::_thesis: for x1, x2 being Point of S st x1 in X /\ X1 & x2 in X /\ X1 holds ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X /\ X1 & x2 in X /\ X1 implies ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| ) assume that A11: x1 in X /\ X1 and A12: x2 in X /\ X1 ; ::_thesis: ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| A13: ||.((f2 /. x1) - (f2 /. x2)).|| <= g * ||.(x1 - x2).|| by A10, A11, A12; ||.((f1 /. x1) - (f1 /. x2)).|| <= s * ||.(x1 - x2).|| by A5, A11, A12; then A14: ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| <= (s * ||.(x1 - x2).||) + (g * ||.(x1 - x2).||) by A13, XREAL_1:7; ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| = ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 - f2) /. x2)).|| by A8, A11, VFUNCT_1:def_2 .= ||.(((f1 /. x1) - (f2 /. x1)) - ((f1 /. x2) - (f2 /. x2))).|| by A8, 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:def_3 .= ||.((f1 /. x1) - ((f1 /. x2) + ((f2 /. x1) - (f2 /. x2)))).|| by RLVECT_1:def_3 .= ||.(((f1 /. x1) - (f1 /. x2)) - ((f2 /. x1) - (f2 /. x2))).|| by RLVECT_1:27 ; then ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= ||.((f1 /. x1) - (f1 /. x2)).|| + ||.((f2 /. x1) - (f2 /. x2)).|| by NORMSP_1:3; hence ||.(((f1 - f2) /. x1) - ((f1 - f2) /. x2)).|| <= p * ||.(x1 - x2).|| by A14, XXREAL_0:2; ::_thesis: verum end; theorem Th41: :: NFCONT_1:41 for X being set for p being Real for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds p (#) f is_Lipschitzian_on X proof let X be set ; ::_thesis: for p being Real for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds p (#) f is_Lipschitzian_on X let p be Real; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds p (#) f is_Lipschitzian_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_Lipschitzian_on X holds p (#) f is_Lipschitzian_on X let f be PartFunc of S,T; ::_thesis: ( f is_Lipschitzian_on X implies p (#) f is_Lipschitzian_on X ) assume A1: f is_Lipschitzian_on X ; ::_thesis: p (#) f is_Lipschitzian_on X then consider s being Real such that A2: 0 < s and A3: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| by Def9; X c= dom f by A1, Def9; hence A4: X c= dom (p (#) f) by VFUNCT_1:def_4; :: according to NFCONT_1:def_9 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) now__::_thesis:_ex_s_being_Real_st_ (_0_<_s_&_(_for_x1,_x2_being_Point_of_S_st_x1_in_X_&_x2_in_X_holds_ ||.(((p_(#)_f)_/._x1)_-_((p_(#)_f)_/._x2)).||_<=_s_*_||.(x1_-_x2).||_)_) percases ( p = 0 or p <> 0 ) ; supposeA5: p = 0 ; ::_thesis: ex s being Real st ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| ) ) take s = s; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| ) ) thus 0 < s by A2; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| ) assume that A6: x1 in X and A7: x2 in X ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| 0 <= ||.(x1 - x2).|| by NORMSP_1:4; then A8: s * 0 <= s * ||.(x1 - x2).|| by A2, XREAL_1:64; ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, A6, VFUNCT_1:def_4 .= ||.((0. T) - ((p (#) f) /. x2)).|| by A5, RLVECT_1:10 .= ||.((0. T) - (p * (f /. x2))).|| by A4, A7, VFUNCT_1:def_4 .= ||.((0. T) - (0. T)).|| by A5, RLVECT_1:10 .= ||.(0. T).|| by RLVECT_1:13 .= 0 by NORMSP_1:1 ; hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= s * ||.(x1 - x2).|| by A8; ::_thesis: verum end; supposeA9: p <> 0 ; ::_thesis: ex g being Element of REAL st ( 0 < g & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| ) ) take g = (abs p) * s; ::_thesis: ( 0 < g & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| ) ) 0 < abs p by A9, COMPLEX1:47; then 0 * s < (abs p) * s by A2, XREAL_1:68; hence 0 < g ; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X implies ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| ) assume that A10: x1 in X and A11: x2 in X ; ::_thesis: ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| 0 <= abs p by COMPLEX1:46; then A12: (abs p) * ||.((f /. x1) - (f /. x2)).|| <= (abs p) * (s * ||.(x1 - x2).||) by A3, A10, A11, XREAL_1:64; ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| = ||.((p * (f /. x1)) - ((p (#) f) /. x2)).|| by A4, A10, VFUNCT_1:def_4 .= ||.((p * (f /. x1)) - (p * (f /. x2))).|| by A4, A11, VFUNCT_1:def_4 .= ||.(p * ((f /. x1) - (f /. x2))).|| by RLVECT_1:34 .= (abs p) * ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:def_1 ; hence ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= g * ||.(x1 - x2).|| by A12; ::_thesis: verum end; end; end; hence ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds ||.(((p (#) f) /. x1) - ((p (#) f) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) ; ::_thesis: verum end; theorem :: NFCONT_1:42 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_Lipschitzian_on X holds ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) let f be PartFunc of S,T; ::_thesis: ( f is_Lipschitzian_on X implies ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) ) assume A1: f is_Lipschitzian_on X ; ::_thesis: ( - f is_Lipschitzian_on X & ||.f.|| is_Lipschitzian_on X ) then consider s being Real such that A2: 0 < s and A3: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| by Def9; - f = (- 1) (#) f by VFUNCT_1:23; hence - f is_Lipschitzian_on X by A1, Th41; ::_thesis: ||.f.|| is_Lipschitzian_on X X c= dom f by A1, Def9; hence A4: X c= dom ||.f.|| by NORMSP_0:def_3; :: according to NFCONT_1:def_10 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= r * ||.(x1 - x2).|| ) ) take s ; ::_thesis: ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= s * ||.(x1 - x2).|| ) ) thus 0 < s by A2; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= s * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X implies abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= s * ||.(x1 - x2).|| ) assume that A5: x1 in X and A6: x2 in X ; ::_thesis: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= s * ||.(x1 - x2).|| abs ((||.f.|| /. x1) - (||.f.|| /. x2)) = abs ((||.f.|| . x1) - (||.f.|| /. x2)) by A4, A5, PARTFUN1:def_6 .= abs ((||.f.|| . x1) - (||.f.|| . x2)) by A4, A6, PARTFUN1:def_6 .= abs (||.(f /. x1).|| - (||.f.|| . x2)) by A4, A5, NORMSP_0:def_3 .= abs (||.(f /. x1).|| - ||.(f /. x2).||) by A4, A6, NORMSP_0:def_3 ; then A7: abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= ||.((f /. x1) - (f /. x2)).|| by NORMSP_1:9; ||.((f /. x1) - (f /. x2)).|| <= s * ||.(x1 - x2).|| by A3, A5, A6; hence abs ((||.f.|| /. x1) - (||.f.|| /. x2)) <= s * ||.(x1 - x2).|| by A7, XXREAL_0:2; ::_thesis: verum end; theorem Th43: :: NFCONT_1:43 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_Lipschitzian_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_Lipschitzian_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_Lipschitzian_on X let f be PartFunc of S,T; ::_thesis: ( X c= dom f & f | X is V23() implies f is_Lipschitzian_on X ) assume that A1: X c= dom f and A2: f | X is V23() ; ::_thesis: f is_Lipschitzian_on X now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_X_&_x2_in_X_holds_ ||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ) assume that A3: x1 in X and A4: x2 in X ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| A5: ( x1 in X /\ (dom f) & x2 in X /\ (dom f) ) by A1, A3, A4, XBOOLE_0:def_4; f /. x1 = f . x1 by A1, A3, PARTFUN1:def_6 .= f . x2 by A2, A5, PARTFUN2:58 .= f /. x2 by A1, A4, PARTFUN1:def_6 ; then ||.((f /. x1) - (f /. x2)).|| = ||.(0. T).|| by RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by NORMSP_1:4; ::_thesis: verum end; hence f is_Lipschitzian_on X by A1, Def9; ::_thesis: verum end; theorem :: NFCONT_1:44 for S being RealNormSpace for Y being Subset of S holds id Y is_Lipschitzian_on Y proof let S be RealNormSpace; ::_thesis: for Y being Subset of S holds id Y is_Lipschitzian_on Y let Y be Subset of S; ::_thesis: id Y is_Lipschitzian_on Y reconsider r = 1 as Real ; thus Y c= dom (id Y) by RELAT_1:45; :: according to NFCONT_1:def_9 ::_thesis: ex r being Real st ( 0 < r & ( for x1, x2 being Point of S st x1 in Y & x2 in Y holds ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) take r ; ::_thesis: ( 0 < r & ( for x1, x2 being Point of S st x1 in Y & x2 in Y holds ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) ) thus r > 0 ; ::_thesis: for x1, x2 being Point of S st x1 in Y & x2 in Y holds ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in Y & x2 in Y implies ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ) assume that A1: x1 in Y and A2: x2 in Y ; ::_thesis: ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ||.(((id Y) /. x1) - ((id Y) /. x2)).|| = ||.(x1 - ((id Y) /. x2)).|| by A1, PARTFUN2:6 .= r * ||.(x1 - x2).|| by A2, PARTFUN2:6 ; hence ||.(((id Y) /. x1) - ((id Y) /. x2)).|| <= r * ||.(x1 - x2).|| ; ::_thesis: verum end; theorem Th45: :: NFCONT_1:45 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for S, T being RealNormSpace for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_continuous_on X let S, T be RealNormSpace; ::_thesis: for f being PartFunc of S,T st f is_Lipschitzian_on X holds f is_continuous_on X let f be PartFunc of S,T; ::_thesis: ( f is_Lipschitzian_on X implies f is_continuous_on X ) assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_continuous_on X then consider r being Real such that A2: 0 < r and A3: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| by Def9; A4: X c= dom f by A1, Def9; then A5: dom (f | X) = X by RELAT_1:62; now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_X_holds_ f_|_X_is_continuous_in_x0 let x0 be Point of S; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 ) assume A6: x0 in X ; ::_thesis: f | X is_continuous_in x0 now__::_thesis:_for_g_being_Real_st_0_<_g_holds_ ex_s9_being_Element_of_REAL_st_ (_0_<_s9_&_(_for_x1_being_Point_of_S_st_x1_in_dom_(f_|_X)_&_||.(x1_-_x0).||_<_s9_holds_ ||.(((f_|_X)_/._x1)_-_((f_|_X)_/._x0)).||_<_g_)_) let g be Real; ::_thesis: ( 0 < g implies ex s9 being Element of REAL st ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) ) assume A7: 0 < g ; ::_thesis: ex s9 being Element of REAL st ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) set s = g / r; take s9 = g / r; ::_thesis: ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) A8: now__::_thesis:_for_x1_being_Point_of_S_st_x1_in_dom_(f_|_X)_&_||.(x1_-_x0).||_<_g_/_r_holds_ ||.(((f_|_X)_/._x1)_-_((f_|_X)_/._x0)).||_<_g let x1 be Point of S; ::_thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < g / r implies ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) assume that A9: x1 in dom (f | X) and A10: ||.(x1 - x0).|| < g / r ; ::_thesis: ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g r * ||.(x1 - x0).|| < (g / r) * r by A2, A10, XREAL_1:68; then A11: r * ||.(x1 - x0).|| < g by A2, XCMPLX_1:87; ||.((f /. x1) - (f /. x0)).|| <= r * ||.(x1 - x0).|| by A3, A5, A6, A9; then ||.((f /. x1) - (f /. x0)).|| < g by A11, XXREAL_0:2; then ||.(((f | X) /. x1) - (f /. x0)).|| < g by A9, PARTFUN2:15; hence ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g by A5, A6, PARTFUN2:15; ::_thesis: verum end; ( 0 < r " & s9 = g * (r ") ) by A2, XCMPLX_0:def_9, XREAL_1:122; hence ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds ||.(((f | X) /. x1) - ((f | X) /. x0)).|| < g ) ) by A7, A8, XREAL_1:129; ::_thesis: verum end; hence f | X is_continuous_in x0 by A5, A6, Th7; ::_thesis: verum end; hence f is_continuous_on X by A4, Def7; ::_thesis: verum end; theorem Th46: :: NFCONT_1:46 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds f is_continuous_on X proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds f is_continuous_on X let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st f is_Lipschitzian_on X holds f is_continuous_on X let f be PartFunc of the carrier of S,REAL; ::_thesis: ( f is_Lipschitzian_on X implies f is_continuous_on X ) assume A1: f is_Lipschitzian_on X ; ::_thesis: f is_continuous_on X then consider r being Real such that A2: 0 < r and A3: for x1, x2 being Point of S st x1 in X & x2 in X holds abs ((f /. x1) - (f /. x2)) <= r * ||.(x1 - x2).|| by Def10; A4: X c= dom f by A1, Def10; then A5: dom (f | X) = X by RELAT_1:62; now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_X_holds_ f_|_X_is_continuous_in_x0 let x0 be Point of S; ::_thesis: ( x0 in X implies f | X is_continuous_in x0 ) assume A6: x0 in X ; ::_thesis: f | X is_continuous_in x0 now__::_thesis:_for_g_being_Real_st_0_<_g_holds_ ex_s9_being_Element_of_REAL_st_ (_0_<_s9_&_(_for_x1_being_Point_of_S_st_x1_in_dom_(f_|_X)_&_||.(x1_-_x0).||_<_s9_holds_ abs_(((f_|_X)_/._x1)_-_((f_|_X)_/._x0))_<_g_)_) let g be Real; ::_thesis: ( 0 < g implies ex s9 being Element of REAL st ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds abs (((f | X) /. x1) - ((f | X) /. x0)) < g ) ) ) assume A7: 0 < g ; ::_thesis: ex s9 being Element of REAL st ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds abs (((f | X) /. x1) - ((f | X) /. x0)) < g ) ) set s = g / r; take s9 = g / r; ::_thesis: ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds abs (((f | X) /. x1) - ((f | X) /. x0)) < g ) ) A8: now__::_thesis:_for_x1_being_Point_of_S_st_x1_in_dom_(f_|_X)_&_||.(x1_-_x0).||_<_g_/_r_holds_ abs_(((f_|_X)_/._x1)_-_((f_|_X)_/._x0))_<_g let x1 be Point of S; ::_thesis: ( x1 in dom (f | X) & ||.(x1 - x0).|| < g / r implies abs (((f | X) /. x1) - ((f | X) /. x0)) < g ) assume that A9: x1 in dom (f | X) and A10: ||.(x1 - x0).|| < g / r ; ::_thesis: abs (((f | X) /. x1) - ((f | X) /. x0)) < g r * ||.(x1 - x0).|| < (g / r) * r by A2, A10, XREAL_1:68; then A11: r * ||.(x1 - x0).|| < g by A2, XCMPLX_1:87; abs ((f /. x1) - (f /. x0)) <= r * ||.(x1 - x0).|| by A3, A5, A6, A9; then abs ((f /. x1) - (f /. x0)) < g by A11, XXREAL_0:2; then abs (((f | X) /. x1) - (f /. x0)) < g by A9, PARTFUN2:15; hence abs (((f | X) /. x1) - ((f | X) /. x0)) < g by A5, A6, PARTFUN2:15; ::_thesis: verum end; ( 0 < r " & s9 = g * (r ") ) by A2, XCMPLX_0:def_9, XREAL_1:122; hence ( 0 < s9 & ( for x1 being Point of S st x1 in dom (f | X) & ||.(x1 - x0).|| < s9 holds abs (((f | X) /. x1) - ((f | X) /. x0)) < g ) ) by A7, A8, XREAL_1:129; ::_thesis: verum end; hence f | X is_continuous_in x0 by A5, A6, Th8; ::_thesis: verum end; hence f is_continuous_on X by A4, Def8; ::_thesis: verum end; theorem :: NFCONT_1:47 for T, S being RealNormSpace for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds f is_continuous_on dom f proof let T, S be RealNormSpace; ::_thesis: for f being PartFunc of S,T st ex r being Point of T st rng f = {r} holds f is_continuous_on dom f let f be PartFunc of S,T; ::_thesis: ( ex r being Point of T st rng f = {r} implies f is_continuous_on dom f ) given r being Point of T such that A1: rng f = {r} ; ::_thesis: f is_continuous_on dom f now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_dom_f_&_x2_in_dom_f_holds_ ||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ) assume that A2: x1 in dom f and A3: x2 in dom f ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| f . x2 in rng f by A3, FUNCT_1:def_3; then f /. x2 in rng f by A3, PARTFUN1:def_6; then A4: 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. T).|| by A4, RLVECT_1:15 .= 0 by NORMSP_1:1 ; hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by NORMSP_1:4; ::_thesis: verum end; then f is_Lipschitzian_on dom f by Def9; hence f is_continuous_on dom f by Th45; ::_thesis: verum end; theorem :: NFCONT_1:48 for X being set for S, T being RealNormSpace for f being PartFunc of S,T st X c= dom f & f | X is V23() holds f is_continuous_on X by Th43, Th45; theorem Th49: :: NFCONT_1:49 for S being RealNormSpace for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds f /. x0 = x0 ) holds f is_continuous_on dom f proof let S be RealNormSpace; ::_thesis: for f being PartFunc of S,S st ( for x0 being Point of S st x0 in dom f holds f /. x0 = x0 ) holds f is_continuous_on dom f let f be PartFunc of S,S; ::_thesis: ( ( for x0 being Point of S st x0 in dom f holds f /. x0 = x0 ) implies f is_continuous_on dom f ) assume A1: for x0 being Point of S st x0 in dom f holds f /. x0 = x0 ; ::_thesis: f is_continuous_on dom f now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_dom_f_&_x2_in_dom_f_holds_ ||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in dom f & x2 in dom f implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ) assume that A2: x1 in dom f and A3: x2 in dom f ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| f /. x1 = x1 by A1, A2; hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by A1, A3; ::_thesis: verum end; then f is_Lipschitzian_on dom f by Def9; hence f is_continuous_on dom f by Th45; ::_thesis: verum end; theorem :: NFCONT_1:50 for S being RealNormSpace for f being PartFunc of S,S st f = id (dom f) holds f is_continuous_on dom f proof let S be RealNormSpace; ::_thesis: for f being PartFunc of S,S st f = id (dom f) holds f is_continuous_on dom f let f be PartFunc of S,S; ::_thesis: ( f = id (dom f) implies f is_continuous_on dom f ) assume A1: f = id (dom f) ; ::_thesis: f is_continuous_on dom f now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_dom_f_holds_ f_/._x0_=_x0 let x0 be Point of S; ::_thesis: ( x0 in dom f implies f /. x0 = x0 ) assume A2: x0 in dom f ; ::_thesis: f /. x0 = x0 thus f /. x0 = f . x0 by A2, PARTFUN1:def_6 .= x0 by A1, A2, FUNCT_1:17 ; ::_thesis: verum end; hence f is_continuous_on dom f by Th49; ::_thesis: verum end; theorem :: NFCONT_1:51 for S being RealNormSpace for Y being Subset of S for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds f is_continuous_on Y proof let S be RealNormSpace; ::_thesis: for Y being Subset of S for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds f is_continuous_on Y let Y be Subset of S; ::_thesis: for f being PartFunc of S,S st Y c= dom f & f | Y = id Y holds f is_continuous_on Y let f be PartFunc of S,S; ::_thesis: ( Y c= dom f & f | Y = id Y implies f is_continuous_on Y ) assume that A1: Y c= dom f and A2: f | Y = id Y ; ::_thesis: f is_continuous_on Y now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_Y_&_x2_in_Y_holds_ ||.((f_/._x1)_-_(f_/._x2)).||_<=_1_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in Y & x2 in Y implies ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| ) assume that A3: x1 in Y and A4: x2 in Y ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| x1 in (dom f) /\ Y by A1, A3, XBOOLE_0:def_4; then A5: x1 in dom (f | Y) by RELAT_1:61; (f | Y) . x1 = x1 by A2, A3, FUNCT_1:17; then f . x1 = x1 by A5, FUNCT_1:47; then A6: f /. x1 = x1 by A1, A3, PARTFUN1:def_6; x2 in (dom f) /\ Y by A1, A4, XBOOLE_0:def_4; then A7: x2 in dom (f | Y) by RELAT_1:61; (f | Y) . x2 = x2 by A2, A4, FUNCT_1:17; then f . x2 = x2 by A7, FUNCT_1:47; hence ||.((f /. x1) - (f /. x2)).|| <= 1 * ||.(x1 - x2).|| by A1, A4, A6, PARTFUN1:def_6; ::_thesis: verum end; then f is_Lipschitzian_on Y by A1, Def9; hence f is_continuous_on Y by Th45; ::_thesis: verum end; theorem :: NFCONT_1:52 for X being set for S being RealNormSpace for f being PartFunc of S,S for r being Real for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of S,S for r being Real for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X let S be RealNormSpace; ::_thesis: for f being PartFunc of S,S for r being Real for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X let f be PartFunc of S,S; ::_thesis: for r being Real for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X let r be Real; ::_thesis: for p being Point of S st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) holds f is_continuous_on X let p be Point of S; ::_thesis: ( X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ) implies f is_continuous_on X ) assume that A1: X c= dom f and A2: for x0 being Point of S st x0 in X holds f /. x0 = (r * x0) + p ; ::_thesis: f is_continuous_on X now__::_thesis:_(_0_<_(abs_r)_+_1_&_(_for_x1,_x2_being_Point_of_S_st_x1_in_X_&_x2_in_X_holds_ ||.((f_/._x1)_-_(f_/._x2)).||_<=_((abs_r)_+_1)_*_||.(x1_-_x2).||_)_) 0 + 0 < (abs r) + 1 by COMPLEX1:46, XREAL_1:8; hence 0 < (abs r) + 1 ; ::_thesis: for x1, x2 being Point of S st x1 in X & x2 in X holds ||.((f /. x1) - (f /. x2)).|| <= ((abs r) + 1) * ||.(x1 - x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in X & x2 in X implies ||.((f /. x1) - (f /. x2)).|| <= ((abs r) + 1) * ||.(x1 - x2).|| ) assume ( x1 in X & x2 in X ) ; ::_thesis: ||.((f /. x1) - (f /. x2)).|| <= ((abs r) + 1) * ||.(x1 - x2).|| then ( f /. x1 = (r * x1) + p & f /. x2 = (r * x2) + p ) by A2; then A3: ||.((f /. x1) - (f /. x2)).|| = ||.((r * x1) + (p - (p + (r * x2)))).|| by RLVECT_1:def_3 .= ||.((r * x1) + ((p - p) - (r * x2))).|| by RLVECT_1:27 .= ||.((r * x1) + ((0. S) - (r * x2))).|| by RLVECT_1:15 .= ||.((r * x1) - (r * x2)).|| by RLVECT_1:14 .= ||.(r * (x1 - x2)).|| by RLVECT_1:34 .= (abs r) * ||.(x1 - x2).|| by NORMSP_1:def_1 ; 0 <= ||.(x1 - x2).|| by NORMSP_1:4; then ||.((f /. x1) - (f /. x2)).|| + 0 <= ((abs r) * ||.(x1 - x2).||) + (1 * ||.(x1 - x2).||) by A3, XREAL_1:7; hence ||.((f /. x1) - (f /. x2)).|| <= ((abs r) + 1) * ||.(x1 - x2).|| ; ::_thesis: verum end; then f is_Lipschitzian_on X by A1, Def9; hence f is_continuous_on X by Th45; ::_thesis: verum end; theorem Th53: :: NFCONT_1:53 for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds f /. x0 = ||.x0.|| ) holds f is_continuous_on dom f proof let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st ( for x0 being Point of S st x0 in dom f holds f /. x0 = ||.x0.|| ) holds f is_continuous_on dom f let f be PartFunc of the carrier of S,REAL; ::_thesis: ( ( for x0 being Point of S st x0 in dom f holds f /. x0 = ||.x0.|| ) implies f is_continuous_on dom f ) assume A1: for x0 being Point of S st x0 in dom f holds f /. x0 = ||.x0.|| ; ::_thesis: f is_continuous_on dom f now__::_thesis:_for_x1,_x2_being_Point_of_S_st_x1_in_dom_f_&_x2_in_dom_f_holds_ abs_((f_/._x1)_-_(f_/._x2))_<=_1_*_||.(x1_-_x2).|| let x1, x2 be Point of S; ::_thesis: ( x1 in dom f & x2 in dom f implies abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).|| ) assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).|| then ( f /. x1 = ||.x1.|| & f /. x2 = ||.x2.|| ) by A1; hence abs ((f /. x1) - (f /. x2)) <= 1 * ||.(x1 - x2).|| by NORMSP_1:9; ::_thesis: verum end; then f is_Lipschitzian_on dom f by Def10; hence f is_continuous_on dom f by Th46; ::_thesis: verum end; theorem :: NFCONT_1:54 for X being set for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ) holds f is_continuous_on X proof let X be set ; ::_thesis: for S being RealNormSpace for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ) holds f is_continuous_on X let S be RealNormSpace; ::_thesis: for f being PartFunc of the carrier of S,REAL st X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ) holds f is_continuous_on X let f be PartFunc of the carrier of S,REAL; ::_thesis: ( X c= dom f & ( for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ) implies f is_continuous_on X ) assume that A1: X c= dom f and A2: for x0 being Point of S st x0 in X holds f /. x0 = ||.x0.|| ; ::_thesis: f is_continuous_on X X = (dom f) /\ X by A1, XBOOLE_1:28; then A3: X = dom (f | X) by RELAT_1:61; now__::_thesis:_for_x0_being_Point_of_S_st_x0_in_dom_(f_|_X)_holds_ (f_|_X)_/._x0_=_||.x0.|| let x0 be Point of S; ::_thesis: ( x0 in dom (f | X) implies (f | X) /. x0 = ||.x0.|| ) assume A4: x0 in dom (f | X) ; ::_thesis: (f | X) /. x0 = ||.x0.|| hence (f | X) /. x0 = f /. x0 by PARTFUN2:15 .= ||.x0.|| by A2, A3, A4 ; ::_thesis: verum end; then f | X is_continuous_on X by A3, Th53; hence f is_continuous_on X by Th22; ::_thesis: verum end;