:: NFCONT_4 semantic presentation begin definition let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); let x0 be real number ; predf is_continuous_in x0 means :Def1: :: NFCONT_4:def 1 ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_continuous_in x0 ); end; :: deftheorem Def1 defines is_continuous_in NFCONT_4:def_1_:_ for n being Element of NAT for f being PartFunc of REAL,(REAL n) for x0 being real number holds ( f is_continuous_in x0 iff ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_continuous_in x0 ) ); theorem Th1: :: NFCONT_4:1 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) st h = f holds ( f is_continuous_in x0 iff h is_continuous_in x0 ) proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) st h = f holds ( f is_continuous_in x0 iff h is_continuous_in x0 ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) st h = f holds ( f is_continuous_in x0 iff h is_continuous_in x0 ) let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st h = f holds ( f is_continuous_in x0 iff h is_continuous_in x0 ) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h = f implies ( f is_continuous_in x0 iff h is_continuous_in x0 ) ) assume A1: h = f ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in x0 ) hereby ::_thesis: ( h is_continuous_in x0 implies f is_continuous_in x0 ) assume f is_continuous_in x0 ; ::_thesis: h is_continuous_in x0 then ex g being PartFunc of REAL,(REAL-NS n) st ( f = g & g is_continuous_in x0 ) by Def1; hence h is_continuous_in x0 by A1; ::_thesis: verum end; thus ( h is_continuous_in x0 implies f is_continuous_in x0 ) by A1, Def1; ::_thesis: verum end; theorem Th2: :: NFCONT_4:2 for n being Element of NAT for X being set for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds f | X is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for X being set for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds f | X is_continuous_in x0 let X be set ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds f | X is_continuous_in x0 let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in X & f is_continuous_in x0 holds f | X is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in X & f is_continuous_in x0 implies f | X is_continuous_in x0 ) assume that A1: x0 in X and A2: f is_continuous_in x0 ; ::_thesis: f | X is_continuous_in x0 consider g being PartFunc of REAL,(REAL-NS n) such that A3: ( f = g & g is_continuous_in x0 ) by A2, Def1; g | X is_continuous_in x0 by A1, A3, NFCONT_3:6; hence f | X is_continuous_in x0 by A3, Def1; ::_thesis: verum end; theorem Th3: :: NFCONT_4:3 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ) hereby ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) implies f is_continuous_in x0 ) assume f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) then consider g being PartFunc of REAL,(REAL-NS n) such that A1: ( f = g & g is_continuous_in x0 ) by Def1; thus x0 in dom f by A1, NFCONT_3:8; ::_thesis: for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) thus for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ::_thesis: verum proof let r be Real; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) assume 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) then consider s being real number such that A2: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds ||.((g /. x1) - (g /. x0)).|| < r ) ) by A1, NFCONT_3:8; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) thus 0 < s by A2; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r ) assume ( x1 in dom f & abs (x1 - x0) < s ) ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r then A3: ||.((g /. x1) - (g /. x0)).|| < r by A1, A2; ( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by A1, REAL_NS1:def_4; hence |.((f /. x1) - (f /. x0)).| < r by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; end; assume A4: ( x0 in dom f & ( for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) ; ::_thesis: f is_continuous_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_real_number_st_ (_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_g_&_abs_(x1_-_x0)_<_s_holds_ ||.((g_/._x1)_-_(g_/._x0)).||_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds ||.((g /. x1) - (g /. x0)).|| < r ) ) ) assume 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds ||.((g /. x1) - (g /. x0)).|| < r ) ) then consider s being real number such that A5: 0 < s and A6: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r by A4; take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds ||.((g /. x1) - (g /. x0)).|| < r ) ) thus 0 < s by A5; ::_thesis: for x1 being real number st x1 in dom g & abs (x1 - x0) < s holds ||.((g /. x1) - (g /. x0)).|| < r let x1 be real number ; ::_thesis: ( x1 in dom g & abs (x1 - x0) < s implies ||.((g /. x1) - (g /. x0)).|| < r ) assume ( x1 in dom g & abs (x1 - x0) < s ) ; ::_thesis: ||.((g /. x1) - (g /. x0)).|| < r then A7: |.((f /. x1) - (f /. x0)).| < r by A6; ( g /. x1 = f /. x1 & g /. x0 = f /. x0 ) by REAL_NS1:def_4; hence ||.((g /. x1) - (g /. x0)).|| < r by A7, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; then g is_continuous_in x0 by A4, NFCONT_3:8; hence f is_continuous_in x0 by Def1; ::_thesis: verum end; theorem Th4: :: NFCONT_4:4 for n being Element of NAT for r being Real for z being Element of REAL n for w being Point of (REAL-NS n) st z = w holds { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } proof let n be Element of NAT ; ::_thesis: for r being Real for z being Element of REAL n for w being Point of (REAL-NS n) st z = w holds { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } let r be Real; ::_thesis: for z being Element of REAL n for w being Point of (REAL-NS n) st z = w holds { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } let z be Element of REAL n; ::_thesis: for w being Point of (REAL-NS n) st z = w holds { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } let w be Point of (REAL-NS n); ::_thesis: ( z = w implies { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ) assume A1: z = w ; ::_thesis: { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } set N1 = { y where y is Element of REAL n : |.(y - z).| < r } ; set N2 = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; A2: { y where y is Element of REAL n : |.(y - z).| < r } c= { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Element of REAL n : |.(y - z).| < r } or x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ) assume x in { y where y is Element of REAL n : |.(y - z).| < r } ; ::_thesis: x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } then consider y being Element of REAL n such that A3: ( x = y & |.(y - z).| < r ) ; reconsider x1 = x as Element of REAL n by A3; reconsider x2 = x1 as Point of (REAL-NS n) by REAL_NS1:def_4; ||.(x2 - w).|| < r by A1, A3, REAL_NS1:1, REAL_NS1:5; hence x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; ::_thesis: verum end; { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } c= { y where y is Element of REAL n : |.(y - z).| < r } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } or x in { y where y is Element of REAL n : |.(y - z).| < r } ) assume x in { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } ; ::_thesis: x in { y where y is Element of REAL n : |.(y - z).| < r } then consider y being Point of (REAL-NS n) such that A4: ( x = y & ||.(y - w).|| < r ) ; reconsider x3 = x as Point of (REAL-NS n) by A4; reconsider x4 = x3 as Element of REAL n by REAL_NS1:def_4; |.(x4 - z).| < r by A1, A4, REAL_NS1:1, REAL_NS1:5; hence x in { y where y is Element of REAL n : |.(y - z).| < r } ; ::_thesis: verum end; hence { y where y is Element of REAL n : |.(y - z).| < r } = { y where y is Point of (REAL-NS n) : ||.(y - w).|| < r } by A2, XBOOLE_0:def_10; ::_thesis: verum end; definition let n be Element of NAT ; let Z be set ; let f be PartFunc of Z,(REAL n); deffunc H1( set ) -> Element of REAL = |.(f /. \$1).|; func|.f.| -> PartFunc of Z,REAL means :Def2: :: NFCONT_4:def 2 ( dom it = dom f & ( for x being set st x in dom it holds it /. x = |.(f /. x).| ) ); existence ex b1 being PartFunc of Z,REAL st ( dom b1 = dom f & ( for x being set st x in dom b1 holds b1 /. x = |.(f /. x).| ) ) proof consider g being Function such that A1: ( dom g = dom f & ( for x being set st x in dom f holds g . x = H1(x) ) ) from FUNCT_1:sch_3(); now__::_thesis:_for_y_being_set_st_y_in_rng_g_holds_ y_in_REAL let y be set ; ::_thesis: ( y in rng g implies y in REAL ) assume y in rng g ; ::_thesis: y in REAL then consider x being set such that A2: ( x in dom g & y = g . x ) by FUNCT_1:def_3; g . x = H1(x) by A1, A2; hence y in REAL by A2; ::_thesis: verum end; then rng g c= REAL by TARSKI:def_3; then g in PFuncs (Z,REAL) by A1, PARTFUN1:def_3; then reconsider g = g as PartFunc of Z,REAL by PARTFUN1:46; take g ; ::_thesis: ( dom g = dom f & ( for x being set st x in dom g holds g /. x = |.(f /. x).| ) ) thus dom g = dom f by A1; ::_thesis: for x being set st x in dom g holds g /. x = |.(f /. x).| let x be set ; ::_thesis: ( x in dom g implies g /. x = |.(f /. x).| ) assume A3: x in dom g ; ::_thesis: g /. x = |.(f /. x).| then g . x = H1(x) by A1; hence g /. x = |.(f /. x).| by A3, PARTFUN1:def_6; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of Z,REAL st dom b1 = dom f & ( for x being set st x in dom b1 holds b1 /. x = |.(f /. x).| ) & dom b2 = dom f & ( for x being set st x in dom b2 holds b2 /. x = |.(f /. x).| ) holds b1 = b2 proof let g1, g2 be PartFunc of Z,REAL; ::_thesis: ( dom g1 = dom f & ( for x being set st x in dom g1 holds g1 /. x = |.(f /. x).| ) & dom g2 = dom f & ( for x being set st x in dom g2 holds g2 /. x = |.(f /. x).| ) implies g1 = g2 ) assume that A4: ( dom g1 = dom f & ( for x being set st x in dom g1 holds g1 /. x = H1(x) ) ) and A5: ( dom g2 = dom f & ( for x being set st x in dom g2 holds g2 /. x = H1(x) ) ) ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_ g1_._x_=_g2_._x let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x ) assume A6: x in dom g1 ; ::_thesis: g1 . x = g2 . x then A7: g1 /. x = |.(f /. x).| by A4; g1 /. x = g2 /. x by A5, A7, A4, A6; then g1 . x = g2 /. x by A6, PARTFUN1:def_6; hence g1 . x = g2 . x by A4, A5, A6, PARTFUN1:def_6; ::_thesis: verum end; hence g1 = g2 by A4, A5, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def2 defines |. NFCONT_4:def_2_:_ for n being Element of NAT for Z being set for f being PartFunc of Z,(REAL n) for b4 being PartFunc of Z,REAL holds ( b4 = |.f.| iff ( dom b4 = dom f & ( for x being set st x in dom b4 holds b4 /. x = |.(f /. x).| ) ) ); definition let n be Element of NAT ; let Z be non empty set ; let f be PartFunc of Z,(REAL n); deffunc H1( set ) -> M13( REAL , REAL n) = - (f /. \$1); defpred S1[ set ] means \$1 in dom f; func - f -> PartFunc of Z,(REAL n) means :Def3: :: NFCONT_4:def 3 ( dom it = dom f & ( for c being set st c in dom it holds it /. c = - (f /. c) ) ); existence ex b1 being PartFunc of Z,(REAL n) st ( dom b1 = dom f & ( for c being set st c in dom b1 holds b1 /. c = - (f /. c) ) ) proof consider F being PartFunc of Z,(REAL n) such that A1: for c being Element of Z holds ( c in dom F iff S1[c] ) and A2: for c being Element of Z st c in dom F holds F /. c = H1(c) from PARTFUN2:sch_2(); take F ; ::_thesis: ( dom F = dom f & ( for c being set st c in dom F holds F /. c = - (f /. c) ) ) thus ( dom F = dom f & ( for c being set st c in dom F holds F /. c = - (f /. c) ) ) by A1, A2, SUBSET_1:3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of Z,(REAL n) st dom b1 = dom f & ( for c being set st c in dom b1 holds b1 /. c = - (f /. c) ) & dom b2 = dom f & ( for c being set st c in dom b2 holds b2 /. c = - (f /. c) ) holds b1 = b2 proof let g1, g2 be PartFunc of Z,(REAL n); ::_thesis: ( dom g1 = dom f & ( for c being set st c in dom g1 holds g1 /. c = - (f /. c) ) & dom g2 = dom f & ( for c being set st c in dom g2 holds g2 /. c = - (f /. c) ) implies g1 = g2 ) assume that A3: ( dom g1 = dom f & ( for x being set st x in dom g1 holds g1 /. x = - (f /. x) ) ) and A4: ( dom g2 = dom f & ( for x being set st x in dom g2 holds g2 /. x = - (f /. x) ) ) ; ::_thesis: g1 = g2 now__::_thesis:_for_x_being_Element_of_Z_st_x_in_dom_g1_holds_ g1_._x_=_g2_._x let x be Element of Z; ::_thesis: ( x in dom g1 implies g1 . x = g2 . x ) assume A5: x in dom g1 ; ::_thesis: g1 . x = g2 . x then A6: g1 /. x = - (f /. x) by A3; g1 /. x = g2 /. x by A4, A6, A3, A5; then g1 . x = g2 /. x by A5, PARTFUN1:def_6; hence g1 . x = g2 . x by A3, A4, A5, PARTFUN1:def_6; ::_thesis: verum end; hence g1 = g2 by A3, A4, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def3 defines - NFCONT_4:def_3_:_ for n being Element of NAT for Z being non empty set for f, b4 being PartFunc of Z,(REAL n) holds ( b4 = - f iff ( dom b4 = dom f & ( for c being set st c in dom b4 holds b4 /. c = - (f /. c) ) ) ); theorem Th5: :: NFCONT_4:5 for n being Element of NAT for W being non empty set for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let W be non empty set ; ::_thesis: for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 + f2 = g1 + g2 let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 + f2 = g1 + g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 + f2 = g1 + g2 A2: dom (f1 + f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_1; then A3: dom (f1 + f2) = dom (g1 + g2) by A1, VALUED_2:def_45; A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_+_f2)_holds_ (f1_+_f2)_._x_=_(g1_+_g2)_._x let x be Element of W; ::_thesis: ( x in dom (f1 + f2) implies (f1 + f2) . x = (g1 + g2) . x ) assume A5: x in dom (f1 + f2) ; ::_thesis: (f1 + f2) . x = (g1 + g2) . x then A6: ( x in dom g1 & x in dom g2 ) by A2, A1, XBOOLE_0:def_4; A7: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4; ( g1 /. x = g1 . x & g2 /. x = g2 . x ) by A6, PARTFUN1:def_6; then A8: (f1 /. x) + (f2 /. x) = (g1 . x) + (g2 . x) by A7, REAL_NS1:2; (f1 + f2) /. x = (f1 /. x) + (f2 /. x) by A5, VFUNCT_1:def_1; then (f1 + f2) . x = (f1 /. x) + (f2 /. x) by A5, PARTFUN1:def_6; hence (f1 + f2) . x = (g1 + g2) . x by A8, A3, A5, VALUED_2:def_45; ::_thesis: verum end; f1 + f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4; hence f1 + f2 = g1 + g2 by A3, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th6: :: NFCONT_4:6 for n being Element of NAT for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) for a being Real st f1 = g1 holds a (#) f1 = a (#) g1 proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) for a being Real st f1 = g1 holds a (#) f1 = a (#) g1 let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) for a being Real st f1 = g1 holds a (#) f1 = a (#) g1 let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) for a being Real st f1 = g1 holds a (#) f1 = a (#) g1 let g1 be PartFunc of W,(REAL n); ::_thesis: for a being Real st f1 = g1 holds a (#) f1 = a (#) g1 let a be Real; ::_thesis: ( f1 = g1 implies a (#) f1 = a (#) g1 ) assume A1: f1 = g1 ; ::_thesis: a (#) f1 = a (#) g1 A2: dom (a (#) f1) = dom f1 by VFUNCT_1:def_4; then A3: dom (a (#) f1) = dom (a (#) g1) by A1, VALUED_2:def_39; A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(a_(#)_f1)_holds_ (a_(#)_f1)_._x_=_(a_(#)_g1)_._x let x be Element of W; ::_thesis: ( x in dom (a (#) f1) implies (a (#) f1) . x = (a (#) g1) . x ) assume A5: x in dom (a (#) f1) ; ::_thesis: (a (#) f1) . x = (a (#) g1) . x then A6: g1 . x = g1 /. x by A1, A2, PARTFUN1:def_6; f1 /. x = g1 /. x by A1, REAL_NS1:def_4; then A7: a * (f1 /. x) = a * (g1 /. x) by REAL_NS1:3; A8: (a (#) f1) /. x = a * (f1 /. x) by A5, VFUNCT_1:def_4; (a (#) g1) . x = a (#) (g1 . x) by A3, A5, VALUED_2:def_39; hence (a (#) f1) . x = (a (#) g1) . x by A5, A7, A8, A6, PARTFUN1:def_6; ::_thesis: verum end; a (#) f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4; hence a (#) f1 = a (#) g1 by A3, A4, PARTFUN1:5; ::_thesis: verum end; theorem :: NFCONT_4:7 for n being Element of NAT for W being non empty set for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1 proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1 let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL n) holds (- 1) (#) f1 = - f1 let f1 be PartFunc of W,(REAL n); ::_thesis: (- 1) (#) f1 = - f1 A1: dom ((- 1) (#) f1) = dom f1 by VALUED_2:def_39; then A2: dom ((- 1) (#) f1) = dom (- f1) by Def3; now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_((-_1)_(#)_f1)_holds_ ((-_1)_(#)_f1)_._x_=_(-_f1)_._x let x be Element of W; ::_thesis: ( x in dom ((- 1) (#) f1) implies ((- 1) (#) f1) . x = (- f1) . x ) assume A3: x in dom ((- 1) (#) f1) ; ::_thesis: ((- 1) (#) f1) . x = (- f1) . x A4: f1 . x = f1 /. x by A1, A3, PARTFUN1:def_6; A5: (- f1) /. x = - (f1 /. x) by A2, A3, Def3; (f1 [#] (- 1)) . x = (- 1) (#) (f1 . x) by A3, VALUED_2:def_39; hence ((- 1) (#) f1) . x = (- f1) . x by A4, A2, A3, A5, PARTFUN1:def_6; ::_thesis: verum end; hence (- 1) (#) f1 = - f1 by A2, PARTFUN1:5; ::_thesis: verum end; theorem Th8: :: NFCONT_4:8 for n being Element of NAT for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds - f1 = - g1 proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds - f1 = - g1 let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds - f1 = - g1 let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds - f1 = - g1 let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies - f1 = - g1 ) assume A1: f1 = g1 ; ::_thesis: - f1 = - g1 dom (- f1) = dom f1 by VFUNCT_1:def_5; then A2: dom (- f1) = dom (- g1) by A1, Def3; A3: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(-_f1)_holds_ (-_f1)_._x_=_(-_g1)_._x let x be Element of W; ::_thesis: ( x in dom (- f1) implies (- f1) . x = (- g1) . x ) assume A4: x in dom (- f1) ; ::_thesis: (- f1) . x = (- g1) . x f1 /. x = g1 /. x by A1, REAL_NS1:def_4; then A5: - (f1 /. x) = - (g1 /. x) by REAL_NS1:4; A6: (- f1) /. x = - (f1 /. x) by A4, VFUNCT_1:def_5; (- g1) /. x = - (g1 /. x) by A2, A4, Def3; then (- f1) . x = (- g1) /. x by A4, A5, A6, PARTFUN1:def_6; hence (- f1) . x = (- g1) . x by A2, A4, PARTFUN1:def_6; ::_thesis: verum end; - f1 is PartFunc of W,(REAL n) by REAL_NS1:def_4; hence - f1 = - g1 by A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem Th9: :: NFCONT_4:9 for n being Element of NAT for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds ||.f1.|| = |.g1.| proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds ||.f1.|| = |.g1.| let W be non empty set ; ::_thesis: for f1 being PartFunc of W,(REAL-NS n) for g1 being PartFunc of W,(REAL n) st f1 = g1 holds ||.f1.|| = |.g1.| let f1 be PartFunc of W,(REAL-NS n); ::_thesis: for g1 being PartFunc of W,(REAL n) st f1 = g1 holds ||.f1.|| = |.g1.| let g1 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 implies ||.f1.|| = |.g1.| ) assume A1: f1 = g1 ; ::_thesis: ||.f1.|| = |.g1.| dom ||.f1.|| = dom f1 by NORMSP_0:def_3; then A2: dom ||.f1.|| = dom |.g1.| by A1, Def2; now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_||.f1.||_holds_ ||.f1.||_._x_=_|.g1.|_._x let x be Element of W; ::_thesis: ( x in dom ||.f1.|| implies ||.f1.|| . x = |.g1.| . x ) assume A3: x in dom ||.f1.|| ; ::_thesis: ||.f1.|| . x = |.g1.| . x A4: f1 /. x = g1 /. x by A1, REAL_NS1:def_4; set y1 = g1 /. x; A5: ||.(f1 /. x).|| = |.(g1 /. x).| by A4, REAL_NS1:1; A6: ||.f1.|| . x = ||.(f1 /. x).|| by A3, NORMSP_0:def_3; |.g1.| /. x = |.(g1 /. x).| by A2, A3, Def2; hence ||.f1.|| . x = |.g1.| . x by A2, A3, A5, A6, PARTFUN1:def_6; ::_thesis: verum end; hence ||.f1.|| = |.g1.| by A2, PARTFUN1:5; ::_thesis: verum end; theorem Th10: :: NFCONT_4:10 for n being Element of NAT for W being non empty set for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 proof let n be Element of NAT ; ::_thesis: for W being non empty set for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let W be non empty set ; ::_thesis: for f1, f2 being PartFunc of W,(REAL-NS n) for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let f1, f2 be PartFunc of W,(REAL-NS n); ::_thesis: for g1, g2 being PartFunc of W,(REAL n) st f1 = g1 & f2 = g2 holds f1 - f2 = g1 - g2 let g1, g2 be PartFunc of W,(REAL n); ::_thesis: ( f1 = g1 & f2 = g2 implies f1 - f2 = g1 - g2 ) assume A1: ( f1 = g1 & f2 = g2 ) ; ::_thesis: f1 - f2 = g1 - g2 A2: dom (f1 - f2) = (dom f1) /\ (dom f2) by VFUNCT_1:def_2; then A3: dom (f1 - f2) = dom (g1 - g2) by A1, VALUED_2:def_46; A4: now__::_thesis:_for_x_being_Element_of_W_st_x_in_dom_(f1_-_f2)_holds_ (f1_-_f2)_._x_=_(g1_-_g2)_._x let x be Element of W; ::_thesis: ( x in dom (f1 - f2) implies (f1 - f2) . x = (g1 - g2) . x ) assume A5: x in dom (f1 - f2) ; ::_thesis: (f1 - f2) . x = (g1 - g2) . x A6: ( f1 /. x = g1 /. x & f2 /. x = g2 /. x ) by A1, REAL_NS1:def_4; ( x in dom f1 & x in dom f2 ) by A5, A2, XBOOLE_0:def_4; then ( g1 . x = g1 /. x & g2 /. x = g2 . x ) by A1, PARTFUN1:def_6; then A7: (f1 /. x) - (f2 /. x) = (g1 . x) - (g2 . x) by A6, REAL_NS1:5; A8: (f1 - f2) /. x = (f1 /. x) - (f2 /. x) by A5, VFUNCT_1:def_2; (f1 - f2) /. x = (f1 - f2) . x by A5, PARTFUN1:def_6; hence (f1 - f2) . x = (g1 - g2) . x by A7, A8, A3, A5, VALUED_2:def_46; ::_thesis: verum end; f1 - f2 is PartFunc of W,(REAL n) by REAL_NS1:def_4; hence f1 - f2 = g1 - g2 by A3, A4, PARTFUN1:5; ::_thesis: verum end; theorem :: NFCONT_4:11 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) thus ( f is_continuous_in x0 implies ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ) ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) implies f is_continuous_in x0 ) proof assume f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) then consider g being PartFunc of REAL,(REAL-NS n) such that A1: ( f = g & g is_continuous_in x0 ) by Def1; thus x0 in dom f by A1, NFCONT_3:9; ::_thesis: for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 let N01 be Subset of (REAL n); ::_thesis: ( ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) implies ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N01 ) assume A2: ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N01 ) ; ::_thesis: ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N01 consider r being Real such that A3: 0 < r and A4: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = N01 by A2; f /. x0 = g /. x0 by A1, REAL_NS1:def_4; then A5: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } = N01 by A4, Th4; { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } is Neighbourhood of g /. x0 by A3, NFCONT_1:3; then consider N being Neighbourhood of x0 such that A6: for x1 being real number st x1 in dom g & x1 in N holds g /. x1 in N01 by A5, A1, NFCONT_3:9; take N ; ::_thesis: for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N01 let x1 be real number ; ::_thesis: ( x1 in dom f & x1 in N implies f /. x1 in N01 ) assume ( x1 in dom f & x1 in N ) ; ::_thesis: f /. x1 in N01 then g /. x1 in N01 by A1, A6; hence f /. x1 in N01 by A1, REAL_NS1:def_4; ::_thesis: verum end; assume A7: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in N1 ) ) ; ::_thesis: f is_continuous_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_ for_x1_being_real_number_st_x1_in_dom_g_&_x1_in_N_holds_ g_/._x1_in_N1 let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st for x1 being real number st x1 in dom g & x1 in N holds g /. x1 in N1 consider r being Real such that A8: 0 < r and A9: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def_1; set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; f /. x0 = g /. x0 by REAL_NS1:def_4; then A10: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4; now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_ x_in_REAL_n let x be set ; ::_thesis: ( x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } implies x in REAL n ) assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; ::_thesis: x in REAL n then ex p being Element of REAL n st ( p = x & |.(p - (f /. x0)).| < r ) ; hence x in REAL n ; ::_thesis: verum end; then { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n) by TARSKI:def_3; then consider N being Neighbourhood of x0 such that A11: for x1 being real number st x1 in dom f & x1 in N holds f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A7, A8; take N = N; ::_thesis: for x1 being real number st x1 in dom g & x1 in N holds g /. x1 in N1 let x1 be real number ; ::_thesis: ( x1 in dom g & x1 in N implies g /. x1 in N1 ) assume ( x1 in dom g & x1 in N ) ; ::_thesis: g /. x1 in N1 then f /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A11; then g /. x1 in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by REAL_NS1:def_4; hence g /. x1 in N1 by A9, A10; ::_thesis: verum end; then g is_continuous_in x0 by A7, NFCONT_3:9; hence f is_continuous_in x0 by Def1; ::_thesis: verum end; theorem :: NFCONT_4:12 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is_continuous_in x0 iff ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; hereby ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) implies f is_continuous_in x0 ) assume f is_continuous_in x0 ; ::_thesis: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) then A1: g is_continuous_in x0 by Th1; hence x0 in dom f by NFCONT_3:10; ::_thesis: for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 thus for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ::_thesis: verum proof let N1 be Subset of (REAL n); ::_thesis: ( ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) implies ex N being Neighbourhood of x0 st f .: N c= N1 ) given r being Real such that A2: ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) ; ::_thesis: ex N being Neighbourhood of x0 st f .: N c= N1 f /. x0 = g /. x0 by REAL_NS1:def_4; then A3: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4; N1 is Neighbourhood of g /. x0 by A2, A3, NFCONT_1:3; then consider N being Neighbourhood of x0 such that A4: g .: N c= N1 by A1, NFCONT_3:10; take N ; ::_thesis: f .: N c= N1 thus f .: N c= N1 by A4; ::_thesis: verum end; end; assume A5: ( x0 in dom f & ( for N1 being Subset of (REAL n) st ex r being Real st ( 0 < r & { y where y is Element of REAL n : |.(y - (f /. x0)).| < r } = N1 ) holds ex N being Neighbourhood of x0 st f .: N c= N1 ) ) ; ::_thesis: f is_continuous_in x0 now__::_thesis:_for_N1_being_Neighbourhood_of_g_/._x0_ex_N_being_Neighbourhood_of_x0_st_g_.:_N_c=_N1 let N1 be Neighbourhood of g /. x0; ::_thesis: ex N being Neighbourhood of x0 st g .: N c= N1 consider r being Real such that A6: 0 < r and A7: { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } c= N1 by NFCONT_1:def_1; set N01 = { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; f /. x0 = g /. x0 by REAL_NS1:def_4; then A8: { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } = { p where p is Point of (REAL-NS n) : ||.(p - (g /. x0)).|| < r } by Th4; now__::_thesis:_for_x_being_set_st_x_in__{__p_where_p_is_Element_of_REAL_n_:_|.(p_-_(f_/._x0)).|_<_r__}__holds_ x_in_REAL_n let x be set ; ::_thesis: ( x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } implies x in REAL n ) assume x in { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } ; ::_thesis: x in REAL n then ex p being Element of REAL n st ( p = x & |.(p - (f /. x0)).| < r ) ; hence x in REAL n ; ::_thesis: verum end; then { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } is Subset of (REAL n) by TARSKI:def_3; then consider N being Neighbourhood of x0 such that A9: f .: N c= { p where p is Element of REAL n : |.(p - (f /. x0)).| < r } by A5, A6; take N = N; ::_thesis: g .: N c= N1 thus g .: N c= N1 by A7, A8, A9, XBOOLE_1:1; ::_thesis: verum end; then g is_continuous_in x0 by A5, NFCONT_3:10; hence f is_continuous_in x0 by Th1; ::_thesis: verum end; theorem :: NFCONT_4:13 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} holds f is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_thesis: ( ex N being Neighbourhood of x0 st (dom f) /\ N = {x0} implies f is_continuous_in x0 ) given N being Neighbourhood of x0 such that A1: (dom f) /\ N = {x0} ; ::_thesis: f is_continuous_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is_continuous_in x0 by A1, NFCONT_3:11; hence f is_continuous_in x0 by Th1; ::_thesis: verum end; theorem :: NFCONT_4:14 for n being Element of NAT for x0 being real number for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 + f2 is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 + f2 is_continuous_in x0 let x0 be real number ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 + f2 is_continuous_in x0 let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 + f2 is_continuous_in x0 ) assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 + f2 is_continuous_in x0 reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: g1 is_continuous_in x0 by A1, Th1; g2 is_continuous_in x0 by A1, Th1; then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12; g1 + g2 = f1 + f2 by Th5; hence f1 + f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum end; theorem :: NFCONT_4:15 for n being Element of NAT for x0 being real number for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 - f2 is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 - f2 is_continuous_in x0 let x0 be real number ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 holds f1 - f2 is_continuous_in x0 let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 implies f1 - f2 is_continuous_in x0 ) assume A1: ( x0 in (dom f1) /\ (dom f2) & f1 is_continuous_in x0 & f2 is_continuous_in x0 ) ; ::_thesis: f1 - f2 is_continuous_in x0 reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: g1 is_continuous_in x0 by A1, Th1; g2 is_continuous_in x0 by A1, Th1; then A3: ( g1 + g2 is_continuous_in x0 & g1 - g2 is_continuous_in x0 ) by A1, A2, NFCONT_3:12; g1 - g2 = f1 - f2 by Th10; hence f1 - f2 is_continuous_in x0 by A3, Th1; ::_thesis: verum end; theorem :: NFCONT_4:16 for n being Element of NAT for r being Real for x0 being real number for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds r (#) f is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for r being Real for x0 being real number for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let r be Real; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is_continuous_in x0 holds r (#) f is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_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 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is_continuous_in x0 by A1, Th1; then A2: r (#) g is_continuous_in x0 by NFCONT_3:13; r (#) g = r (#) f by Th6; hence r (#) f is_continuous_in x0 by A2, Th1; ::_thesis: verum end; theorem :: NFCONT_4:17 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds |.f.| is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds |.f.| is_continuous_in x0 let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds |.f.| is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies |.f.| is_continuous_in x0 ) assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: |.f.| is_continuous_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is_continuous_in x0 by A1, Th1; then ||.g.|| is_continuous_in x0 by A1, NFCONT_3:14; hence |.f.| is_continuous_in x0 by Th9; ::_thesis: verum end; theorem :: NFCONT_4:18 for n being Element of NAT for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds - f is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds - f is_continuous_in x0 let x0 be real number ; ::_thesis: for f being PartFunc of REAL,(REAL n) st x0 in dom f & f is_continuous_in x0 holds - f is_continuous_in x0 let f be PartFunc of REAL,(REAL n); ::_thesis: ( x0 in dom f & f is_continuous_in x0 implies - f is_continuous_in x0 ) assume A1: ( x0 in dom f & f is_continuous_in x0 ) ; ::_thesis: - f is_continuous_in x0 reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is_continuous_in x0 by A1, Th1; then A2: - g is_continuous_in x0 by A1, NFCONT_3:14; - g = - f by Th8; hence - f is_continuous_in x0 by A2, Th1; ::_thesis: verum end; theorem :: NFCONT_4:19 for n being Element of NAT for x0 being real number for S being RealNormSpace for z being Point of (REAL-NS n) for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for S being RealNormSpace for z being Point of (REAL-NS n) for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 let x0 be real number ; ::_thesis: for S being RealNormSpace for z being Point of (REAL-NS n) for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 let S be RealNormSpace; ::_thesis: for z being Point of (REAL-NS n) for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 let z be Point of (REAL-NS n); ::_thesis: for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 let f1 be PartFunc of REAL,(REAL n); ::_thesis: for f2 being PartFunc of (REAL-NS n),S st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z holds f2 * f1 is_continuous_in x0 let f2 be PartFunc of (REAL-NS n),S; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z implies f2 * f1 is_continuous_in x0 ) assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & z = f1 /. x0 & f2 is_continuous_in z ) ; ::_thesis: f2 * f1 is_continuous_in x0 reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: g1 is_continuous_in x0 by A1, Th1; f1 /. x0 = g1 /. x0 by REAL_NS1:def_4; hence f2 * f1 is_continuous_in x0 by A2, A1, NFCONT_3:15; ::_thesis: verum end; theorem Th20: :: NFCONT_4:20 for x0 being real number for S being RealNormSpace for f1 being PartFunc of REAL,S for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 proof let x0 be real number ; ::_thesis: for S being RealNormSpace for f1 being PartFunc of REAL,S for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let S be RealNormSpace; ::_thesis: for f1 being PartFunc of REAL,S for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f1 be PartFunc of REAL,S; ::_thesis: for f2 being PartFunc of S,REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f2 be PartFunc of S,REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 ) assume A1: x0 in dom (f2 * f1) ; ::_thesis: ( not f1 is_continuous_in x0 or not f2 is_continuous_in f1 /. x0 or f2 * f1 is_continuous_in x0 ) assume that A2: f1 is_continuous_in x0 and A3: f2 is_continuous_in f1 /. x0 ; ::_thesis: f2 * f1 is_continuous_in x0 let s1 be Real_Sequence; :: according to FCONT_1:def_1 ::_thesis: ( not rng s1 c= dom (f2 * f1) or not s1 is convergent or not lim s1 = x0 or ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) ) assume that A4: rng s1 c= dom (f2 * f1) and A5: ( s1 is convergent & lim s1 = x0 ) ; ::_thesis: ( (f2 * f1) /* s1 is convergent & (f2 * f1) . x0 = lim ((f2 * f1) /* s1) ) A6: dom (f2 * f1) c= dom f1 by RELAT_1:25; A7: rng (f1 /* s1) c= dom f2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (f1 /* s1) or x in dom f2 ) assume x in rng (f1 /* s1) ; ::_thesis: x in dom f2 then consider n being Element of NAT such that A8: x = (f1 /* s1) . n by FUNCT_2:113; s1 . n in rng s1 by VALUED_0:28; then f1 . (s1 . n) in dom f2 by A4, FUNCT_1:11; hence x in dom f2 by A4, A6, A8, FUNCT_2:108, XBOOLE_1:1; ::_thesis: verum end; A9: now__::_thesis:_for_n_being_Element_of_NAT_holds_((f2_*_f1)_/*_s1)_._n_=_(f2_/*_(f1_/*_s1))_._n let n be Element of NAT ; ::_thesis: ((f2 * f1) /* s1) . n = (f2 /* (f1 /* s1)) . n s1 . n in rng s1 by VALUED_0:28; then A10: s1 . n in dom f1 by A4, FUNCT_1:11; thus ((f2 * f1) /* s1) . n = (f2 * f1) . (s1 . n) by A4, FUNCT_2:108 .= f2 . (f1 . (s1 . n)) by A10, FUNCT_1:13 .= f2 . ((f1 /* s1) . n) by A4, A6, FUNCT_2:108, XBOOLE_1:1 .= (f2 /* (f1 /* s1)) . n by A7, FUNCT_2:108 ; ::_thesis: verum end; then A11: f2 /* (f1 /* s1) = (f2 * f1) /* s1 by FUNCT_2:63; rng s1 c= dom f1 by A4, A6, XBOOLE_1:1; then A12: ( f1 /* s1 is convergent & f1 /. x0 = lim (f1 /* s1) ) by A2, A5, NFCONT_3:def_1; hence (f2 * f1) /* s1 is convergent by A3, A7, A11, NFCONT_1:def_6; ::_thesis: (f2 * f1) . x0 = lim ((f2 * f1) /* s1) thus (f2 * f1) . x0 = (f2 * f1) /. x0 by A1, PARTFUN1:def_6 .= f2 /. (f1 /. x0) by A1, PARTFUN2:3 .= lim (f2 /* (f1 /* s1)) by A12, A3, A7, NFCONT_1:def_6 .= lim ((f2 * f1) /* s1) by A9, FUNCT_2:63 ; ::_thesis: verum end; definition let n be Element of NAT ; let f be PartFunc of (REAL n),REAL; let x0 be Element of REAL n; predf is_continuous_in x0 means :Def4: :: NFCONT_4:def 4 ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st ( x0 = y0 & f = g & g is_continuous_in y0 ); end; :: deftheorem Def4 defines is_continuous_in NFCONT_4:def_4_:_ for n being Element of NAT for f being PartFunc of (REAL n),REAL for x0 being Element of REAL n holds ( f is_continuous_in x0 iff ex y0 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st ( x0 = y0 & f = g & g is_continuous_in y0 ) ); theorem Th21: :: NFCONT_4:21 for n being Element of NAT for f being PartFunc of (REAL n),REAL for h being PartFunc of (REAL-NS n),REAL for x0 being Element of REAL n for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds ( f is_continuous_in x0 iff h is_continuous_in y0 ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of (REAL n),REAL for h being PartFunc of (REAL-NS n),REAL for x0 being Element of REAL n for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds ( f is_continuous_in x0 iff h is_continuous_in y0 ) let f be PartFunc of (REAL n),REAL; ::_thesis: for h being PartFunc of (REAL-NS n),REAL for x0 being Element of REAL n for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds ( f is_continuous_in x0 iff h is_continuous_in y0 ) let h be PartFunc of (REAL-NS n),REAL; ::_thesis: for x0 being Element of REAL n for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds ( f is_continuous_in x0 iff h is_continuous_in y0 ) let x0 be Element of REAL n; ::_thesis: for y0 being Point of (REAL-NS n) st f = h & x0 = y0 holds ( f is_continuous_in x0 iff h is_continuous_in y0 ) let y0 be Point of (REAL-NS n); ::_thesis: ( f = h & x0 = y0 implies ( f is_continuous_in x0 iff h is_continuous_in y0 ) ) assume A1: ( f = h & x0 = y0 ) ; ::_thesis: ( f is_continuous_in x0 iff h is_continuous_in y0 ) hereby ::_thesis: ( h is_continuous_in y0 implies f is_continuous_in x0 ) assume f is_continuous_in x0 ; ::_thesis: h is_continuous_in y0 then ex y1 being Point of (REAL-NS n) ex g being PartFunc of (REAL-NS n),REAL st ( x0 = y1 & f = g & g is_continuous_in y1 ) by Def4; hence h is_continuous_in y0 by A1; ::_thesis: verum end; thus ( h is_continuous_in y0 implies f is_continuous_in x0 ) by A1, Def4; ::_thesis: verum end; theorem Th22: :: NFCONT_4:22 for n being Element of NAT for x0 being real number for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 proof let n be Element of NAT ; ::_thesis: for x0 being real number for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let x0 be real number ; ::_thesis: for f1 being PartFunc of REAL,(REAL n) for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f1 be PartFunc of REAL,(REAL n); ::_thesis: for f2 being PartFunc of (REAL n),REAL st x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 holds f2 * f1 is_continuous_in x0 let f2 be PartFunc of (REAL n),REAL; ::_thesis: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 implies f2 * f1 is_continuous_in x0 ) assume A1: ( x0 in dom (f2 * f1) & f1 is_continuous_in x0 & f2 is_continuous_in f1 /. x0 ) ; ::_thesis: f2 * f1 is_continuous_in x0 reconsider g1 = f1 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; reconsider g2 = f2 as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4; A2: g1 is_continuous_in x0 by A1, Th1; f1 /. x0 = g1 /. x0 by REAL_NS1:def_4; then g2 is_continuous_in g1 /. x0 by A1, Th21; hence f2 * f1 is_continuous_in x0 by A2, A1, Th20; ::_thesis: verum end; definition let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); attrf is continuous means :Def5: :: NFCONT_4:def 5 for x0 being real number st x0 in dom f holds f is_continuous_in x0; end; :: deftheorem Def5 defines continuous NFCONT_4:def_5_:_ for n being Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is continuous iff for x0 being real number st x0 in dom f holds f is_continuous_in x0 ); theorem Th23: :: NFCONT_4:23 for n being Element of NAT for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of REAL,(REAL n) st g = f holds ( g is continuous iff f is continuous ) proof let n be Element of NAT ; ::_thesis: for g being PartFunc of REAL,(REAL-NS n) for f being PartFunc of REAL,(REAL n) st g = f holds ( g is continuous iff f is continuous ) let g be PartFunc of REAL,(REAL-NS n); ::_thesis: for f being PartFunc of REAL,(REAL n) st g = f holds ( g is continuous iff f is continuous ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( g = f implies ( g is continuous iff f is continuous ) ) assume A1: g = f ; ::_thesis: ( g is continuous iff f is continuous ) hereby ::_thesis: ( f is continuous implies g is continuous ) assume A2: g is continuous ; ::_thesis: f is continuous now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_f_holds_ f_is_continuous_in_x0 let x0 be real number ; ::_thesis: ( x0 in dom f implies f is_continuous_in x0 ) assume x0 in dom f ; ::_thesis: f is_continuous_in x0 then g is_continuous_in x0 by A2, A1, NFCONT_3:def_2; hence f is_continuous_in x0 by A1, Th1; ::_thesis: verum end; hence f is continuous by Def5; ::_thesis: verum end; assume A3: f is continuous ; ::_thesis: g is continuous now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_g_holds_ g_is_continuous_in_x0 let x0 be real number ; ::_thesis: ( x0 in dom g implies g is_continuous_in x0 ) assume x0 in dom g ; ::_thesis: g is_continuous_in x0 then f is_continuous_in x0 by A3, A1, Def5; hence g is_continuous_in x0 by A1, Th1; ::_thesis: verum end; hence g is continuous by NFCONT_3:def_2; ::_thesis: verum end; theorem Th24: :: NFCONT_4:24 for n being Element of NAT for X being set for f being PartFunc of REAL,(REAL n) st X c= dom f holds ( f | X is continuous iff for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) proof let n be Element of NAT ; ::_thesis: for X being set for f being PartFunc of REAL,(REAL n) st X c= dom f holds ( f | X is continuous iff for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f holds ( f | X is continuous iff for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f implies ( f | X is continuous iff for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ) assume A1: X c= dom f ; ::_thesis: ( f | X is continuous iff for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) thus ( f | X is continuous implies for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) ::_thesis: ( ( for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) implies f | X is continuous ) proof assume A2: f | X is continuous ; ::_thesis: for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) let x0 be real number ; ::_thesis: for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) let r be Real; ::_thesis: ( x0 in X & 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) assume that A3: x0 in X and A4: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) x0 in dom (f | X) by A1, A3, RELAT_1:62; then f | X is_continuous_in x0 by A2, Def5; then consider s being real number such that A5: 0 < s and A6: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A4, Th3; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) thus 0 < s by A5; ::_thesis: for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r let x1 be real number ; ::_thesis: ( x1 in X & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r ) assume that A7: x1 in X and A8: abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r A9: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A1, XBOOLE_1:28 ; then |.((f /. x1) - (f /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A7, PARTFUN2:15 .= |.(((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 A10: for x0 being real number for r being Real st x0 in X & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ; ::_thesis: f | X is continuous A11: dom (f | X) = (dom f) /\ X by RELAT_1:61 .= X by A1, XBOOLE_1:28 ; now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_(f_|_X)_holds_ f_|_X_is_continuous_in_x0 let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) assume A12: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 A13: x0 in X by A12, RELAT_1:57; for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) ) assume 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) then consider s being real number such that A14: 0 < s and A15: for x1 being real number st x1 in X & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r by A10, A13; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) ) thus 0 < s by A14; ::_thesis: for x1 being real number st x1 in dom (f | X) & abs (x1 - x0) < s holds |.(((f | X) /. x1) - ((f | X) /. x0)).| < r let x1 be real number ; ::_thesis: ( x1 in dom (f | X) & abs (x1 - x0) < s implies |.(((f | X) /. x1) - ((f | X) /. x0)).| < r ) assume that A16: x1 in dom (f | X) and A17: abs (x1 - x0) < s ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x0)).| < r |.(((f | X) /. x1) - ((f | X) /. x0)).| = |.(((f | X) /. x1) - (f /. x0)).| by A12, PARTFUN2:15 .= |.((f /. x1) - (f /. x0)).| by A16, PARTFUN2:15 ; hence |.(((f | X) /. x1) - ((f | X) /. x0)).| < r by A11, A15, A16, A17; ::_thesis: verum end; hence f | X is_continuous_in x0 by Th3, A12; ::_thesis: verum end; hence f | X is continuous by Def5; ::_thesis: verum end; registration let n be Element of NAT ; cluster Function-like constant -> continuous for Element of bool [:REAL,(REAL n):]; coherence for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds b1 is continuous proof let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is continuous ) assume A1: f is constant ; ::_thesis: f is continuous now__::_thesis:_for_x0_being_real_number_ for_r_being_Real_st_x0_in_dom_f_&_0_<_r_holds_ ex_s_being_real_number_st_ (_0_<_s_&_(_for_x1_being_real_number_st_x1_in_dom_f_&_abs_(x1_-_x0)_<_s_holds_ |.((f_/._x1)_-_(f_/._x0)).|_<_r_)_) reconsider s = 1 as real number ; let x0 be real number ; ::_thesis: for r being Real st x0 in dom f & 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) let r be Real; ::_thesis: ( x0 in dom f & 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) ) assume that A2: x0 in dom f and A3: 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) take s = s; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r ) ) thus 0 < s ; ::_thesis: for x1 being real number st x1 in dom f & abs (x1 - x0) < s holds |.((f /. x1) - (f /. x0)).| < r let x1 be real number ; ::_thesis: ( x1 in dom f & abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r ) assume A4: x1 in dom f ; ::_thesis: ( abs (x1 - x0) < s implies |.((f /. x1) - (f /. x0)).| < r ) assume abs (x1 - x0) < s ; ::_thesis: |.((f /. x1) - (f /. x0)).| < r f /. x1 = f . x1 by A4, PARTFUN1:def_6 .= f . x0 by A1, A2, A4, FUNCT_1:def_10 .= f /. x0 by A2, PARTFUN1:def_6 ; hence |.((f /. x1) - (f /. x0)).| < r by A3; ::_thesis: verum end; then f | (dom f) is continuous by Th24; hence f is continuous by RELAT_1:69; ::_thesis: verum end; end; registration let n be Element of NAT ; cluster Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() continuous for Element of bool [:REAL,(REAL n):]; existence ex b1 being PartFunc of REAL,(REAL n) st b1 is continuous proof take f = the constant PartFunc of REAL,(REAL n); ::_thesis: f is continuous thus f is continuous ; ::_thesis: verum end; end; registration let n be Element of NAT ; let f be continuous PartFunc of REAL,(REAL n); let X be set ; clusterf | X -> continuous for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is continuous proof for x0 being real number st x0 in dom (f | X) holds f | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom (f | X) implies f | X is_continuous_in x0 ) assume A1: x0 in dom (f | X) ; ::_thesis: f | X is_continuous_in x0 then x0 in dom f by RELAT_1:57; then A2: f is_continuous_in x0 by Def5; x0 in X by A1, RELAT_1:57; hence f | X is_continuous_in x0 by A2, Th2; ::_thesis: verum end; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is continuous by Def5; ::_thesis: verum end; end; theorem :: NFCONT_4:25 for n being Element of NAT for X, X1 being set for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds f | X1 is continuous proof let n be Element of NAT ; ::_thesis: for X, X1 being set for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds f | X1 is continuous let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is continuous & X1 c= X holds f | X1 is continuous let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is continuous & X1 c= X implies f | X1 is continuous ) assume A1: f | X is continuous ; ::_thesis: ( not X1 c= X or f | X1 is continuous ) assume X1 c= X ; ::_thesis: f | X1 is continuous then f | X1 = (f | X) | X1 by RELAT_1:74; hence f | X1 is continuous by A1; ::_thesis: verum end; registration let n be Element of NAT ; cluster empty Function-like -> continuous for Element of bool [:REAL,(REAL n):]; coherence for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds b1 is continuous ; end; registration let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); let X be trivial set ; clusterf | X -> continuous for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is continuous proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | X is continuous PartFunc of REAL,(REAL-NS n) ; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is continuous by Th23; ::_thesis: verum end; end; registration let n be Element of NAT ; let f1, f2 be continuous PartFunc of REAL,(REAL n); clusterf1 + f2 -> continuous for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds b1 is continuous proof reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A1: ( g1 is continuous & g2 is continuous ) by Th23; g1 + g2 = f1 + f2 by Th5; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds b1 is continuous by A1, Th23; ::_thesis: verum end; end; theorem :: NFCONT_4:26 for n being Element of NAT for X being set for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) proof let n be Element of NAT ; ::_thesis: for X being set for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) let X be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous holds ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous implies ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) ) assume A1: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f2 | X is continuous ) ; ::_thesis: ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: g1 | X is continuous by A1, Th23; g2 | X is continuous by A1, Th23; then A3: ( (g1 + g2) | X is continuous & (g1 - g2) | X is continuous ) by A1, A2, NFCONT_3:19; A4: g1 + g2 = f1 + f2 by Th5; g1 - g2 = f1 - f2 by Th10; hence ( (f1 + f2) | X is continuous & (f1 - f2) | X is continuous ) by A3, A4, Th23; ::_thesis: verum end; theorem :: NFCONT_4:27 for n being Element of NAT for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) proof let n be Element of NAT ; ::_thesis: for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous holds ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous implies ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) ) assume A1: ( X c= dom f1 & X1 c= dom f2 & f1 | X is continuous & f2 | X1 is continuous ) ; ::_thesis: ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: g1 | X is continuous by A1, Th23; g2 | X1 is continuous by A1, Th23; then A3: ( (g1 + g2) | (X /\ X1) is continuous & (g1 - g2) | (X /\ X1) is continuous ) by A1, A2, NFCONT_3:20; A4: g1 + g2 = f1 + f2 by Th5; g1 - g2 = f1 - f2 by Th10; hence ( (f1 + f2) | (X /\ X1) is continuous & (f1 - f2) | (X /\ X1) is continuous ) by A3, A4, Th23; ::_thesis: verum end; registration let n be Element of NAT ; let f be continuous PartFunc of REAL,(REAL n); let r be Real; clusterr (#) f -> continuous for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds b1 is continuous proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A1: g is continuous by Th23; r (#) g = r (#) f by Th6; hence for b1 being PartFunc of REAL,(REAL n) st b1 = r (#) f holds b1 is continuous by A1, Th23; ::_thesis: verum end; end; theorem :: NFCONT_4:28 for n being Element of NAT for X being set for r being Real for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds (r (#) f) | X is continuous proof let n be Element of NAT ; ::_thesis: for X being set for r being Real for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds (r (#) f) | X is continuous let X be set ; ::_thesis: for r being Real for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds (r (#) f) | X is continuous let r be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds (r (#) f) | X is continuous let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies (r (#) f) | X is continuous ) assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: (r (#) f) | X is continuous reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | X is continuous PartFunc of REAL,(REAL-NS n) by A1, Th23; then A2: (r (#) g) | X is continuous by A1, NFCONT_3:21; r (#) g = r (#) f by Th6; hence (r (#) f) | X is continuous by A2, Th23; ::_thesis: verum end; theorem :: NFCONT_4:29 for n being Element of NAT for X being set for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds ( |.f.| | X is continuous & (- f) | X is continuous ) proof let n be Element of NAT ; ::_thesis: for X being set for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds ( |.f.| | X is continuous & (- f) | X is continuous ) let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st X c= dom f & f | X is continuous holds ( |.f.| | X is continuous & (- f) | X is continuous ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( X c= dom f & f | X is continuous implies ( |.f.| | X is continuous & (- f) | X is continuous ) ) assume A1: ( X c= dom f & f | X is continuous ) ; ::_thesis: ( |.f.| | X is continuous & (- f) | X is continuous ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | X is continuous by A1, Th23; then A2: ( ||.g.|| | X is continuous & (- g) | X is continuous ) by A1, NFCONT_3:22; hence |.f.| | X is continuous by Th9; ::_thesis: (- f) | X is continuous - g = - f by Th8; hence (- f) | X is continuous by A2, Th23; ::_thesis: verum end; theorem :: NFCONT_4:30 for n being Element of NAT for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds f | REAL is continuous proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 holds f | REAL is continuous let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being real number st f is_continuous_in x0 implies f | REAL is continuous ) assume A1: ( f is total & ( for x1, x2 being real number holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) ) ; ::_thesis: ( for x0 being real number holds not f is_continuous_in x0 or f | REAL is continuous ) given x0 being real number such that A2: f is_continuous_in x0 ; ::_thesis: f | REAL is continuous reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A3: now__::_thesis:_for_x1,_x2_being_real_number_holds_g_/._(x1_+_x2)_=_(g_/._x1)_+_(g_/._x2) let x1, x2 be real number ; ::_thesis: g /. (x1 + x2) = (g /. x1) + (g /. x2) A4: ( g /. x1 = f /. x1 & g /. x2 = f /. x2 ) by REAL_NS1:def_4; thus g /. (x1 + x2) = f /. (x1 + x2) by REAL_NS1:def_4 .= (f /. x1) + (f /. x2) by A1 .= (g /. x1) + (g /. x2) by A4, REAL_NS1:2 ; ::_thesis: verum end; g is_continuous_in x0 by A2, Th1; then g | REAL is continuous by A1, A3, NFCONT_3:23; hence f | REAL is continuous by Th23; ::_thesis: verum end; theorem :: NFCONT_4:31 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds Y is compact proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds Y is compact let f be PartFunc of REAL,(REAL n); ::_thesis: for Y being Subset of (REAL-NS n) st dom f is compact & f | (dom f) is continuous & Y = rng f holds Y is compact let Y be Subset of (REAL-NS n); ::_thesis: ( dom f is compact & f | (dom f) is continuous & Y = rng f implies Y is compact ) assume A1: ( dom f is compact & f | (dom f) is continuous & Y = rng f ) ; ::_thesis: Y is compact reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | (dom g) is continuous by A1, Th23; hence Y is compact by A1, NFCONT_3:24; ::_thesis: verum end; theorem :: NFCONT_4:32 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for Y being Subset of REAL for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds Z is compact proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for Y being Subset of REAL for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds Z is compact let f be PartFunc of REAL,(REAL n); ::_thesis: for Y being Subset of REAL for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds Z is compact let Y be Subset of REAL; ::_thesis: for Z being Subset of (REAL-NS n) st Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous holds Z is compact let Z be Subset of (REAL-NS n); ::_thesis: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous implies Z is compact ) assume A1: ( Y c= dom f & Z = f .: Y & Y is compact & f | Y is continuous ) ; ::_thesis: Z is compact reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | Y is continuous by A1, Th23; hence Z is compact by A1, NFCONT_3:25; ::_thesis: verum end; definition let n be Element of NAT ; let f be PartFunc of REAL,(REAL n); attrf is Lipschitzian means :Def6: :: NFCONT_4:def 6 ex g being PartFunc of REAL,(REAL-NS n) st ( g = f & g is Lipschitzian ); end; :: deftheorem Def6 defines Lipschitzian NFCONT_4:def_6_:_ for n being Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is Lipschitzian iff ex g being PartFunc of REAL,(REAL-NS n) st ( g = f & g is Lipschitzian ) ); theorem Th33: :: NFCONT_4:33 for n being Element of NAT for f being PartFunc of REAL,(REAL n) holds ( f is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) hereby ::_thesis: ( ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) implies f is Lipschitzian ) assume f is Lipschitzian ; ::_thesis: ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) then consider g being PartFunc of REAL,(REAL-NS n) such that A1: ( g = f & g is Lipschitzian ) by Def6; consider r being real number such that A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom g & x2 in dom g holds ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) ) ) by A1, NFCONT_3:def_3; take r = r; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) thus 0 < r by A2; ::_thesis: for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) thus for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ::_thesis: verum proof let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) then A3: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A1, A2; ( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def_4; hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; end; given r being real number such that A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ; ::_thesis: f is Lipschitzian reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_g_&_x2_in_dom_g_holds_ ||.((g_/._x1)_-_(g_/._x2)).||_<=_r_*_(abs_(x1_-_x2)) let x1, x2 be real number ; ::_thesis: ( x1 in dom g & x2 in dom g implies ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) ) assume ( x1 in dom g & x2 in dom g ) ; ::_thesis: ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) then A5: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4; ( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def_4; hence ||.((g /. x1) - (g /. x2)).|| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; then g is Lipschitzian by A4, NFCONT_3:def_3; hence f is Lipschitzian by Def6; ::_thesis: verum end; theorem Th34: :: NFCONT_4:34 for n being Element of NAT for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) st f = h holds ( f is Lipschitzian iff h is Lipschitzian ) proof let n be Element of NAT ; ::_thesis: for f being PartFunc of REAL,(REAL n) for h being PartFunc of REAL,(REAL-NS n) st f = h holds ( f is Lipschitzian iff h is Lipschitzian ) let f be PartFunc of REAL,(REAL n); ::_thesis: for h being PartFunc of REAL,(REAL-NS n) st f = h holds ( f is Lipschitzian iff h is Lipschitzian ) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( f = h implies ( f is Lipschitzian iff h is Lipschitzian ) ) assume A1: f = h ; ::_thesis: ( f is Lipschitzian iff h is Lipschitzian ) hereby ::_thesis: ( h is Lipschitzian implies f is Lipschitzian ) assume f is Lipschitzian ; ::_thesis: h is Lipschitzian then consider r being real number such that A2: ( 0 < r & ( for x1, x2 being real number st x1 in dom f & x2 in dom f holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) by Th33; now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_h_&_x2_in_dom_h_holds_ ||.((h_/._x1)_-_(h_/._x2)).||_<=_r_*_(abs_(x1_-_x2)) let x1, x2 be real number ; ::_thesis: ( x1 in dom h & x2 in dom h implies ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) ) assume ( x1 in dom h & x2 in dom h ) ; ::_thesis: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) then A3: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, A1; ( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4; hence ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A3, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; hence h is Lipschitzian by A2, NFCONT_3:def_3; ::_thesis: verum end; assume h is Lipschitzian ; ::_thesis: f is Lipschitzian then consider r being real number such that A4: ( 0 < r & ( for x1, x2 being real number st x1 in dom h & x2 in dom h holds ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) ) ) by NFCONT_3:def_3; now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_f_&_x2_in_dom_f_holds_ |.((f_/._x1)_-_(f_/._x2)).|_<=_r_*_(abs_(x1_-_x2)) let x1, x2 be real number ; ::_thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) assume ( x1 in dom f & x2 in dom f ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) then A5: ||.((h /. x1) - (h /. x2)).|| <= r * (abs (x1 - x2)) by A4, A1; ( f /. x1 = h /. x1 & f /. x2 = h /. x2 ) by A1, REAL_NS1:def_4; hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A5, REAL_NS1:1, REAL_NS1:5; ::_thesis: verum end; hence f is Lipschitzian by A4, Th33; ::_thesis: verum end; theorem :: NFCONT_4:35 for n being Element of NAT for X being set for f being PartFunc of REAL,(REAL n) holds ( f | X is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) proof let n be Element of NAT ; ::_thesis: for X being set for f being PartFunc of REAL,(REAL n) holds ( f | X is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) holds ( f | X is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian iff ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ) hereby ::_thesis: ( ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian ) assume f | X is Lipschitzian ; ::_thesis: ex r being real number st ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) then consider r being real number such that A1: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) ) ) by Th33; take r = r; ::_thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) thus 0 < r by A1; ::_thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) thus for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ::_thesis: verum proof let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) assume A2: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) then |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A1; then |.((f /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15; hence |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A2, PARTFUN2:15; ::_thesis: verum end; end; given r being real number such that A3: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) ) ) ; ::_thesis: f | X is Lipschitzian now__::_thesis:_for_x1,_x2_being_real_number_st_x1_in_dom_(f_|_X)_&_x2_in_dom_(f_|_X)_holds_ |.(((f_|_X)_/._x1)_-_((f_|_X)_/._x2)).|_<=_r_*_(abs_(x1_-_x2)) let x1, x2 be real number ; ::_thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) ) assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; ::_thesis: |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) then |.((f /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A3; then |.(((f | X) /. x1) - (f /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15; hence |.(((f | X) /. x1) - ((f | X) /. x2)).| <= r * (abs (x1 - x2)) by A4, PARTFUN2:15; ::_thesis: verum end; hence f | X is Lipschitzian by A3, Th33; ::_thesis: verum end; registration let n be Element of NAT ; cluster empty Function-like -> Lipschitzian for Element of bool [:REAL,(REAL n):]; coherence for b1 being PartFunc of REAL,(REAL n) st b1 is empty holds b1 is Lipschitzian proof let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is empty implies f is Lipschitzian ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; assume f is empty ; ::_thesis: f is Lipschitzian then g is empty ; hence f is Lipschitzian by Th34; ::_thesis: verum end; end; registration let n be Element of NAT ; cluster empty Relation-like REAL -defined REAL n -valued Function-like V233() V234() V235() for Element of bool [:REAL,(REAL n):]; existence ex b1 being PartFunc of REAL,(REAL n) st b1 is empty proof take the empty PartFunc of REAL,(REAL n) ; ::_thesis: the empty PartFunc of REAL,(REAL n) is empty thus the empty PartFunc of REAL,(REAL n) is empty ; ::_thesis: verum end; end; registration let n be Element of NAT ; let f be Lipschitzian PartFunc of REAL,(REAL n); let X be set ; clusterf | X -> Lipschitzian for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is Lipschitzian proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is Lipschitzian by Th34; then g | X is Lipschitzian ; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f | X holds b1 is Lipschitzian by Th34; ::_thesis: verum end; end; theorem :: NFCONT_4:36 for n being Element of NAT for X, X1 being set for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds f | X1 is Lipschitzian proof let n be Element of NAT ; ::_thesis: for X, X1 being set for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds f | X1 is Lipschitzian let X, X1 be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X1 c= X holds f | X1 is Lipschitzian let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X1 c= X implies f | X1 is Lipschitzian ) assume that A1: f | X is Lipschitzian and A2: X1 c= X ; ::_thesis: f | X1 is Lipschitzian f | X1 = (f | X) | X1 by A2, RELAT_1:74; hence f | X1 is Lipschitzian by A1; ::_thesis: verum end; registration let n be Element of NAT ; let f1, f2 be Lipschitzian PartFunc of REAL,(REAL n); clusterf1 + f2 -> Lipschitzian for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds b1 is Lipschitzian proof reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A1: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34; g1 + g2 = f1 + f2 by Th5; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 + f2 holds b1 is Lipschitzian by A1, Th34; ::_thesis: verum end; clusterf1 - f2 -> Lipschitzian for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds b1 is Lipschitzian proof reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A2: ( g1 is Lipschitzian & g2 is Lipschitzian ) by Th34; g1 - g2 = f1 - f2 by Th10; hence for b1 being PartFunc of REAL,(REAL n) st b1 = f1 - f2 holds b1 is Lipschitzian by A2, Th34; ::_thesis: verum end; end; theorem :: NFCONT_4:37 for n being Element of NAT for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 + f2) | (X /\ X1) is Lipschitzian proof let n be Element of NAT ; ::_thesis: for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 + f2) | (X /\ X1) is Lipschitzian let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 + f2) | (X /\ X1) is Lipschitzian let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 + f2) | (X /\ X1) is Lipschitzian ) assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 + f2) | (X /\ X1) is Lipschitzian reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; ( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1; then A2: (g1 + g2) | (X /\ X1) is Lipschitzian by NFCONT_3:28; g1 + g2 = f1 + f2 by Th5; hence (f1 + f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum end; theorem :: NFCONT_4:38 for n being Element of NAT for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 - f2) | (X /\ X1) is Lipschitzian proof let n be Element of NAT ; ::_thesis: for X, X1 being set for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 - f2) | (X /\ X1) is Lipschitzian let X, X1 be set ; ::_thesis: for f1, f2 being PartFunc of REAL,(REAL n) st f1 | X is Lipschitzian & f2 | X1 is Lipschitzian holds (f1 - f2) | (X /\ X1) is Lipschitzian let f1, f2 be PartFunc of REAL,(REAL n); ::_thesis: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian implies (f1 - f2) | (X /\ X1) is Lipschitzian ) assume A1: ( f1 | X is Lipschitzian & f2 | X1 is Lipschitzian ) ; ::_thesis: (f1 - f2) | (X /\ X1) is Lipschitzian reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; ( g1 | X is Lipschitzian & g2 | X1 is Lipschitzian ) by Th34, A1; then A2: (g1 - g2) | (X /\ X1) is Lipschitzian by NFCONT_3:29; g1 - g2 = f1 - f2 by Th10; hence (f1 - f2) | (X /\ X1) is Lipschitzian by A2, Th34; ::_thesis: verum end; registration let n be Element of NAT ; let f be Lipschitzian PartFunc of REAL,(REAL n); let p be Real; clusterp (#) f -> Lipschitzian for PartFunc of REAL,(REAL n); coherence for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds b1 is Lipschitzian proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; A1: g is Lipschitzian by Th34; p (#) g = p (#) f by Th6; hence for b1 being PartFunc of REAL,(REAL n) st b1 = p (#) f holds b1 is Lipschitzian by A1, Th34; ::_thesis: verum end; end; theorem :: NFCONT_4:39 for n being Element of NAT for X being set for p being Real for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds (p (#) f) | X is Lipschitzian proof let n be Element of NAT ; ::_thesis: for X being set for p being Real for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds (p (#) f) | X is Lipschitzian let X be set ; ::_thesis: for p being Real for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds (p (#) f) | X is Lipschitzian let p be Real; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian & X c= dom f holds (p (#) f) | X is Lipschitzian let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian & X c= dom f implies (p (#) f) | X is Lipschitzian ) assume A1: ( f | X is Lipschitzian & X c= dom f ) ; ::_thesis: (p (#) f) | X is Lipschitzian reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | X is Lipschitzian by Th34, A1; then A2: (p (#) g) | X is Lipschitzian by A1, NFCONT_3:30; p (#) g = p (#) f by Th6; hence (p (#) f) | X is Lipschitzian by A2, Th34; ::_thesis: verum end; registration let n be Element of NAT ; let f be Lipschitzian PartFunc of REAL,(REAL n); cluster|.f.| -> Lipschitzian for PartFunc of REAL,REAL; coherence for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds b1 is Lipschitzian proof reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is Lipschitzian by Th34; then ||.g.|| is Lipschitzian ; hence for b1 being PartFunc of REAL,REAL st b1 = |.f.| holds b1 is Lipschitzian by Th9; ::_thesis: verum end; end; theorem :: NFCONT_4:40 for n being Element of NAT for X being set for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) proof let n be Element of NAT ; ::_thesis: for X being set for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) st f | X is Lipschitzian holds ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) let f be PartFunc of REAL,(REAL n); ::_thesis: ( f | X is Lipschitzian implies ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) ) assume A1: f | X is Lipschitzian ; ::_thesis: ( - (f | X) is Lipschitzian & |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g | X is Lipschitzian by A1, Th34; then A2: ( - (g | X) is Lipschitzian & ||.g.|| | X is Lipschitzian & (- g) | X is Lipschitzian ) by NFCONT_3:31; - (g | X) = - (f | X) by Th8; hence - (f | X) is Lipschitzian by A2, Th34; ::_thesis: ( |.f.| | X is Lipschitzian & (- f) | X is Lipschitzian ) thus |.f.| | X is Lipschitzian by A2, Th9; ::_thesis: (- f) | X is Lipschitzian - g = - f by Th8; hence (- f) | X is Lipschitzian by A2, Th34; ::_thesis: verum end; registration let n be Element of NAT ; cluster Function-like constant -> Lipschitzian for Element of bool [:REAL,(REAL n):]; coherence for b1 being PartFunc of REAL,(REAL n) st b1 is constant holds b1 is Lipschitzian proof let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is constant implies f is Lipschitzian ) assume A1: f is constant ; ::_thesis: f is Lipschitzian reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; g is constant by A1; hence f is Lipschitzian by Th34; ::_thesis: verum end; end; registration let n be Element of NAT ; cluster Function-like Lipschitzian -> continuous for Element of bool [:REAL,(REAL n):]; coherence for b1 being PartFunc of REAL,(REAL n) st b1 is Lipschitzian holds b1 is continuous proof let f be PartFunc of REAL,(REAL n); ::_thesis: ( f is Lipschitzian implies f is continuous ) reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; assume f is Lipschitzian ; ::_thesis: f is continuous then g is Lipschitzian by Th34; hence f is continuous by Th23; ::_thesis: verum end; end; theorem :: NFCONT_4:41 for n being Element of NAT for X being set for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ) holds f | X is continuous proof let n be Element of NAT ; ::_thesis: for X being set for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ) holds f | X is continuous let X be set ; ::_thesis: for f being PartFunc of REAL,(REAL n) for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ) holds f | X is continuous let f be PartFunc of REAL,(REAL n); ::_thesis: for r, p being Element of REAL n st ( for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ) holds f | X is continuous let r, p be Element of REAL n; ::_thesis: ( ( for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ) implies f | X is continuous ) assume A1: for x0 being real number st x0 in X holds f /. x0 = (x0 * r) + p ; ::_thesis: f | X is continuous reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def_4; reconsider r0 = r, p0 = p as Point of (REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_x0_being_real_number_st_x0_in_X_holds_ g_/._x0_=_(x0_*_r0)_+_p0 let x0 be real number ; ::_thesis: ( x0 in X implies g /. x0 = (x0 * r0) + p0 ) assume A2: x0 in X ; ::_thesis: g /. x0 = (x0 * r0) + p0 A3: x0 * r = x0 * r0 by REAL_NS1:3; thus g /. x0 = f /. x0 by REAL_NS1:def_4 .= (x0 * r) + p by A2, A1 .= (x0 * r0) + p0 by A3, REAL_NS1:2 ; ::_thesis: verum end; then g | X is continuous by NFCONT_3:33; hence f | X is continuous by Th23; ::_thesis: verum end; theorem Th42: :: NFCONT_4:42 for n, i being Element of NAT for x0 being Element of REAL n st 1 <= i & i <= n holds proj (i,n) is_continuous_in x0 proof let n, i be Element of NAT ; ::_thesis: for x0 being Element of REAL n st 1 <= i & i <= n holds proj (i,n) is_continuous_in x0 let x0 be Element of REAL n; ::_thesis: ( 1 <= i & i <= n implies proj (i,n) is_continuous_in x0 ) assume A1: ( 1 <= i & i <= n ) ; ::_thesis: proj (i,n) is_continuous_in x0 A2: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; reconsider prg = proj (i,n) as PartFunc of (REAL-NS n),REAL by REAL_NS1:def_4; reconsider px0 = x0 as Element of (REAL-NS n) by REAL_NS1:def_4; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_s_holds_ |.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) ) assume A3: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) take s = r; ::_thesis: ( 0 < s & ( for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) ) thus 0 < s by A3; ::_thesis: for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r now__::_thesis:_for_px1_being_Element_of_(REAL-NS_n)_st_px1_in_dom_prg_&_||.(px1_-_px0).||_<_r_holds_ |.(((proj_(i,n))_/._px1)_-_((proj_(i,n))_/._px0)).|_<_r let px1 be Element of (REAL-NS n); ::_thesis: ( px1 in dom prg & ||.(px1 - px0).|| < r implies |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ) assume A4: ( px1 in dom prg & ||.(px1 - px0).|| < r ) ; ::_thesis: |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r reconsider x1 = px1 as Element of REAL n by REAL_NS1:def_4; A5: ||.(px1 - px0).|| = |.(x1 - x0).| by REAL_NS1:1, REAL_NS1:5; (proj (i,n)) /. (x1 - x0) = ((proj (i,n)) /. x1) - ((proj (i,n)) /. x0) by A1, PDIFF_8:12; then |.(((proj (i,n)) /. x1) - ((proj (i,n)) /. x0)).| <= |.(x1 - x0).| by A1, PDIFF_8:5; hence |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r by A4, A5, XXREAL_0:2; ::_thesis: verum end; hence for px1 being Element of (REAL-NS n) st px1 in dom prg & ||.(px1 - px0).|| < s holds |.(((proj (i,n)) /. px1) - ((proj (i,n)) /. px0)).| < r ; ::_thesis: verum end; then prg is_continuous_in px0 by A2, NFCONT_1:8; hence proj (i,n) is_continuous_in x0 by Def4; ::_thesis: verum end; theorem Th43: :: NFCONT_4:43 for x0 being real number for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) holds ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) ) proof let x0 be real number ; ::_thesis: for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) holds ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) ) let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) holds ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) ) let h be PartFunc of REAL,(REAL n); ::_thesis: ( h is_continuous_in x0 iff ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) ) hereby ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 ) assume A1: h is_continuous_in x0 ; ::_thesis: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) hence A2: x0 in dom h by Th3; ::_thesis: for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 thus for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 ) assume i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0 then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1; A4: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; rng h c= REAL n ; then A5: dom ((proj (i,n)) * h) = dom h by A4, RELAT_1:27; proj (i,n) is_continuous_in h /. x0 by A3, Th42; hence (proj (i,n)) * h is_continuous_in x0 by A5, A1, A2, Th22; ::_thesis: verum end; end; assume A6: ( x0 in dom h & ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is_continuous_in x0 ) ) ; ::_thesis: h is_continuous_in x0 for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r ) ) proof let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r0 ) ) ) assume A7: 0 < r0 ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r0 ) ) set r = r0 / 2; A8: 0 < r0 / 2 by A7, XREAL_1:215; defpred S1[ Nat, real number ] means ( 0 < \$2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < \$2 holds |.((((proj (\$1,n)) * h) . x1) - (((proj (\$1,n)) * h) . x0)).| < (r0 / 2) / n ) ); A9: 0 < (r0 / 2) / n by A8, XREAL_1:139; A10: for j being Nat st j in Seg n holds ex x being Element of REAL st S1[j,x] proof let j be Nat; ::_thesis: ( j in Seg n implies ex x being Element of REAL st S1[j,x] ) assume A11: j in Seg n ; ::_thesis: ex x being Element of REAL st S1[j,x] A12: (proj (j,n)) * h is_continuous_in x0 by A6, A11; A13: dom (proj (j,n)) = REAL n by FUNCT_2:def_1; rng h c= REAL n ; then A14: dom ((proj (j,n)) * h) = dom h by A13, RELAT_1:27; consider sj being real number such that A15: ( 0 < sj & ( for x1 being real number st x1 in dom ((proj (j,n)) * h) & abs (x1 - x0) < sj holds |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n ) ) by A12, A9, FCONT_1:3; sj is Real by XREAL_0:def_1; hence ex x being Element of REAL st S1[j,x] by A15, A14; ::_thesis: verum end; consider s0 being FinSequence of REAL such that A16: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A10); n in Seg n by FINSEQ_1:3; then reconsider rs0 = rng s0 as non empty ext-real-membered set by A16, FUNCT_1:3; rng s0 is finite by A16, FINSET_1:8; then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ; A17: min rs0 in rng s0 by XXREAL_2:def_7; then reconsider s = min rs0 as Real ; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r0 ) ) ex i1 being set st ( i1 in dom s0 & s = s0 . i1 ) by A17, FUNCT_1:def_3; hence 0 < s by A16; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r0 now__::_thesis:_for_x1_being_real_number_st_x1_in_dom_h_&_abs_(x1_-_x0)_<_s_holds_ |.((h_/._x1)_-_(h_/._x0)).|_<_r0 let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies |.((h /. x1) - (h /. x0)).| < r0 ) assume A18: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: |.((h /. x1) - (h /. x0)).| < r0 now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_ |.((proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).|_<=_(r0_/_2)_/_n let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n ) assume ( 1 <= j & j <= n ) ; ::_thesis: |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n then A19: j in Seg n by FINSEQ_1:1; then s0 . j in rng s0 by A16, FUNCT_1:3; then s <= s0 . j by XXREAL_2:def_7; then abs (x1 - x0) < s0 . j by A18, XXREAL_0:2; then A20: |.((((proj (j,n)) * h) . x1) - (((proj (j,n)) * h) . x0)).| < (r0 / 2) / n by A19, A18, A16; A21: ((proj (j,n)) * h) . x1 = (proj (j,n)) . (h . x1) by A18, FUNCT_1:13 .= (proj (j,n)) . (h /. x1) by A18, PARTFUN1:def_6 ; ((proj (j,n)) * h) . x0 = (proj (j,n)) . (h . x0) by A6, FUNCT_1:13 .= (proj (j,n)) . (h /. x0) by A6, PARTFUN1:def_6 ; hence |.((proj (j,n)) . ((h /. x1) - (h /. x0))).| <= (r0 / 2) / n by A20, A21, PDIFF_8:12; ::_thesis: verum end; then |.((h /. x1) - (h /. x0)).| <= n * ((r0 / 2) / n) by PDIFF_8:17; then A22: |.((h /. x1) - (h /. x0)).| <= r0 / 2 by XCMPLX_1:87; r0 / 2 < r0 by A7, XREAL_1:216; hence |.((h /. x1) - (h /. x0)).| < r0 by A22, XXREAL_0:2; ::_thesis: verum end; hence for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds |.((h /. x1) - (h /. x0)).| < r0 ; ::_thesis: verum end; hence h is_continuous_in x0 by A6, Th3; ::_thesis: verum end; theorem :: NFCONT_4:44 for n being non empty Element of NAT for h being PartFunc of REAL,(REAL n) holds ( h is continuous iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ) proof let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL n) holds ( h is continuous iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ) let h be PartFunc of REAL,(REAL n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ) hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ) implies h is continuous ) assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous thus for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is continuous ) assume A2: i in Seg n ; ::_thesis: (proj (i,n)) * h is continuous A3: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; rng h c= REAL n ; then A4: dom ((proj (i,n)) * h) = dom h by A3, RELAT_1:27; now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((proj_(i,n))_*_h)_holds_ (proj_(i,n))_*_h_is_continuous_in_x0 let x0 be real number ; ::_thesis: ( x0 in dom ((proj (i,n)) * h) implies (proj (i,n)) * h is_continuous_in x0 ) assume x0 in dom ((proj (i,n)) * h) ; ::_thesis: (proj (i,n)) * h is_continuous_in x0 then h is_continuous_in x0 by A1, A4, Def5; hence (proj (i,n)) * h is_continuous_in x0 by A2, Th43; ::_thesis: verum end; hence (proj (i,n)) * h is continuous by FCONT_1:def_2; ::_thesis: verum end; end; assume A5: for i being Element of NAT st i in Seg n holds (proj (i,n)) * h is continuous ; ::_thesis: h is continuous let x0 be real number ; :: according to NFCONT_4:def_5 ::_thesis: ( x0 in dom h implies h is_continuous_in x0 ) assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0 now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ (proj_(i,n))_*_h_is_continuous_in_x0 let i be Element of NAT ; ::_thesis: ( i in Seg n implies (proj (i,n)) * h is_continuous_in x0 ) assume A7: i in Seg n ; ::_thesis: (proj (i,n)) * h is_continuous_in x0 A8: dom (proj (i,n)) = REAL n by FUNCT_2:def_1; rng h c= REAL n ; then A9: dom ((proj (i,n)) * h) = dom h by A8, RELAT_1:27; (proj (i,n)) * h is continuous by A5, A7; hence (proj (i,n)) * h is_continuous_in x0 by A6, A9, FCONT_1:def_2; ::_thesis: verum end; hence h is_continuous_in x0 by A6, Th43; ::_thesis: verum end; theorem Th45: :: NFCONT_4:45 for n, i being Element of NAT for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds Proj (i,n) is_continuous_in x0 proof let n, i be Element of NAT ; ::_thesis: for x0 being Point of (REAL-NS n) st 1 <= i & i <= n holds Proj (i,n) is_continuous_in x0 let x0 be Point of (REAL-NS n); ::_thesis: ( 1 <= i & i <= n implies Proj (i,n) is_continuous_in x0 ) assume A1: ( 1 <= i & i <= n ) ; ::_thesis: Proj (i,n) is_continuous_in x0 A2: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_s_being_Real_st_ (_0_<_s_&_(_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_ ||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r_)_) let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) ) ) assume A3: 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) ) take s = r; ::_thesis: ( 0 < s & ( for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) ) thus 0 < s by A3; ::_thesis: for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r now__::_thesis:_for_x1_being_Point_of_(REAL-NS_n)_st_x1_in_dom_(Proj_(i,n))_&_||.(x1_-_x0).||_<_s_holds_ ||.(((Proj_(i,n))_/._x1)_-_((Proj_(i,n))_/._x0)).||_<_r let x1 be Point of (REAL-NS n); ::_thesis: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s implies ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ) assume A4: ( x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s ) ; ::_thesis: ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r (Proj (i,n)) /. (x1 - x0) = ((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0) by A1, PDIFF_8:11; then ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| <= ||.(x1 - x0).|| by A1, PDIFF_8:3; hence ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r by A4, XXREAL_0:2; ::_thesis: verum end; hence for x1 being Point of (REAL-NS n) st x1 in dom (Proj (i,n)) & ||.(x1 - x0).|| < s holds ||.(((Proj (i,n)) /. x1) - ((Proj (i,n)) /. x0)).|| < r ; ::_thesis: verum end; hence Proj (i,n) is_continuous_in x0 by A2, NFCONT_1:7; ::_thesis: verum end; theorem Th46: :: NFCONT_4:46 for x0 being real number for n being non empty Element of NAT for h being PartFunc of REAL,(REAL-NS n) holds ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ) proof let x0 be real number ; ::_thesis: for n being non empty Element of NAT for h being PartFunc of REAL,(REAL-NS n) holds ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ) let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL-NS n) holds ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h is_continuous_in x0 iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ) hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ) implies h is_continuous_in x0 ) assume A1: h is_continuous_in x0 ; ::_thesis: for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 then A2: x0 in dom h by NFCONT_3:7; thus for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 ) assume i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0 then A3: ( 1 <= i & i <= n ) by FINSEQ_1:1; A4: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; rng h c= the carrier of (REAL-NS n) ; then A5: dom ((Proj (i,n)) * h) = dom h by A4, RELAT_1:27; Proj (i,n) is_continuous_in h /. x0 by A3, Th45; hence (Proj (i,n)) * h is_continuous_in x0 by A2, A5, A1, NFCONT_3:15; ::_thesis: verum end; end; assume A6: for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is_continuous_in x0 ; ::_thesis: h is_continuous_in x0 1 <= n by NAT_1:14; then 1 in Seg n by FINSEQ_1:1; then (Proj (1,n)) * h is_continuous_in x0 by A6; then A7: x0 in dom ((Proj (1,n)) * h) by NFCONT_3:8; A8: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25; for r being Real st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds ||.((h /. x1) - (h /. x0)).|| < r ) ) proof let r0 be Real; ::_thesis: ( 0 < r0 implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds ||.((h /. x1) - (h /. x0)).|| < r0 ) ) ) set r = r0 / 2; assume A9: 0 < r0 ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds ||.((h /. x1) - (h /. x0)).|| < r0 ) ) then A10: 0 < r0 / 2 by XREAL_1:215; defpred S1[ set , real number ] means ex j being Element of NAT st ( \$1 = j & 0 < \$2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < \$2 holds ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ); A11: 0 < (r0 / 2) / n by A10, XREAL_1:139; A12: for j0 being Nat st j0 in Seg n holds ex x being Element of REAL st S1[j0,x] proof let j0 be Nat; ::_thesis: ( j0 in Seg n implies ex x being Element of REAL st S1[j0,x] ) assume A13: j0 in Seg n ; ::_thesis: ex x being Element of REAL st S1[j0,x] reconsider j = j0 as Element of NAT by ORDINAL1:def_12; A14: (Proj (j,n)) * h is_continuous_in x0 by A6, A13; A15: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; rng h c= the carrier of (REAL-NS n) ; then A16: dom ((Proj (j,n)) * h) = dom h by A15, RELAT_1:27; consider sj being real number such that A17: ( 0 < sj & ( for x1 being real number st x1 in dom ((Proj (j,n)) * h) & abs (x1 - x0) < sj holds ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A14, A11, NFCONT_3:8; sj is Real by XREAL_0:def_1; hence ex x being Element of REAL st S1[j0,x] by A17, A16; ::_thesis: verum end; consider s0 being FinSequence of REAL such that A18: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds S1[k,s0 . k] ) ) from FINSEQ_1:sch_5(A12); n in Seg n by FINSEQ_1:3; then reconsider rs0 = rng s0 as non empty ext-real-membered set by A18, FUNCT_1:3; rng s0 is finite by A18, FINSET_1:8; then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ; A19: min rs0 in rng s0 by XXREAL_2:def_7; then reconsider s = min rs0 as Real ; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds ||.((h /. x1) - (h /. x0)).|| < r0 ) ) consider i1 being set such that A20: ( i1 in dom s0 & s = s0 . i1 ) by A19, FUNCT_1:def_3; ex j being Element of NAT st ( i1 = j & 0 < s0 . i1 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . i1 holds ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18, A20; hence 0 < s by A20; ::_thesis: for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds ||.((h /. x1) - (h /. x0)).|| < r0 let x1 be real number ; ::_thesis: ( x1 in dom h & abs (x1 - x0) < s implies ||.((h /. x1) - (h /. x0)).|| < r0 ) assume A21: ( x1 in dom h & abs (x1 - x0) < s ) ; ::_thesis: ||.((h /. x1) - (h /. x0)).|| < r0 now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_n_holds_ ||.((Proj_(j,n))_._((h_/._x1)_-_(h_/._x0))).||_<=_(r0_/_2)_/_n let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= n implies ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n ) assume ( 1 <= j & j <= n ) ; ::_thesis: ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n then A22: j in Seg n by FINSEQ_1:1; then consider jj being Element of NAT such that A23: ( jj = j & 0 < s0 . j & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . j holds ||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A18; s0 . j in rng s0 by A22, A18, FUNCT_1:3; then s <= s0 . j by XXREAL_2:def_7; then abs (x1 - x0) < s0 . j by A21, XXREAL_0:2; then A24: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by A23, A21; A25: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; then A26: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by A21, PARTFUN2:4; ((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by A25, A8, A7, PARTFUN2:4; hence ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by A24, A26, PDIFF_8:11; ::_thesis: verum end; then ||.((h /. x1) - (h /. x0)).|| <= n * ((r0 / 2) / n) by PDIFF_8:16; then A27: ||.((h /. x1) - (h /. x0)).|| <= r0 / 2 by XCMPLX_1:87; r0 / 2 < r0 by A9, XREAL_1:216; hence ||.((h /. x1) - (h /. x0)).|| < r0 by A27, XXREAL_0:2; ::_thesis: verum end; hence h is_continuous_in x0 by A8, A7, NFCONT_3:8; ::_thesis: verum end; theorem :: NFCONT_4:47 for n being non empty Element of NAT for h being PartFunc of REAL,(REAL-NS n) holds ( h is continuous iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ) proof let n be non empty Element of NAT ; ::_thesis: for h being PartFunc of REAL,(REAL-NS n) holds ( h is continuous iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ) let h be PartFunc of REAL,(REAL-NS n); ::_thesis: ( h is continuous iff for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ) hereby ::_thesis: ( ( for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ) implies h is continuous ) assume A1: h is continuous ; ::_thesis: for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous thus for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ::_thesis: verum proof let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is continuous ) assume A2: i in Seg n ; ::_thesis: (Proj (i,n)) * h is continuous A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; rng h c= the carrier of (REAL-NS n) ; then A4: dom ((Proj (i,n)) * h) = dom h by A3, RELAT_1:27; now__::_thesis:_for_x0_being_real_number_st_x0_in_dom_((Proj_(i,n))_*_h)_holds_ (Proj_(i,n))_*_h_is_continuous_in_x0 let x0 be real number ; ::_thesis: ( x0 in dom ((Proj (i,n)) * h) implies (Proj (i,n)) * h is_continuous_in x0 ) assume x0 in dom ((Proj (i,n)) * h) ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0 then h is_continuous_in x0 by A1, A4, NFCONT_3:def_2; hence (Proj (i,n)) * h is_continuous_in x0 by A2, Th46; ::_thesis: verum end; hence (Proj (i,n)) * h is continuous by NFCONT_3:def_2; ::_thesis: verum end; end; assume A5: for i being Element of NAT st i in Seg n holds (Proj (i,n)) * h is continuous ; ::_thesis: h is continuous let x0 be real number ; :: according to NFCONT_3:def_2 ::_thesis: ( not x0 in dom h or h is_continuous_in x0 ) assume A6: x0 in dom h ; ::_thesis: h is_continuous_in x0 now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_Seg_n_holds_ (Proj_(i,n))_*_h_is_continuous_in_x0 let i be Element of NAT ; ::_thesis: ( i in Seg n implies (Proj (i,n)) * h is_continuous_in x0 ) assume A7: i in Seg n ; ::_thesis: (Proj (i,n)) * h is_continuous_in x0 A8: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def_1; rng h c= the carrier of (REAL-NS n) ; then A9: dom ((Proj (i,n)) * h) = dom h by A8, RELAT_1:27; (Proj (i,n)) * h is continuous by A5, A7; hence (Proj (i,n)) * h is_continuous_in x0 by A6, A9, NFCONT_3:def_2; ::_thesis: verum end; hence h is_continuous_in x0 by Th46; ::_thesis: verum end;