:: SEQFUNC semantic presentation begin definition let D1, D2 be set ; mode Functional_Sequence of D1,D2 is sequence of (PFuncs (D1,D2)); end; definition let D1, D2 be set ; let F be Functional_Sequence of D1,D2; let n be Nat; :: original: . redefine funcF . n -> PartFunc of D1,D2; coherence F . n is PartFunc of D1,D2 proof n in NAT by ORDINAL1:def_12; then n in dom F by FUNCT_2:def_1; then F . n in rng F by FUNCT_1:def_3; hence F . n is PartFunc of D1,D2 by PARTFUN1:46; ::_thesis: verum end; end; Lm1: for D1, D2 being set for f being Function holds ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) ) ) proof let D1, D2 be set ; ::_thesis: for f being Function holds ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) ) ) let f be Function; ::_thesis: ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) ) ) thus ( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) ) ) ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 ) proof assume A1: f is Functional_Sequence of D1,D2 ; ::_thesis: ( dom f = NAT & ( for x being set st x in NAT holds f . x is PartFunc of D1,D2 ) ) hence dom f = NAT by FUNCT_2:def_1; ::_thesis: for x being set st x in NAT holds f . x is PartFunc of D1,D2 let x be set ; ::_thesis: ( x in NAT implies f . x is PartFunc of D1,D2 ) assume x in NAT ; ::_thesis: f . x is PartFunc of D1,D2 then x in dom f by A1, FUNCT_2:def_1; then A2: f . x in rng f by FUNCT_1:def_3; rng f c= PFuncs (D1,D2) by A1, RELAT_1:def_19; hence f . x is PartFunc of D1,D2 by A2, PARTFUN1:46; ::_thesis: verum end; assume that A3: dom f = NAT and A4: for x being set st x in NAT holds f . x is PartFunc of D1,D2 ; ::_thesis: f is Functional_Sequence of D1,D2 now__::_thesis:_for_y_being_set_st_y_in_rng_f_holds_ y_in_PFuncs_(D1,D2) let y be set ; ::_thesis: ( y in rng f implies y in PFuncs (D1,D2) ) assume y in rng f ; ::_thesis: y in PFuncs (D1,D2) then consider x being set such that A5: x in dom f and A6: y = f . x by FUNCT_1:def_3; f . x is PartFunc of D1,D2 by A3, A4, A5; hence y in PFuncs (D1,D2) by A6, PARTFUN1:45; ::_thesis: verum end; then rng f c= PFuncs (D1,D2) by TARSKI:def_3; hence f is Functional_Sequence of D1,D2 by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem :: SEQFUNC:1 for D1, D2 being set for f being Function holds ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) ) ) proof let D1, D2 be set ; ::_thesis: for f being Function holds ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) ) ) let f be Function; ::_thesis: ( f is Functional_Sequence of D1,D2 iff ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) ) ) thus ( f is Functional_Sequence of D1,D2 implies ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) ) ) by Lm1; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n is PartFunc of D1,D2 ) implies f is Functional_Sequence of D1,D2 ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n is PartFunc of D1,D2 ; ::_thesis: f is Functional_Sequence of D1,D2 for x being set st x in NAT holds f . x is PartFunc of D1,D2 by A2; hence f is Functional_Sequence of D1,D2 by A1, Lm1; ::_thesis: verum end; scheme :: SEQFUNC:sch 1 ExFuncSeq{ F1() -> set , F2() -> set , F3( set ) -> PartFunc of F1(),F2() } : ex G being Functional_Sequence of F1(),F2() st for n being Nat holds G . n = F3(n) proof defpred S1[ set , set ] means \$2 = F3(\$1); A1: for x being set st x in NAT holds ex y being set st S1[x,y] ; consider f being Function such that A2: dom f = NAT and A3: for x being set st x in NAT holds S1[x,f . x] from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_NAT_holds_ f_._x_is_PartFunc_of_F1(),F2() let x be set ; ::_thesis: ( x in NAT implies f . x is PartFunc of F1(),F2() ) assume x in NAT ; ::_thesis: f . x is PartFunc of F1(),F2() then f . x = F3(x) by A3; hence f . x is PartFunc of F1(),F2() ; ::_thesis: verum end; then reconsider f = f as Functional_Sequence of F1(),F2() by A2, Lm1; take f ; ::_thesis: for n being Nat holds f . n = F3(n) let n be Nat; ::_thesis: f . n = F3(n) n in NAT by ORDINAL1:def_12; hence f . n = F3(n) by A3; ::_thesis: verum end; definition let D be non empty set ; let H be Functional_Sequence of D,REAL; let r be real number ; funcr (#) H -> Functional_Sequence of D,REAL means :Def1: :: SEQFUNC:def 1 for n being Nat holds it . n = r (#) (H . n); existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = r (#) (H . n) proof deffunc H1( Nat) -> Element of K19(K20(D,REAL)) = r (#) (H . \$1); thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = r (#) (H . n) ) & ( for n being Nat holds b2 . n = r (#) (H . n) ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = r (#) (H . n) ) & ( for n being Nat holds H2 . n = r (#) (H . n) ) implies H1 = H2 ) assume that A1: for n being Nat holds H1 . n = r (#) (H . n) and A2: for n being Nat holds H2 . n = r (#) (H . n) ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H1 . n = r (#) (H . n) by A1; hence H1 . n = H2 . n by A2; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines (#) SEQFUNC:def_1_:_ for D being non empty set for H being Functional_Sequence of D,REAL for r being real number for b4 being Functional_Sequence of D,REAL holds ( b4 = r (#) H iff for n being Nat holds b4 . n = r (#) (H . n) ); definition let D be non empty set ; let H be Functional_Sequence of D,REAL; funcH " -> Functional_Sequence of D,REAL means :Def2: :: SEQFUNC:def 2 for n being Nat holds it . n = (H . n) ^ ; existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = (H . n) ^ proof deffunc H1( Nat) -> Element of K19(K20(D,REAL)) = (H . \$1) ^ ; thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = (H . n) ^ ) & ( for n being Nat holds b2 . n = (H . n) ^ ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (H . n) ^ ) & ( for n being Nat holds H2 . n = (H . n) ^ ) implies H1 = H2 ) assume that A1: for n being Nat holds H1 . n = (H . n) ^ and A2: for n being Nat holds H2 . n = (H . n) ^ ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H1 . n = (H . n) ^ by A1; hence H1 . n = H2 . n by A2; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; func - H -> Functional_Sequence of D,REAL means :Def3: :: SEQFUNC:def 3 for n being Nat holds it . n = - (H . n); existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = - (H . n) proof take (- 1) (#) H ; ::_thesis: for n being Nat holds ((- 1) (#) H) . n = - (H . n) let n be Nat; ::_thesis: ((- 1) (#) H) . n = - (H . n) thus ((- 1) (#) H) . n = - (H . n) by Def1; ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = - (H . n) ) & ( for n being Nat holds b2 . n = - (H . n) ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = - (H . n) ) & ( for n being Nat holds H2 . n = - (H . n) ) implies H1 = H2 ) assume that A3: for n being Nat holds H1 . n = - (H . n) and A4: for n being Nat holds H2 . n = - (H . n) ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H1 . n = - (H . n) by A3; hence H1 . n = H2 . n by A4; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; involutiveness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = - (b2 . n) ) holds for n being Nat holds b2 . n = - (b1 . n) proof let G, H be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds G . n = - (H . n) ) implies for n being Nat holds H . n = - (G . n) ) assume A5: for n being Nat holds G . n = - (H . n) ; ::_thesis: for n being Nat holds H . n = - (G . n) let n be Nat; ::_thesis: H . n = - (G . n) thus H . n = - (- (H . n)) .= - (G . n) by A5 ; ::_thesis: verum end; func abs H -> Functional_Sequence of D,REAL means :Def4: :: SEQFUNC:def 4 for n being Nat holds it . n = abs (H . n); existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = abs (H . n) proof deffunc H1( Nat) -> Element of K19(K20(D,REAL)) = abs (H . \$1); thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = abs (H . n) ) & ( for n being Nat holds b2 . n = abs (H . n) ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = abs (H . n) ) & ( for n being Nat holds H2 . n = abs (H . n) ) implies H1 = H2 ) assume that A6: for n being Nat holds H1 . n = abs (H . n) and A7: for n being Nat holds H2 . n = abs (H . n) ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H2 . n = abs (H . n) by A7; hence H1 . n = H2 . n by A6; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; projectivity for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = abs (b2 . n) ) holds for n being Nat holds b1 . n = abs (b1 . n) proof let G, H be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds G . n = abs (H . n) ) implies for n being Nat holds G . n = abs (G . n) ) assume A8: for n being Nat holds G . n = abs (H . n) ; ::_thesis: for n being Nat holds G . n = abs (G . n) let n be Nat; ::_thesis: G . n = abs (G . n) thus G . n = abs (abs (H . n)) by A8 .= abs (G . n) by A8 ; ::_thesis: verum end; end; :: deftheorem Def2 defines " SEQFUNC:def_2_:_ for D being non empty set for H, b3 being Functional_Sequence of D,REAL holds ( b3 = H " iff for n being Nat holds b3 . n = (H . n) ^ ); :: deftheorem Def3 defines - SEQFUNC:def_3_:_ for D being non empty set for H, b3 being Functional_Sequence of D,REAL holds ( b3 = - H iff for n being Nat holds b3 . n = - (H . n) ); :: deftheorem Def4 defines abs SEQFUNC:def_4_:_ for D being non empty set for H, b3 being Functional_Sequence of D,REAL holds ( b3 = abs H iff for n being Nat holds b3 . n = abs (H . n) ); definition let D be non empty set ; let G, H be Functional_Sequence of D,REAL; funcG + H -> Functional_Sequence of D,REAL means :Def5: :: SEQFUNC:def 5 for n being Nat holds it . n = (G . n) + (H . n); existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = (G . n) + (H . n) proof deffunc H1( Nat) -> Element of K19(K20(D,REAL)) = (G . \$1) + (H . \$1); thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = (G . n) + (H . n) ) & ( for n being Nat holds b2 . n = (G . n) + (H . n) ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (G . n) + (H . n) ) & ( for n being Nat holds H2 . n = (G . n) + (H . n) ) implies H1 = H2 ) assume that A1: for n being Nat holds H1 . n = (G . n) + (H . n) and A2: for n being Nat holds H2 . n = (G . n) + (H . n) ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H1 . n = (G . n) + (H . n) by A1; hence H1 . n = H2 . n by A2; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def5 defines + SEQFUNC:def_5_:_ for D being non empty set for G, H, b4 being Functional_Sequence of D,REAL holds ( b4 = G + H iff for n being Nat holds b4 . n = (G . n) + (H . n) ); definition let D be non empty set ; let G, H be Functional_Sequence of D,REAL; funcG - H -> Functional_Sequence of D,REAL equals :: SEQFUNC:def 6 G + (- H); correctness coherence G + (- H) is Functional_Sequence of D,REAL; ; end; :: deftheorem defines - SEQFUNC:def_6_:_ for D being non empty set for G, H being Functional_Sequence of D,REAL holds G - H = G + (- H); definition let D be non empty set ; let G, H be Functional_Sequence of D,REAL; funcG (#) H -> Functional_Sequence of D,REAL means :Def7: :: SEQFUNC:def 7 for n being Nat holds it . n = (G . n) (#) (H . n); existence ex b1 being Functional_Sequence of D,REAL st for n being Nat holds b1 . n = (G . n) (#) (H . n) proof deffunc H1( Nat) -> Element of K19(K20(D,REAL)) = (G . \$1) (#) (H . \$1); thus ex f being Functional_Sequence of D,REAL st for n being Nat holds f . n = H1(n) from SEQFUNC:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Functional_Sequence of D,REAL st ( for n being Nat holds b1 . n = (G . n) (#) (H . n) ) & ( for n being Nat holds b2 . n = (G . n) (#) (H . n) ) holds b1 = b2 proof let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: ( ( for n being Nat holds H1 . n = (G . n) (#) (H . n) ) & ( for n being Nat holds H2 . n = (G . n) (#) (H . n) ) implies H1 = H2 ) assume that A1: for n being Nat holds H1 . n = (G . n) (#) (H . n) and A2: for n being Nat holds H2 . n = (G . n) (#) (H . n) ; ::_thesis: H1 = H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_H2_._n let n be Element of NAT ; ::_thesis: H1 . n = H2 . n H1 . n = (G . n) (#) (H . n) by A1; hence H1 . n = H2 . n by A2; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def7 defines (#) SEQFUNC:def_7_:_ for D being non empty set for G, H, b4 being Functional_Sequence of D,REAL holds ( b4 = G (#) H iff for n being Nat holds b4 . n = (G . n) (#) (H . n) ); definition let D be non empty set ; let H, G be Functional_Sequence of D,REAL; funcG / H -> Functional_Sequence of D,REAL equals :: SEQFUNC:def 8 G (#) (H "); correctness coherence G (#) (H ") is Functional_Sequence of D,REAL; ; end; :: deftheorem defines / SEQFUNC:def_8_:_ for D being non empty set for H, G being Functional_Sequence of D,REAL holds G / H = G (#) (H "); theorem :: SEQFUNC:2 for D being non empty set for H1, G, H being Functional_Sequence of D,REAL holds ( H1 = G / H iff for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) proof let D be non empty set ; ::_thesis: for H1, G, H being Functional_Sequence of D,REAL holds ( H1 = G / H iff for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) let H1, G, H be Functional_Sequence of D,REAL; ::_thesis: ( H1 = G / H iff for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) thus ( H1 = G / H implies for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) ::_thesis: ( ( for n being Element of NAT holds H1 . n = (G . n) / (H . n) ) implies H1 = G / H ) proof assume A1: H1 = G / H ; ::_thesis: for n being Element of NAT holds H1 . n = (G . n) / (H . n) let n be Element of NAT ; ::_thesis: H1 . n = (G . n) / (H . n) thus H1 . n = (G . n) (#) ((H ") . n) by A1, Def7 .= (G . n) (#) ((H . n) ^) by Def2 .= (G . n) / (H . n) by RFUNCT_1:31 ; ::_thesis: verum end; assume A2: for n being Element of NAT holds H1 . n = (G . n) / (H . n) ; ::_thesis: H1 = G / H now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_(G_/_H)_._n let n be Element of NAT ; ::_thesis: H1 . n = (G / H) . n thus H1 . n = (G . n) / (H . n) by A2 .= (G . n) (#) ((H . n) ^) by RFUNCT_1:31 .= (G . n) (#) ((H ") . n) by Def2 .= (G / H) . n by Def7 ; ::_thesis: verum end; hence H1 = G / H by FUNCT_2:63; ::_thesis: verum end; theorem Th3: :: SEQFUNC:3 for D being non empty set for H1, G, H being Functional_Sequence of D,REAL holds ( H1 = G - H iff for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) proof let D be non empty set ; ::_thesis: for H1, G, H being Functional_Sequence of D,REAL holds ( H1 = G - H iff for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) let H1, G, H be Functional_Sequence of D,REAL; ::_thesis: ( H1 = G - H iff for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) thus ( H1 = G - H implies for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) ::_thesis: ( ( for n being Element of NAT holds H1 . n = (G . n) - (H . n) ) implies H1 = G - H ) proof assume A1: H1 = G - H ; ::_thesis: for n being Element of NAT holds H1 . n = (G . n) - (H . n) let n be Element of NAT ; ::_thesis: H1 . n = (G . n) - (H . n) thus H1 . n = (G . n) + ((- H) . n) by A1, Def5 .= (G . n) - (H . n) by Def3 ; ::_thesis: verum end; assume A2: for n being Element of NAT holds H1 . n = (G . n) - (H . n) ; ::_thesis: H1 = G - H now__::_thesis:_for_n_being_Element_of_NAT_holds_H1_._n_=_(G_-_H)_._n let n be Element of NAT ; ::_thesis: H1 . n = (G - H) . n thus H1 . n = (G . n) - (H . n) by A2 .= (G . n) + ((- H) . n) by Def3 .= (G - H) . n by Def5 ; ::_thesis: verum end; hence H1 = G - H by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:4 for D being non empty set for G, H, J being Functional_Sequence of D,REAL holds ( G + H = H + G & (G + H) + J = G + (H + J) ) proof let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds ( G + H = H + G & (G + H) + J = G + (H + J) ) let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( G + H = H + G & (G + H) + J = G + (H + J) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(G_+_H)_._n_=_(H_+_G)_._n let n be Element of NAT ; ::_thesis: (G + H) . n = (H + G) . n thus (G + H) . n = (H . n) + (G . n) by Def5 .= (H + G) . n by Def5 ; ::_thesis: verum end; hence G + H = H + G by FUNCT_2:63; ::_thesis: (G + H) + J = G + (H + J) now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_+_H)_+_J)_._n_=_(G_+_(H_+_J))_._n let n be Element of NAT ; ::_thesis: ((G + H) + J) . n = (G + (H + J)) . n thus ((G + H) + J) . n = ((G + H) . n) + (J . n) by Def5 .= ((G . n) + (H . n)) + (J . n) by Def5 .= (G . n) + ((H . n) + (J . n)) by RFUNCT_1:8 .= (G . n) + ((H + J) . n) by Def5 .= (G + (H + J)) . n by Def5 ; ::_thesis: verum end; hence (G + H) + J = G + (H + J) by FUNCT_2:63; ::_thesis: verum end; theorem Th5: :: SEQFUNC:5 for D being non empty set for G, H, J being Functional_Sequence of D,REAL holds ( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) ) proof let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds ( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) ) let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( G (#) H = H (#) G & (G (#) H) (#) J = G (#) (H (#) J) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(G_(#)_H)_._n_=_(H_(#)_G)_._n let n be Element of NAT ; ::_thesis: (G (#) H) . n = (H (#) G) . n thus (G (#) H) . n = (H . n) (#) (G . n) by Def7 .= (H (#) G) . n by Def7 ; ::_thesis: verum end; hence G (#) H = H (#) G by FUNCT_2:63; ::_thesis: (G (#) H) (#) J = G (#) (H (#) J) now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_(#)_H)_(#)_J)_._n_=_(G_(#)_(H_(#)_J))_._n let n be Element of NAT ; ::_thesis: ((G (#) H) (#) J) . n = (G (#) (H (#) J)) . n thus ((G (#) H) (#) J) . n = ((G (#) H) . n) (#) (J . n) by Def7 .= ((G . n) (#) (H . n)) (#) (J . n) by Def7 .= (G . n) (#) ((H . n) (#) (J . n)) by RFUNCT_1:9 .= (G . n) (#) ((H (#) J) . n) by Def7 .= (G (#) (H (#) J)) . n by Def7 ; ::_thesis: verum end; hence (G (#) H) (#) J = G (#) (H (#) J) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:6 for D being non empty set for G, H, J being Functional_Sequence of D,REAL holds ( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) ) proof let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds ( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) ) let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( (G + H) (#) J = (G (#) J) + (H (#) J) & J (#) (G + H) = (J (#) G) + (J (#) H) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_+_H)_(#)_J)_._n_=_((G_(#)_J)_+_(H_(#)_J))_._n let n be Element of NAT ; ::_thesis: ((G + H) (#) J) . n = ((G (#) J) + (H (#) J)) . n thus ((G + H) (#) J) . n = ((G + H) . n) (#) (J . n) by Def7 .= ((G . n) + (H . n)) (#) (J . n) by Def5 .= ((G . n) (#) (J . n)) + ((H . n) (#) (J . n)) by RFUNCT_1:10 .= ((G (#) J) . n) + ((H . n) (#) (J . n)) by Def7 .= ((G (#) J) . n) + ((H (#) J) . n) by Def7 .= ((G (#) J) + (H (#) J)) . n by Def5 ; ::_thesis: verum end; hence (G + H) (#) J = (G (#) J) + (H (#) J) by FUNCT_2:63; ::_thesis: J (#) (G + H) = (J (#) G) + (J (#) H) hence J (#) (G + H) = (G (#) J) + (H (#) J) by Th5 .= (J (#) G) + (H (#) J) by Th5 .= (J (#) G) + (J (#) H) by Th5 ; ::_thesis: verum end; theorem :: SEQFUNC:7 for D being non empty set for H being Functional_Sequence of D,REAL holds - H = (- 1) (#) H proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds - H = (- 1) (#) H let H be Functional_Sequence of D,REAL; ::_thesis: - H = (- 1) (#) H now__::_thesis:_for_n_being_Element_of_NAT_holds_(-_H)_._n_=_((-_1)_(#)_H)_._n let n be Element of NAT ; ::_thesis: (- H) . n = ((- 1) (#) H) . n thus (- H) . n = - (H . n) by Def3 .= ((- 1) (#) H) . n by Def1 ; ::_thesis: verum end; hence - H = (- 1) (#) H by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:8 for D being non empty set for G, H, J being Functional_Sequence of D,REAL holds ( (G - H) (#) J = (G (#) J) - (H (#) J) & (J (#) G) - (J (#) H) = J (#) (G - H) ) proof let D be non empty set ; ::_thesis: for G, H, J being Functional_Sequence of D,REAL holds ( (G - H) (#) J = (G (#) J) - (H (#) J) & (J (#) G) - (J (#) H) = J (#) (G - H) ) let G, H, J be Functional_Sequence of D,REAL; ::_thesis: ( (G - H) (#) J = (G (#) J) - (H (#) J) & (J (#) G) - (J (#) H) = J (#) (G - H) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_-_H)_(#)_J)_._n_=_((G_(#)_J)_-_(H_(#)_J))_._n let n be Element of NAT ; ::_thesis: ((G - H) (#) J) . n = ((G (#) J) - (H (#) J)) . n thus ((G - H) (#) J) . n = ((G - H) . n) (#) (J . n) by Def7 .= ((G . n) - (H . n)) (#) (J . n) by Th3 .= ((G . n) (#) (J . n)) - ((H . n) (#) (J . n)) by RFUNCT_1:14 .= ((G (#) J) . n) - ((H . n) (#) (J . n)) by Def7 .= ((G (#) J) . n) - ((H (#) J) . n) by Def7 .= ((G (#) J) - (H (#) J)) . n by Th3 ; ::_thesis: verum end; hence A1: (G - H) (#) J = (G (#) J) - (H (#) J) by FUNCT_2:63; ::_thesis: (J (#) G) - (J (#) H) = J (#) (G - H) thus (J (#) G) - (J (#) H) = (J (#) G) - (H (#) J) by Th5 .= (G - H) (#) J by A1, Th5 .= J (#) (G - H) by Th5 ; ::_thesis: verum end; theorem :: SEQFUNC:9 for D being non empty set for r being Real for G, H being Functional_Sequence of D,REAL holds ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) ) proof let D be non empty set ; ::_thesis: for r being Real for G, H being Functional_Sequence of D,REAL holds ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) ) let r be Real; ::_thesis: for G, H being Functional_Sequence of D,REAL holds ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) ) let G, H be Functional_Sequence of D,REAL; ::_thesis: ( r (#) (G + H) = (r (#) G) + (r (#) H) & r (#) (G - H) = (r (#) G) - (r (#) H) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(G_+_H))_._n_=_((r_(#)_G)_+_(r_(#)_H))_._n let n be Element of NAT ; ::_thesis: (r (#) (G + H)) . n = ((r (#) G) + (r (#) H)) . n thus (r (#) (G + H)) . n = r (#) ((G + H) . n) by Def1 .= r (#) ((G . n) + (H . n)) by Def5 .= (r (#) (G . n)) + (r (#) (H . n)) by RFUNCT_1:16 .= ((r (#) G) . n) + (r (#) (H . n)) by Def1 .= ((r (#) G) . n) + ((r (#) H) . n) by Def1 .= ((r (#) G) + (r (#) H)) . n by Def5 ; ::_thesis: verum end; hence r (#) (G + H) = (r (#) G) + (r (#) H) by FUNCT_2:63; ::_thesis: r (#) (G - H) = (r (#) G) - (r (#) H) now__::_thesis:_for_n_being_Element_of_NAT_holds_(r_(#)_(G_-_H))_._n_=_((r_(#)_G)_-_(r_(#)_H))_._n let n be Element of NAT ; ::_thesis: (r (#) (G - H)) . n = ((r (#) G) - (r (#) H)) . n thus (r (#) (G - H)) . n = r (#) ((G - H) . n) by Def1 .= r (#) ((G . n) - (H . n)) by Th3 .= (r (#) (G . n)) - (r (#) (H . n)) by RFUNCT_1:18 .= ((r (#) G) . n) - (r (#) (H . n)) by Def1 .= ((r (#) G) . n) - ((r (#) H) . n) by Def1 .= ((r (#) G) - (r (#) H)) . n by Th3 ; ::_thesis: verum end; hence r (#) (G - H) = (r (#) G) - (r (#) H) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:10 for D being non empty set for r, p being Real for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H) proof let D be non empty set ; ::_thesis: for r, p being Real for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H) let r, p be Real; ::_thesis: for H being Functional_Sequence of D,REAL holds (r * p) (#) H = r (#) (p (#) H) let H be Functional_Sequence of D,REAL; ::_thesis: (r * p) (#) H = r (#) (p (#) H) now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_*_p)_(#)_H)_._n_=_(r_(#)_(p_(#)_H))_._n let n be Element of NAT ; ::_thesis: ((r * p) (#) H) . n = (r (#) (p (#) H)) . n thus ((r * p) (#) H) . n = (r * p) (#) (H . n) by Def1 .= r (#) (p (#) (H . n)) by RFUNCT_1:17 .= r (#) ((p (#) H) . n) by Def1 .= (r (#) (p (#) H)) . n by Def1 ; ::_thesis: verum end; hence (r * p) (#) H = r (#) (p (#) H) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:11 for D being non empty set for H being Functional_Sequence of D,REAL holds 1 (#) H = H proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds 1 (#) H = H let H be Functional_Sequence of D,REAL; ::_thesis: 1 (#) H = H now__::_thesis:_for_n_being_Element_of_NAT_holds_(1_(#)_H)_._n_=_H_._n let n be Element of NAT ; ::_thesis: (1 (#) H) . n = H . n thus (1 (#) H) . n = 1 (#) (H . n) by Def1 .= H . n by RFUNCT_1:21 ; ::_thesis: verum end; hence 1 (#) H = H by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:12 canceled; theorem :: SEQFUNC:13 for D being non empty set for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) " proof let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds (G ") (#) (H ") = (G (#) H) " let G, H be Functional_Sequence of D,REAL; ::_thesis: (G ") (#) (H ") = (G (#) H) " now__::_thesis:_for_n_being_Element_of_NAT_holds_((G_")_(#)_(H_"))_._n_=_((G_(#)_H)_")_._n let n be Element of NAT ; ::_thesis: ((G ") (#) (H ")) . n = ((G (#) H) ") . n thus ((G ") (#) (H ")) . n = ((G ") . n) (#) ((H ") . n) by Def7 .= ((G . n) ^) (#) ((H ") . n) by Def2 .= ((G . n) ^) (#) ((H . n) ^) by Def2 .= ((G . n) (#) (H . n)) ^ by RFUNCT_1:27 .= ((G (#) H) . n) ^ by Def7 .= ((G (#) H) ") . n by Def2 ; ::_thesis: verum end; hence (G ") (#) (H ") = (G (#) H) " by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:14 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL st r <> 0 holds (r (#) H) " = (r ") (#) (H ") proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL st r <> 0 holds (r (#) H) " = (r ") (#) (H ") let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL st r <> 0 holds (r (#) H) " = (r ") (#) (H ") let H be Functional_Sequence of D,REAL; ::_thesis: ( r <> 0 implies (r (#) H) " = (r ") (#) (H ") ) assume A1: r <> 0 ; ::_thesis: (r (#) H) " = (r ") (#) (H ") now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_H)_")_._n_=_((r_")_(#)_(H_"))_._n let n be Element of NAT ; ::_thesis: ((r (#) H) ") . n = ((r ") (#) (H ")) . n thus ((r (#) H) ") . n = ((r (#) H) . n) ^ by Def2 .= (r (#) (H . n)) ^ by Def1 .= (r ") (#) ((H . n) ^) by A1, RFUNCT_1:28 .= (r ") (#) ((H ") . n) by Def2 .= ((r ") (#) (H ")) . n by Def1 ; ::_thesis: verum end; hence (r (#) H) " = (r ") (#) (H ") by FUNCT_2:63; ::_thesis: verum end; theorem Th15: :: SEQFUNC:15 for D being non empty set for H being Functional_Sequence of D,REAL holds (abs H) " = abs (H ") proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL holds (abs H) " = abs (H ") let H be Functional_Sequence of D,REAL; ::_thesis: (abs H) " = abs (H ") now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(H_"))_._n_=_((abs_H)_")_._n let n be Element of NAT ; ::_thesis: (abs (H ")) . n = ((abs H) ") . n thus (abs (H ")) . n = abs ((H ") . n) by Def4 .= abs ((H . n) ^) by Def2 .= (abs (H . n)) ^ by RFUNCT_1:30 .= ((abs H) . n) ^ by Def4 .= ((abs H) ") . n by Def2 ; ::_thesis: verum end; hence (abs H) " = abs (H ") by FUNCT_2:63; ::_thesis: verum end; theorem Th16: :: SEQFUNC:16 for D being non empty set for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H) proof let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds abs (G (#) H) = (abs G) (#) (abs H) let G, H be Functional_Sequence of D,REAL; ::_thesis: abs (G (#) H) = (abs G) (#) (abs H) now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(G_(#)_H))_._n_=_((abs_G)_(#)_(abs_H))_._n let n be Element of NAT ; ::_thesis: (abs (G (#) H)) . n = ((abs G) (#) (abs H)) . n thus (abs (G (#) H)) . n = abs ((G (#) H) . n) by Def4 .= abs ((G . n) (#) (H . n)) by Def7 .= (abs (G . n)) (#) (abs (H . n)) by RFUNCT_1:24 .= ((abs G) . n) (#) (abs (H . n)) by Def4 .= ((abs G) . n) (#) ((abs H) . n) by Def4 .= ((abs G) (#) (abs H)) . n by Def7 ; ::_thesis: verum end; hence abs (G (#) H) = (abs G) (#) (abs H) by FUNCT_2:63; ::_thesis: verum end; theorem :: SEQFUNC:17 for D being non empty set for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H) proof let D be non empty set ; ::_thesis: for G, H being Functional_Sequence of D,REAL holds abs (G / H) = (abs G) / (abs H) let G, H be Functional_Sequence of D,REAL; ::_thesis: abs (G / H) = (abs G) / (abs H) thus abs (G / H) = (abs G) (#) (abs (H ")) by Th16 .= (abs G) / (abs H) by Th15 ; ::_thesis: verum end; theorem :: SEQFUNC:18 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL holds abs (r (#) H) = (abs r) (#) (abs H) proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL holds abs (r (#) H) = (abs r) (#) (abs H) let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL holds abs (r (#) H) = (abs r) (#) (abs H) let H be Functional_Sequence of D,REAL; ::_thesis: abs (r (#) H) = (abs r) (#) (abs H) now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(r_(#)_H))_._n_=_((abs_r)_(#)_(abs_H))_._n let n be Element of NAT ; ::_thesis: (abs (r (#) H)) . n = ((abs r) (#) (abs H)) . n thus (abs (r (#) H)) . n = abs ((r (#) H) . n) by Def4 .= abs (r (#) (H . n)) by Def1 .= (abs r) (#) (abs (H . n)) by RFUNCT_1:25 .= (abs r) (#) ((abs H) . n) by Def4 .= ((abs r) (#) (abs H)) . n by Def1 ; ::_thesis: verum end; hence abs (r (#) H) = (abs r) (#) (abs H) by FUNCT_2:63; ::_thesis: verum end; definition let D1, D2 be set ; let F be Functional_Sequence of D1,D2; let X be set ; predX common_on_dom F means :Def9: :: SEQFUNC:def 9 ( X <> {} & ( for n being Element of NAT holds X c= dom (F . n) ) ); end; :: deftheorem Def9 defines common_on_dom SEQFUNC:def_9_:_ for D1, D2 being set for F being Functional_Sequence of D1,D2 for X being set holds ( X common_on_dom F iff ( X <> {} & ( for n being Element of NAT holds X c= dom (F . n) ) ) ); definition let D be non empty set ; let H be Functional_Sequence of D,REAL; let x be Element of D; funcH # x -> Real_Sequence means :Def10: :: SEQFUNC:def 10 for n being Element of NAT holds it . n = (H . n) . x; existence ex b1 being Real_Sequence st for n being Element of NAT holds b1 . n = (H . n) . x proof deffunc H1( Element of NAT ) -> Element of REAL = (H . \$1) . x; thus ex f being Real_Sequence st for n being Element of NAT holds f . n = H1(n) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for n being Element of NAT holds b1 . n = (H . n) . x ) & ( for n being Element of NAT holds b2 . n = (H . n) . x ) holds b1 = b2 proof let S1, S2 be Real_Sequence; ::_thesis: ( ( for n being Element of NAT holds S1 . n = (H . n) . x ) & ( for n being Element of NAT holds S2 . n = (H . n) . x ) implies S1 = S2 ) assume that A1: for n being Element of NAT holds S1 . n = (H . n) . x and A2: for n being Element of NAT holds S2 . n = (H . n) . x ; ::_thesis: S1 = S2 now__::_thesis:_for_n_being_Element_of_NAT_holds_S1_._n_=_S2_._n let n be Element of NAT ; ::_thesis: S1 . n = S2 . n S1 . n = (H . n) . x by A1; hence S1 . n = S2 . n by A2; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def10 defines # SEQFUNC:def_10_:_ for D being non empty set for H being Functional_Sequence of D,REAL for x being Element of D for b4 being Real_Sequence holds ( b4 = H # x iff for n being Element of NAT holds b4 . n = (H . n) . x ); definition let D be non empty set ; let H be Functional_Sequence of D,REAL; let X be set ; predH is_point_conv_on X means :Def11: :: SEQFUNC:def 11 ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ); end; :: deftheorem Def11 defines is_point_conv_on SEQFUNC:def_11_:_ for D being non empty set for H being Functional_Sequence of D,REAL for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) ); theorem Th19: :: SEQFUNC:19 for D being non empty set for H being Functional_Sequence of D,REAL for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) let X be set ; ::_thesis: ( H is_point_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) thus ( H is_point_conv_on X implies ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) ) ::_thesis: ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) implies H is_point_conv_on X ) proof assume A1: H is_point_conv_on X ; ::_thesis: ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) ) hence X common_on_dom H by Def11; ::_thesis: ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) consider f being PartFunc of D,REAL such that A2: X = dom f and A3: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p by A1, Def11; take f ; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) thus X = dom f by A2; ::_thesis: for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) let x be Element of D; ::_thesis: ( x in X implies ( H # x is convergent & lim (H # x) = f . x ) ) assume A4: x in X ; ::_thesis: ( H # x is convergent & lim (H # x) = f . x ) A5: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((H_#_x)_._n)_-_(f_._x))_<_p let p be real number ; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p ) assume A6: p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p p is Real by XREAL_0:def_1; then consider k being Element of NAT such that A7: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p by A3, A4, A6; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H # x) . n) - (f . x)) < p then abs (((H . n) . x) - (f . x)) < p by A7; hence abs (((H # x) . n) - (f . x)) < p by Def10; ::_thesis: verum end; hence H # x is convergent by SEQ_2:def_6; ::_thesis: lim (H # x) = f . x hence lim (H # x) = f . x by A5, SEQ_2:def_7; ::_thesis: verum end; assume A8: X common_on_dom H ; ::_thesis: ( for f being PartFunc of D,REAL holds ( not X = dom f or ex x being Element of D st ( x in X & not ( H # x is convergent & lim (H # x) = f . x ) ) ) or H is_point_conv_on X ) given f being PartFunc of D,REAL such that A9: X = dom f and A10: for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ; ::_thesis: H is_point_conv_on X ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) proof take f ; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) thus X = dom f by A9; ::_thesis: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let x be Element of D; ::_thesis: ( x in X implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume x in X ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p then A11: ( H # x is convergent & lim (H # x) = f . x ) by A10; let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p then consider k being Element of NAT such that A12: for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p by A11, SEQ_2:def_7; take k ; ::_thesis: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p then abs (((H # x) . n) - (f . x)) < p by A12; hence abs (((H . n) . x) - (f . x)) < p by Def10; ::_thesis: verum end; hence H is_point_conv_on X by A8, Def11; ::_thesis: verum end; theorem Th20: :: SEQFUNC:20 for D being non empty set for H being Functional_Sequence of D,REAL for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set holds ( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) ) let X be set ; ::_thesis: ( H is_point_conv_on X iff ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) ) defpred S1[ set ] means \$1 in X; deffunc H1( Element of D) -> Element of REAL = lim (H # \$1); consider f being PartFunc of D,REAL such that A1: for x being Element of D holds ( x in dom f iff S1[x] ) and A2: for x being Element of D st x in dom f holds f . x = H1(x) from SEQ_1:sch_3(); thus ( H is_point_conv_on X implies ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) ) ::_thesis: ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) implies H is_point_conv_on X ) proof assume A3: H is_point_conv_on X ; ::_thesis: ( X common_on_dom H & ( for x being Element of D st x in X holds H # x is convergent ) ) hence X common_on_dom H by Def11; ::_thesis: for x being Element of D st x in X holds H # x is convergent let x be Element of D; ::_thesis: ( x in X implies H # x is convergent ) assume A4: x in X ; ::_thesis: H # x is convergent ex f being PartFunc of D,REAL st ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) ) ) by A3, Th19; hence H # x is convergent by A4; ::_thesis: verum end; assume that A5: X common_on_dom H and A6: for x being Element of D st x in X holds H # x is convergent ; ::_thesis: H is_point_conv_on X now__::_thesis:_ex_f_being_PartFunc_of_D,REAL_st_ (_X_=_dom_f_&_(_for_x_being_Element_of_D_st_x_in_X_holds_ (_H_#_x_is_convergent_&_f_._x_=_lim_(H_#_x)_)_)_) take f = f; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds ( H # x is convergent & f . x = lim (H # x) ) ) ) thus A7: X = dom f ::_thesis: for x being Element of D st x in X holds ( H # x is convergent & f . x = lim (H # x) ) proof thus X c= dom f :: according to XBOOLE_0:def_10 ::_thesis: dom f c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom f ) assume A8: x in X ; ::_thesis: x in dom f X c= dom (H . 0) by A5, Def9; then X c= D by XBOOLE_1:1; then reconsider x9 = x as Element of D by A8; x9 in dom f by A1, A8; hence x in dom f ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in X ) assume x in dom f ; ::_thesis: x in X hence x in X by A1; ::_thesis: verum end; let x be Element of D; ::_thesis: ( x in X implies ( H # x is convergent & f . x = lim (H # x) ) ) assume A9: x in X ; ::_thesis: ( H # x is convergent & f . x = lim (H # x) ) hence H # x is convergent by A6; ::_thesis: f . x = lim (H # x) thus f . x = lim (H # x) by A2, A7, A9; ::_thesis: verum end; hence H is_point_conv_on X by A5, Th19; ::_thesis: verum end; definition let D be non empty set ; let H be Functional_Sequence of D,REAL; let X be set ; predH is_unif_conv_on X means :Def12: :: SEQFUNC:def 12 ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p ) ) ); end; :: deftheorem Def12 defines is_unif_conv_on SEQFUNC:def_12_:_ for D being non empty set for H being Functional_Sequence of D,REAL for X being set holds ( H is_unif_conv_on X iff ( X common_on_dom H & ex f being PartFunc of D,REAL st ( X = dom f & ( for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p ) ) ) ); definition let D be non empty set ; let H be Functional_Sequence of D,REAL; let X be set ; assume A1: H is_point_conv_on X ; func lim (H,X) -> PartFunc of D,REAL means :Def13: :: SEQFUNC:def 13 ( dom it = X & ( for x being Element of D st x in dom it holds it . x = lim (H # x) ) ); existence ex b1 being PartFunc of D,REAL st ( dom b1 = X & ( for x being Element of D st x in dom b1 holds b1 . x = lim (H # x) ) ) proof consider f being PartFunc of D,REAL such that A2: X = dom f and A3: for x being Element of D st x in X holds ( H # x is convergent & lim (H # x) = f . x ) by A1, Th19; take f ; ::_thesis: ( dom f = X & ( for x being Element of D st x in dom f holds f . x = lim (H # x) ) ) thus dom f = X by A2; ::_thesis: for x being Element of D st x in dom f holds f . x = lim (H # x) let x be Element of D; ::_thesis: ( x in dom f implies f . x = lim (H # x) ) assume x in dom f ; ::_thesis: f . x = lim (H # x) hence f . x = lim (H # x) by A2, A3; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of D,REAL st dom b1 = X & ( for x being Element of D st x in dom b1 holds b1 . x = lim (H # x) ) & dom b2 = X & ( for x being Element of D st x in dom b2 holds b2 . x = lim (H # x) ) holds b1 = b2 proof deffunc H1( Element of D) -> Element of REAL = lim (H # \$1); thus for f1, f2 being PartFunc of D,REAL st dom f1 = X & ( for x being Element of D st x in dom f1 holds f1 . x = H1(x) ) & dom f2 = X & ( for x being Element of D st x in dom f2 holds f2 . x = H1(x) ) holds f1 = f2 from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem Def13 defines lim SEQFUNC:def_13_:_ for D being non empty set for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for b4 being PartFunc of D,REAL holds ( b4 = lim (H,X) iff ( dom b4 = X & ( for x being Element of D st x in dom b4 holds b4 . x = lim (H # x) ) ) ); theorem Th21: :: SEQFUNC:21 for D being non empty set for H being Functional_Sequence of D,REAL for X being set for f being PartFunc of D,REAL st H is_point_conv_on X holds ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set for f being PartFunc of D,REAL st H is_point_conv_on X holds ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set for f being PartFunc of D,REAL st H is_point_conv_on X holds ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) let X be set ; ::_thesis: for f being PartFunc of D,REAL st H is_point_conv_on X holds ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) let f be PartFunc of D,REAL; ::_thesis: ( H is_point_conv_on X implies ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) ) assume A1: H is_point_conv_on X ; ::_thesis: ( f = lim (H,X) iff ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) thus ( f = lim (H,X) implies ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) ) ::_thesis: ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) implies f = lim (H,X) ) proof assume A2: f = lim (H,X) ; ::_thesis: ( dom f = X & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) hence A3: dom f = X by A1, Def13; ::_thesis: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let x be Element of D; ::_thesis: ( x in X implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume A4: x in X ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p then A5: H # x is convergent by A1, Th20; let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume A6: p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p f . x = lim (H # x) by A1, A2, A3, A4, Def13; then consider k being Element of NAT such that A7: for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p by A5, A6, SEQ_2:def_7; take k ; ::_thesis: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p then abs (((H # x) . n) - (f . x)) < p by A7; hence abs (((H . n) . x) - (f . x)) < p by Def10; ::_thesis: verum end; assume that A8: dom f = X and A9: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ; ::_thesis: f = lim (H,X) now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_f_holds_ f_._x_=_lim_(H_#_x) let x be Element of D; ::_thesis: ( x in dom f implies f . x = lim (H # x) ) assume A10: x in dom f ; ::_thesis: f . x = lim (H # x) A11: now__::_thesis:_for_p_being_real_number_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((H_#_x)_._n)_-_(f_._x))_<_p let p be real number ; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p ) assume A12: p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p p is Real by XREAL_0:def_1; then consider k being Element of NAT such that A13: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p by A8, A9, A10, A12; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((H # x) . n) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H # x) . n) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H # x) . n) - (f . x)) < p then abs (((H . n) . x) - (f . x)) < p by A13; hence abs (((H # x) . n) - (f . x)) < p by Def10; ::_thesis: verum end; then H # x is convergent by SEQ_2:def_6; hence f . x = lim (H # x) by A11, SEQ_2:def_7; ::_thesis: verum end; hence f = lim (H,X) by A1, A8, Def13; ::_thesis: verum end; theorem Th22: :: SEQFUNC:22 for D being non empty set for H being Functional_Sequence of D,REAL for X being set st H is_unif_conv_on X holds H is_point_conv_on X proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st H is_unif_conv_on X holds H is_point_conv_on X let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_unif_conv_on X holds H is_point_conv_on X let X be set ; ::_thesis: ( H is_unif_conv_on X implies H is_point_conv_on X ) assume A1: H is_unif_conv_on X ; ::_thesis: H is_point_conv_on X A2: now__::_thesis:_ex_f_being_PartFunc_of_D,REAL_st_ (_X_=_dom_f_&_(_for_x_being_Element_of_D_st_x_in_X_holds_ for_p_being_Real_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((H_._n)_._x)_-_(f_._x))_<_p_)_) consider f being PartFunc of D,REAL such that A3: X = dom f and A4: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by A1, Def12; take f = f; ::_thesis: ( X = dom f & ( for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) ) thus X = dom f by A3; ::_thesis: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let x be Element of D; ::_thesis: ( x in X implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume A5: x in X ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p then consider k being Element of NAT such that A6: for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by A4; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p hence abs (((H . n) . x) - (f . x)) < p by A5, A6; ::_thesis: verum end; X common_on_dom H by A1, Def12; hence H is_point_conv_on X by A2, Def11; ::_thesis: verum end; theorem Th23: :: SEQFUNC:23 for D being non empty set for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds Y common_on_dom H proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds Y common_on_dom H let H be Functional_Sequence of D,REAL; ::_thesis: for Y, X being set st Y c= X & Y <> {} & X common_on_dom H holds Y common_on_dom H let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & X common_on_dom H implies Y common_on_dom H ) assume that A1: Y c= X and A2: Y <> {} and A3: X common_on_dom H ; ::_thesis: Y common_on_dom H now__::_thesis:_for_n_being_Element_of_NAT_holds_Y_c=_dom_(H_._n) let n be Element of NAT ; ::_thesis: Y c= dom (H . n) X c= dom (H . n) by A3, Def9; hence Y c= dom (H . n) by A1, XBOOLE_1:1; ::_thesis: verum end; hence Y common_on_dom H by A2, Def9; ::_thesis: verum end; theorem :: SEQFUNC:24 for D being non empty set for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & H is_point_conv_on X holds ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & H is_point_conv_on X holds ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) let H be Functional_Sequence of D,REAL; ::_thesis: for Y, X being set st Y c= X & Y <> {} & H is_point_conv_on X holds ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & H is_point_conv_on X implies ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) ) assume that A1: Y c= X and A2: Y <> {} and A3: H is_point_conv_on X ; ::_thesis: ( H is_point_conv_on Y & (lim (H,X)) | Y = lim (H,Y) ) consider f being PartFunc of D,REAL such that A4: X = dom f and A5: for x being Element of D st x in X holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p by A3, Def11; A6: now__::_thesis:_ex_g_being_Element_of_K19(K20(D,REAL))_st_ (_Y_=_dom_g_&_(_for_x_being_Element_of_D_st_x_in_Y_holds_ for_p_being_Real_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((H_._n)_._x)_-_(g_._x))_<_p_)_) take g = f | Y; ::_thesis: ( Y = dom g & ( for x being Element of D st x in Y holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p ) ) thus A7: Y = dom g by A1, A4, RELAT_1:62; ::_thesis: for x being Element of D st x in Y holds for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p let x be Element of D; ::_thesis: ( x in Y implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p ) assume A8: x in Y ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p then consider k being Element of NAT such that A9: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p by A1, A5, A8; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (g . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (g . x)) < p ) assume n >= k ; ::_thesis: abs (((H . n) . x) - (g . x)) < p then abs (((H . n) . x) - (f . x)) < p by A9; hence abs (((H . n) . x) - (g . x)) < p by A7, A8, FUNCT_1:47; ::_thesis: verum end; X common_on_dom H by A3, Def11; then Y common_on_dom H by A1, A2, Th23; hence A10: H is_point_conv_on Y by A6, Def11; ::_thesis: (lim (H,X)) | Y = lim (H,Y) A11: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H,X))_|_Y)_holds_ ((lim_(H,X))_|_Y)_._x_=_(lim_(H,Y))_._x let x be Element of D; ::_thesis: ( x in dom ((lim (H,X)) | Y) implies ((lim (H,X)) | Y) . x = (lim (H,Y)) . x ) assume A12: x in dom ((lim (H,X)) | Y) ; ::_thesis: ((lim (H,X)) | Y) . x = (lim (H,Y)) . x then A13: x in (dom (lim (H,X))) /\ Y by RELAT_1:61; then A14: x in dom (lim (H,X)) by XBOOLE_0:def_4; x in Y by A13, XBOOLE_0:def_4; then A15: x in dom (lim (H,Y)) by A10, Def13; thus ((lim (H,X)) | Y) . x = (lim (H,X)) . x by A12, FUNCT_1:47 .= lim (H # x) by A3, A14, Def13 .= (lim (H,Y)) . x by A10, A15, Def13 ; ::_thesis: verum end; dom (lim (H,X)) = X by A3, Def13; then (dom (lim (H,X))) /\ Y = Y by A1, XBOOLE_1:28; then dom ((lim (H,X)) | Y) = Y by RELAT_1:61; then dom ((lim (H,X)) | Y) = dom (lim (H,Y)) by A10, Def13; hence (lim (H,X)) | Y = lim (H,Y) by A11, PARTFUN1:5; ::_thesis: verum end; theorem :: SEQFUNC:25 for D being non empty set for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & H is_unif_conv_on X holds H is_unif_conv_on Y proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for Y, X being set st Y c= X & Y <> {} & H is_unif_conv_on X holds H is_unif_conv_on Y let H be Functional_Sequence of D,REAL; ::_thesis: for Y, X being set st Y c= X & Y <> {} & H is_unif_conv_on X holds H is_unif_conv_on Y let Y, X be set ; ::_thesis: ( Y c= X & Y <> {} & H is_unif_conv_on X implies H is_unif_conv_on Y ) assume that A1: Y c= X and A2: Y <> {} and A3: H is_unif_conv_on X ; ::_thesis: H is_unif_conv_on Y consider f being PartFunc of D,REAL such that A4: dom f = X and A5: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by A3, Def12; A6: now__::_thesis:_ex_g_being_Element_of_K19(K20(D,REAL))_st_ (_dom_g_=_Y_&_(_for_p_being_Real_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_ for_x_being_Element_of_D_st_n_>=_k_&_x_in_Y_holds_ abs_(((H_._n)_._x)_-_(g_._x))_<_p_)_) take g = f | Y; ::_thesis: ( dom g = Y & ( for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p ) ) thus A7: dom g = (dom f) /\ Y by RELAT_1:61 .= Y by A1, A4, XBOOLE_1:28 ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p then consider k being Element of NAT such that A8: for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by A5; take k = k; ::_thesis: for n being Element of NAT for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p let n be Element of NAT ; ::_thesis: for x being Element of D st n >= k & x in Y holds abs (((H . n) . x) - (g . x)) < p let x be Element of D; ::_thesis: ( n >= k & x in Y implies abs (((H . n) . x) - (g . x)) < p ) assume that A9: n >= k and A10: x in Y ; ::_thesis: abs (((H . n) . x) - (g . x)) < p abs (((H . n) . x) - (f . x)) < p by A1, A8, A9, A10; hence abs (((H . n) . x) - (g . x)) < p by A7, A10, FUNCT_1:47; ::_thesis: verum end; X common_on_dom H by A3, Def12; then Y common_on_dom H by A1, A2, Th23; hence H is_unif_conv_on Y by A6, Def12; ::_thesis: verum end; theorem Th26: :: SEQFUNC:26 for D being non empty set for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds for x being Element of D st x in X holds {x} common_on_dom H proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds for x being Element of D st x in X holds {x} common_on_dom H let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds for x being Element of D st x in X holds {x} common_on_dom H let X be set ; ::_thesis: ( X common_on_dom H implies for x being Element of D st x in X holds {x} common_on_dom H ) assume A1: X common_on_dom H ; ::_thesis: for x being Element of D st x in X holds {x} common_on_dom H let x be Element of D; ::_thesis: ( x in X implies {x} common_on_dom H ) assume A2: x in X ; ::_thesis: {x} common_on_dom H thus {x} <> {} ; :: according to SEQFUNC:def_9 ::_thesis: for n being Element of NAT holds {x} c= dom (H . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_{x}_c=_dom_(H_._n) let n be Element of NAT ; ::_thesis: {x} c= dom (H . n) X c= dom (H . n) by A1, Def9; hence {x} c= dom (H . n) by A2, ZFMISC_1:31; ::_thesis: verum end; hence for n being Element of NAT holds {x} c= dom (H . n) ; ::_thesis: verum end; theorem :: SEQFUNC:27 for D being non empty set for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds {x} common_on_dom H proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds {x} common_on_dom H let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds {x} common_on_dom H let X be set ; ::_thesis: ( H is_point_conv_on X implies for x being Element of D st x in X holds {x} common_on_dom H ) assume H is_point_conv_on X ; ::_thesis: for x being Element of D st x in X holds {x} common_on_dom H then X common_on_dom H by Def11; hence for x being Element of D st x in X holds {x} common_on_dom H by Th26; ::_thesis: verum end; theorem Th28: :: SEQFUNC:28 for D being non empty set for H1, H2 being Functional_Sequence of D,REAL for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) proof let D be non empty set ; ::_thesis: for H1, H2 being Functional_Sequence of D,REAL for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: for x being Element of D st {x} common_on_dom H1 & {x} common_on_dom H2 holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let x be Element of D; ::_thesis: ( {x} common_on_dom H1 & {x} common_on_dom H2 implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) ) assume that A1: {x} common_on_dom H1 and A2: {x} common_on_dom H2 ; ::_thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_+_(H2_#_x))_._n_=_((H1_+_H2)_#_x)_._n let n be Element of NAT ; ::_thesis: ((H1 # x) + (H2 # x)) . n = ((H1 + H2) # x) . n A3: {x} c= dom (H2 . n) by A2, Def9; ( x in {x} & {x} c= dom (H1 . n) ) by A1, Def9, TARSKI:def_1; then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A3, XBOOLE_0:def_4; then A4: x in dom ((H1 . n) + (H2 . n)) by VALUED_1:def_1; thus ((H1 # x) + (H2 # x)) . n = ((H1 # x) . n) + ((H2 # x) . n) by SEQ_1:7 .= ((H1 . n) . x) + ((H2 # x) . n) by Def10 .= ((H1 . n) . x) + ((H2 . n) . x) by Def10 .= ((H1 . n) + (H2 . n)) . x by A4, VALUED_1:def_1 .= ((H1 + H2) . n) . x by Def5 .= ((H1 + H2) # x) . n by Def10 ; ::_thesis: verum end; hence (H1 # x) + (H2 # x) = (H1 + H2) # x by FUNCT_2:63; ::_thesis: ( (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_-_(H2_#_x))_._n_=_((H1_-_H2)_#_x)_._n let n be Element of NAT ; ::_thesis: ((H1 # x) - (H2 # x)) . n = ((H1 - H2) # x) . n A5: {x} c= dom (H2 . n) by A2, Def9; ( x in {x} & {x} c= dom (H1 . n) ) by A1, Def9, TARSKI:def_1; then x in (dom (H1 . n)) /\ (dom (H2 . n)) by A5, XBOOLE_0:def_4; then A6: x in dom ((H1 . n) - (H2 . n)) by VALUED_1:12; thus ((H1 # x) - (H2 # x)) . n = ((H1 # x) . n) - ((H2 # x) . n) by RFUNCT_2:1 .= ((H1 . n) . x) - ((H2 # x) . n) by Def10 .= ((H1 . n) . x) - ((H2 . n) . x) by Def10 .= ((H1 . n) - (H2 . n)) . x by A6, VALUED_1:13 .= ((H1 - H2) . n) . x by Th3 .= ((H1 - H2) # x) . n by Def10 ; ::_thesis: verum end; hence (H1 # x) - (H2 # x) = (H1 - H2) # x by FUNCT_2:63; ::_thesis: (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x now__::_thesis:_for_n_being_Element_of_NAT_holds_((H1_#_x)_(#)_(H2_#_x))_._n_=_((H1_(#)_H2)_#_x)_._n let n be Element of NAT ; ::_thesis: ((H1 # x) (#) (H2 # x)) . n = ((H1 (#) H2) # x) . n thus ((H1 # x) (#) (H2 # x)) . n = ((H1 # x) . n) * ((H2 # x) . n) by SEQ_1:8 .= ((H1 . n) . x) * ((H2 # x) . n) by Def10 .= ((H1 . n) . x) * ((H2 . n) . x) by Def10 .= ((H1 . n) (#) (H2 . n)) . x by VALUED_1:5 .= ((H1 (#) H2) . n) . x by Def7 .= ((H1 (#) H2) # x) . n by Def10 ; ::_thesis: verum end; hence (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x by FUNCT_2:63; ::_thesis: verum end; theorem Th29: :: SEQFUNC:29 for D being non empty set for H being Functional_Sequence of D,REAL for x being Element of D holds ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for x being Element of D holds ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) let H be Functional_Sequence of D,REAL; ::_thesis: for x being Element of D holds ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) let x be Element of D; ::_thesis: ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((abs_H)_#_x)_._n_=_(abs_(H_#_x))_._n let n be Element of NAT ; ::_thesis: ((abs H) # x) . n = (abs (H # x)) . n thus ((abs H) # x) . n = ((abs H) . n) . x by Def10 .= (abs (H . n)) . x by Def4 .= abs ((H . n) . x) by VALUED_1:18 .= abs ((H # x) . n) by Def10 .= (abs (H # x)) . n by SEQ_1:12 ; ::_thesis: verum end; hence (abs H) # x = abs (H # x) by FUNCT_2:63; ::_thesis: (- H) # x = - (H # x) now__::_thesis:_for_n_being_Element_of_NAT_holds_((-_H)_#_x)_._n_=_(-_(H_#_x))_._n let n be Element of NAT ; ::_thesis: ((- H) # x) . n = (- (H # x)) . n thus ((- H) # x) . n = ((- H) . n) . x by Def10 .= (- (H . n)) . x by Def3 .= - ((H . n) . x) by VALUED_1:8 .= - ((H # x) . n) by Def10 .= (- (H # x)) . n by SEQ_1:10 ; ::_thesis: verum end; hence (- H) # x = - (H # x) by FUNCT_2:63; ::_thesis: verum end; theorem Th30: :: SEQFUNC:30 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL for x being Element of D st {x} common_on_dom H holds (r (#) H) # x = r (#) (H # x) proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL for x being Element of D st {x} common_on_dom H holds (r (#) H) # x = r (#) (H # x) let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL for x being Element of D st {x} common_on_dom H holds (r (#) H) # x = r (#) (H # x) let H be Functional_Sequence of D,REAL; ::_thesis: for x being Element of D st {x} common_on_dom H holds (r (#) H) # x = r (#) (H # x) let x be Element of D; ::_thesis: ( {x} common_on_dom H implies (r (#) H) # x = r (#) (H # x) ) assume A1: {x} common_on_dom H ; ::_thesis: (r (#) H) # x = r (#) (H # x) now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_H)_#_x)_._n_=_(r_(#)_(H_#_x))_._n let n be Element of NAT ; ::_thesis: ((r (#) H) # x) . n = (r (#) (H # x)) . n ( x in {x} & {x} c= dom (H . n) ) by A1, Def9, TARSKI:def_1; then x in dom (H . n) ; then A2: x in dom (r (#) (H . n)) by VALUED_1:def_5; thus ((r (#) H) # x) . n = ((r (#) H) . n) . x by Def10 .= (r (#) (H . n)) . x by Def1 .= r * ((H . n) . x) by A2, VALUED_1:def_5 .= r * ((H # x) . n) by Def10 .= (r (#) (H # x)) . n by SEQ_1:9 ; ::_thesis: verum end; hence (r (#) H) # x = r (#) (H # x) by FUNCT_2:63; ::_thesis: verum end; theorem Th31: :: SEQFUNC:31 for D being non empty set for H1, H2 being Functional_Sequence of D,REAL for X being set st X common_on_dom H1 & X common_on_dom H2 holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) proof let D be non empty set ; ::_thesis: for H1, H2 being Functional_Sequence of D,REAL for X being set st X common_on_dom H1 & X common_on_dom H2 holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H1 & X common_on_dom H2 holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let X be set ; ::_thesis: ( X common_on_dom H1 & X common_on_dom H2 implies for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) ) assume A1: ( X common_on_dom H1 & X common_on_dom H2 ) ; ::_thesis: for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let x be Element of D; ::_thesis: ( x in X implies ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) ) assume x in X ; ::_thesis: ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) then ( {x} common_on_dom H1 & {x} common_on_dom H2 ) by A1, Th26; hence ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) by Th28; ::_thesis: verum end; theorem Th32: :: SEQFUNC:32 for D being non empty set for H being Functional_Sequence of D,REAL for x being Element of D holds ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) by Th29; theorem Th33: :: SEQFUNC:33 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let X be set ; ::_thesis: ( X common_on_dom H implies for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) ) assume A1: X common_on_dom H ; ::_thesis: for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let x be Element of D; ::_thesis: ( x in X implies (r (#) H) # x = r (#) (H # x) ) assume x in X ; ::_thesis: (r (#) H) # x = r (#) (H # x) then {x} common_on_dom H by A1, Th26; hence (r (#) H) # x = r (#) (H # x) by Th30; ::_thesis: verum end; theorem Th34: :: SEQFUNC:34 for D being non empty set for H1, H2 being Functional_Sequence of D,REAL for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) proof let D be non empty set ; ::_thesis: for H1, H2 being Functional_Sequence of D,REAL for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) let X be set ; ::_thesis: ( H1 is_point_conv_on X & H2 is_point_conv_on X implies for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) ) assume ( H1 is_point_conv_on X & H2 is_point_conv_on X ) ; ::_thesis: for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) then ( X common_on_dom H1 & X common_on_dom H2 ) by Def11; hence for x being Element of D st x in X holds ( (H1 # x) + (H2 # x) = (H1 + H2) # x & (H1 # x) - (H2 # x) = (H1 - H2) # x & (H1 # x) (#) (H2 # x) = (H1 (#) H2) # x ) by Th31; ::_thesis: verum end; theorem :: SEQFUNC:35 for D being non empty set for H being Functional_Sequence of D,REAL for x being Element of D holds ( (abs H) # x = abs (H # x) & (- H) # x = - (H # x) ) by Th32; theorem :: SEQFUNC:36 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_point_conv_on X holds for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) let X be set ; ::_thesis: ( H is_point_conv_on X implies for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) ) assume H is_point_conv_on X ; ::_thesis: for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) then X common_on_dom H by Def11; hence for x being Element of D st x in X holds (r (#) H) # x = r (#) (H # x) by Th33; ::_thesis: verum end; theorem Th37: :: SEQFUNC:37 for D being non empty set for H1, H2 being Functional_Sequence of D,REAL for X being set st X common_on_dom H1 & X common_on_dom H2 holds ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) proof let D be non empty set ; ::_thesis: for H1, H2 being Functional_Sequence of D,REAL for X being set st X common_on_dom H1 & X common_on_dom H2 holds ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H1 & X common_on_dom H2 holds ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) let X be set ; ::_thesis: ( X common_on_dom H1 & X common_on_dom H2 implies ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) ) assume that A1: X common_on_dom H1 and A2: X common_on_dom H2 ; ::_thesis: ( X common_on_dom H1 + H2 & X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) A3: X <> {} by A1, Def9; now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_+_H2)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((H1 + H2) . n) ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9; then X c= (dom (H1 . n)) /\ (dom (H2 . n)) by XBOOLE_1:19; then X c= dom ((H1 . n) + (H2 . n)) by VALUED_1:def_1; hence X c= dom ((H1 + H2) . n) by Def5; ::_thesis: verum end; hence X common_on_dom H1 + H2 by A3, Def9; ::_thesis: ( X common_on_dom H1 - H2 & X common_on_dom H1 (#) H2 ) now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_-_H2)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((H1 - H2) . n) ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9; then X c= (dom (H1 . n)) /\ (dom (H2 . n)) by XBOOLE_1:19; then X c= dom ((H1 . n) - (H2 . n)) by VALUED_1:12; hence X c= dom ((H1 - H2) . n) by Th3; ::_thesis: verum end; hence X common_on_dom H1 - H2 by A3, Def9; ::_thesis: X common_on_dom H1 (#) H2 now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((H1_(#)_H2)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((H1 (#) H2) . n) ( X c= dom (H1 . n) & X c= dom (H2 . n) ) by A1, A2, Def9; then X c= (dom (H1 . n)) /\ (dom (H2 . n)) by XBOOLE_1:19; then X c= dom ((H1 . n) (#) (H2 . n)) by VALUED_1:def_4; hence X c= dom ((H1 (#) H2) . n) by Def7; ::_thesis: verum end; hence X common_on_dom H1 (#) H2 by A3, Def9; ::_thesis: verum end; theorem Th38: :: SEQFUNC:38 for D being non empty set for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds ( X common_on_dom abs H & X common_on_dom - H ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds ( X common_on_dom abs H & X common_on_dom - H ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds ( X common_on_dom abs H & X common_on_dom - H ) let X be set ; ::_thesis: ( X common_on_dom H implies ( X common_on_dom abs H & X common_on_dom - H ) ) assume A1: X common_on_dom H ; ::_thesis: ( X common_on_dom abs H & X common_on_dom - H ) then A2: X <> {} by Def9; now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((abs_H)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((abs H) . n) dom (H . n) = dom (abs (H . n)) by VALUED_1:def_11 .= dom ((abs H) . n) by Def4 ; hence X c= dom ((abs H) . n) by A1, Def9; ::_thesis: verum end; hence X common_on_dom abs H by A2, Def9; ::_thesis: X common_on_dom - H now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((-_H)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((- H) . n) dom (H . n) = dom (- (H . n)) by VALUED_1:8 .= dom ((- H) . n) by Def3 ; hence X c= dom ((- H) . n) by A1, Def9; ::_thesis: verum end; hence X common_on_dom - H by A2, Def9; ::_thesis: verum end; theorem Th39: :: SEQFUNC:39 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds X common_on_dom r (#) H proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds X common_on_dom r (#) H let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st X common_on_dom H holds X common_on_dom r (#) H let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st X common_on_dom H holds X common_on_dom r (#) H let X be set ; ::_thesis: ( X common_on_dom H implies X common_on_dom r (#) H ) assume A1: X common_on_dom H ; ::_thesis: X common_on_dom r (#) H A2: now__::_thesis:_for_n_being_Element_of_NAT_holds_X_c=_dom_((r_(#)_H)_._n) let n be Element of NAT ; ::_thesis: X c= dom ((r (#) H) . n) dom (H . n) = dom (r (#) (H . n)) by VALUED_1:def_5 .= dom ((r (#) H) . n) by Def1 ; hence X c= dom ((r (#) H) . n) by A1, Def9; ::_thesis: verum end; X <> {} by A1, Def9; hence X common_on_dom r (#) H by A2, Def9; ::_thesis: verum end; theorem :: SEQFUNC:40 for D being non empty set for H1, H2 being Functional_Sequence of D,REAL for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) proof let D be non empty set ; ::_thesis: for H1, H2 being Functional_Sequence of D,REAL for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) let H1, H2 be Functional_Sequence of D,REAL; ::_thesis: for X being set st H1 is_point_conv_on X & H2 is_point_conv_on X holds ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) let X be set ; ::_thesis: ( H1 is_point_conv_on X & H2 is_point_conv_on X implies ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) ) assume that A1: H1 is_point_conv_on X and A2: H2 is_point_conv_on X ; ::_thesis: ( H1 + H2 is_point_conv_on X & lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (H1_+_H2)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (H1 + H2) # x is convergent ) assume A4: x in X ; ::_thesis: (H1 + H2) # x is convergent then ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; then (H1 # x) + (H2 # x) is convergent by SEQ_2:5; hence (H1 + H2) # x is convergent by A1, A2, A4, Th34; ::_thesis: verum end; A5: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (H1_-_H2)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (H1 - H2) # x is convergent ) assume A6: x in X ; ::_thesis: (H1 - H2) # x is convergent then ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; then (H1 # x) - (H2 # x) is convergent by SEQ_2:11; hence (H1 - H2) # x is convergent by A1, A2, A6, Th34; ::_thesis: verum end; A7: ( X common_on_dom H1 & X common_on_dom H2 ) by A1, A2, Th20; then X common_on_dom H1 + H2 by Th37; hence A8: H1 + H2 is_point_conv_on X by A3, Th20; ::_thesis: ( lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) & H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) A9: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_+_(lim_(H2,X)))_holds_ ((lim_(H1,X))_+_(lim_(H2,X)))_._x_=_lim_((H1_+_H2)_#_x) let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) + (lim (H2,X))) implies ((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x) ) assume A10: x in dom ((lim (H1,X)) + (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) + (lim (H2,X))) . x = lim ((H1 + H2) # x) then A11: x in (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:def_1; then A12: x in dom (lim (H2,X)) by XBOOLE_0:def_4; A13: x in dom (lim (H1,X)) by A11, XBOOLE_0:def_4; then A14: x in X by A1, Def13; then A15: ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; thus ((lim (H1,X)) + (lim (H2,X))) . x = ((lim (H1,X)) . x) + ((lim (H2,X)) . x) by A10, VALUED_1:def_1 .= (lim (H1 # x)) + ((lim (H2,X)) . x) by A1, A13, Def13 .= (lim (H1 # x)) + (lim (H2 # x)) by A2, A12, Def13 .= lim ((H1 # x) + (H2 # x)) by A15, SEQ_2:6 .= lim ((H1 + H2) # x) by A1, A2, A14, Th34 ; ::_thesis: verum end; A16: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (H1_(#)_H2)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (H1 (#) H2) # x is convergent ) assume A17: x in X ; ::_thesis: (H1 (#) H2) # x is convergent then ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; then (H1 # x) (#) (H2 # x) is convergent by SEQ_2:14; hence (H1 (#) H2) # x is convergent by A1, A2, A17, Th34; ::_thesis: verum end; A18: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_(#)_(lim_(H2,X)))_holds_ ((lim_(H1,X))_(#)_(lim_(H2,X)))_._x_=_lim_((H1_(#)_H2)_#_x) let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) (#) (lim (H2,X))) implies ((lim (H1,X)) (#) (lim (H2,X))) . x = lim ((H1 (#) H2) # x) ) assume x in dom ((lim (H1,X)) (#) (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) (#) (lim (H2,X))) . x = lim ((H1 (#) H2) # x) then A19: x in (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:def_4; then A20: x in dom (lim (H2,X)) by XBOOLE_0:def_4; A21: x in dom (lim (H1,X)) by A19, XBOOLE_0:def_4; then A22: x in X by A1, Def13; then A23: ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; thus ((lim (H1,X)) (#) (lim (H2,X))) . x = ((lim (H1,X)) . x) * ((lim (H2,X)) . x) by VALUED_1:5 .= (lim (H1 # x)) * ((lim (H2,X)) . x) by A1, A21, Def13 .= (lim (H1 # x)) * (lim (H2 # x)) by A2, A20, Def13 .= lim ((H1 # x) (#) (H2 # x)) by A23, SEQ_2:15 .= lim ((H1 (#) H2) # x) by A1, A2, A22, Th34 ; ::_thesis: verum end; A24: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_((lim_(H1,X))_-_(lim_(H2,X)))_holds_ ((lim_(H1,X))_-_(lim_(H2,X)))_._x_=_lim_((H1_-_H2)_#_x) let x be Element of D; ::_thesis: ( x in dom ((lim (H1,X)) - (lim (H2,X))) implies ((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x) ) assume A25: x in dom ((lim (H1,X)) - (lim (H2,X))) ; ::_thesis: ((lim (H1,X)) - (lim (H2,X))) . x = lim ((H1 - H2) # x) then A26: x in (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:12; then A27: x in dom (lim (H2,X)) by XBOOLE_0:def_4; A28: x in dom (lim (H1,X)) by A26, XBOOLE_0:def_4; then A29: x in X by A1, Def13; then A30: ( H1 # x is convergent & H2 # x is convergent ) by A1, A2, Th20; thus ((lim (H1,X)) - (lim (H2,X))) . x = ((lim (H1,X)) . x) - ((lim (H2,X)) . x) by A25, VALUED_1:13 .= (lim (H1 # x)) - ((lim (H2,X)) . x) by A1, A28, Def13 .= (lim (H1 # x)) - (lim (H2 # x)) by A2, A27, Def13 .= lim ((H1 # x) - (H2 # x)) by A30, SEQ_2:12 .= lim ((H1 - H2) # x) by A1, A2, A29, Th34 ; ::_thesis: verum end; dom ((lim (H1,X)) + (lim (H2,X))) = (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:def_1 .= X /\ (dom (lim (H2,X))) by A1, Def13 .= X /\ X by A2, Def13 .= X ; hence lim ((H1 + H2),X) = (lim (H1,X)) + (lim (H2,X)) by A8, A9, Def13; ::_thesis: ( H1 - H2 is_point_conv_on X & lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) X common_on_dom H1 - H2 by A7, Th37; hence A31: H1 - H2 is_point_conv_on X by A5, Th20; ::_thesis: ( lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) & H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) dom ((lim (H1,X)) - (lim (H2,X))) = (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:12 .= X /\ (dom (lim (H2,X))) by A1, Def13 .= X /\ X by A2, Def13 .= X ; hence lim ((H1 - H2),X) = (lim (H1,X)) - (lim (H2,X)) by A31, A24, Def13; ::_thesis: ( H1 (#) H2 is_point_conv_on X & lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) ) X common_on_dom H1 (#) H2 by A7, Th37; hence A32: H1 (#) H2 is_point_conv_on X by A16, Th20; ::_thesis: lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) dom ((lim (H1,X)) (#) (lim (H2,X))) = (dom (lim (H1,X))) /\ (dom (lim (H2,X))) by VALUED_1:def_4 .= X /\ (dom (lim (H2,X))) by A1, Def13 .= X /\ X by A2, Def13 .= X ; hence lim ((H1 (#) H2),X) = (lim (H1,X)) (#) (lim (H2,X)) by A32, A18, Def13; ::_thesis: verum end; theorem :: SEQFUNC:41 for D being non empty set for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds ( abs H is_point_conv_on X & lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds ( abs H is_point_conv_on X & lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_point_conv_on X holds ( abs H is_point_conv_on X & lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) let X be set ; ::_thesis: ( H is_point_conv_on X implies ( abs H is_point_conv_on X & lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) ) assume A1: H is_point_conv_on X ; ::_thesis: ( abs H is_point_conv_on X & lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) A2: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (abs_H)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (abs H) # x is convergent ) assume x in X ; ::_thesis: (abs H) # x is convergent then H # x is convergent by A1, Th20; then abs (H # x) is convergent by SEQ_4:13; hence (abs H) # x is convergent by Th32; ::_thesis: verum end; A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(-_(lim_(H,X)))_holds_ (-_(lim_(H,X)))_._x_=_lim_((-_H)_#_x) let x be Element of D; ::_thesis: ( x in dom (- (lim (H,X))) implies (- (lim (H,X))) . x = lim ((- H) # x) ) assume x in dom (- (lim (H,X))) ; ::_thesis: (- (lim (H,X))) . x = lim ((- H) # x) then A4: x in dom (lim (H,X)) by VALUED_1:8; then x in X by A1, Def13; then A5: H # x is convergent by A1, Th20; thus (- (lim (H,X))) . x = - ((lim (H,X)) . x) by VALUED_1:8 .= - (lim (H # x)) by A1, A4, Def13 .= lim (- (H # x)) by A5, SEQ_2:10 .= lim ((- H) # x) by Th32 ; ::_thesis: verum end; A6: X common_on_dom H by A1, Th20; then X common_on_dom abs H by Th38; hence A7: abs H is_point_conv_on X by A2, Th20; ::_thesis: ( lim ((abs H),X) = abs (lim (H,X)) & - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) A8: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(abs_(lim_(H,X)))_holds_ (abs_(lim_(H,X)))_._x_=_lim_((abs_H)_#_x) let x be Element of D; ::_thesis: ( x in dom (abs (lim (H,X))) implies (abs (lim (H,X))) . x = lim ((abs H) # x) ) assume x in dom (abs (lim (H,X))) ; ::_thesis: (abs (lim (H,X))) . x = lim ((abs H) # x) then A9: x in dom (lim (H,X)) by VALUED_1:def_11; then x in X by A1, Def13; then A10: H # x is convergent by A1, Th20; thus (abs (lim (H,X))) . x = abs ((lim (H,X)) . x) by VALUED_1:18 .= abs (lim (H # x)) by A1, A9, Def13 .= lim (abs (H # x)) by A10, SEQ_4:14 .= lim ((abs H) # x) by Th32 ; ::_thesis: verum end; A11: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (-_H)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (- H) # x is convergent ) assume x in X ; ::_thesis: (- H) # x is convergent then H # x is convergent by A1, Th20; then - (H # x) is convergent by SEQ_2:9; hence (- H) # x is convergent by Th32; ::_thesis: verum end; dom (abs (lim (H,X))) = dom (lim (H,X)) by VALUED_1:def_11 .= X by A1, Def13 ; hence lim ((abs H),X) = abs (lim (H,X)) by A7, A8, Def13; ::_thesis: ( - H is_point_conv_on X & lim ((- H),X) = - (lim (H,X)) ) X common_on_dom - H by A6, Th38; hence A12: - H is_point_conv_on X by A11, Th20; ::_thesis: lim ((- H),X) = - (lim (H,X)) dom (- (lim (H,X))) = dom (lim (H,X)) by VALUED_1:8 .= X by A1, Def13 ; hence lim ((- H),X) = - (lim (H,X)) by A12, A3, Def13; ::_thesis: verum end; theorem :: SEQFUNC:42 for D being non empty set for r being Real for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) proof let D be non empty set ; ::_thesis: for r being Real for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) let r be Real; ::_thesis: for H being Functional_Sequence of D,REAL for X being set st H is_point_conv_on X holds ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set st H is_point_conv_on X holds ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) let X be set ; ::_thesis: ( H is_point_conv_on X implies ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) ) assume A1: H is_point_conv_on X ; ::_thesis: ( r (#) H is_point_conv_on X & lim ((r (#) H),X) = r (#) (lim (H,X)) ) then A2: X common_on_dom H by Th20; A3: now__::_thesis:_for_x_being_Element_of_D_st_x_in_dom_(r_(#)_(lim_(H,X)))_holds_ (r_(#)_(lim_(H,X)))_._x_=_lim_((r_(#)_H)_#_x) let x be Element of D; ::_thesis: ( x in dom (r (#) (lim (H,X))) implies (r (#) (lim (H,X))) . x = lim ((r (#) H) # x) ) assume A4: x in dom (r (#) (lim (H,X))) ; ::_thesis: (r (#) (lim (H,X))) . x = lim ((r (#) H) # x) then A5: x in dom (lim (H,X)) by VALUED_1:def_5; then A6: x in X by A1, Def13; then A7: H # x is convergent by A1, Th20; thus (r (#) (lim (H,X))) . x = r * ((lim (H,X)) . x) by A4, VALUED_1:def_5 .= r * (lim (H # x)) by A1, A5, Def13 .= lim (r (#) (H # x)) by A7, SEQ_2:8 .= lim ((r (#) H) # x) by A2, A6, Th33 ; ::_thesis: verum end; A8: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ (r_(#)_H)_#_x_is_convergent let x be Element of D; ::_thesis: ( x in X implies (r (#) H) # x is convergent ) assume A9: x in X ; ::_thesis: (r (#) H) # x is convergent then H # x is convergent by A1, Th20; then r (#) (H # x) is convergent by SEQ_2:7; hence (r (#) H) # x is convergent by A2, A9, Th33; ::_thesis: verum end; X common_on_dom r (#) H by A2, Th39; hence A10: r (#) H is_point_conv_on X by A8, Th20; ::_thesis: lim ((r (#) H),X) = r (#) (lim (H,X)) dom (r (#) (lim (H,X))) = dom (lim (H,X)) by VALUED_1:def_5 .= X by A1, Def13 ; hence lim ((r (#) H),X) = r (#) (lim (H,X)) by A10, A3, Def13; ::_thesis: verum end; theorem Th43: :: SEQFUNC:43 for D being non empty set for H being Functional_Sequence of D,REAL for X being set holds ( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) proof let D be non empty set ; ::_thesis: for H being Functional_Sequence of D,REAL for X being set holds ( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) let H be Functional_Sequence of D,REAL; ::_thesis: for X being set holds ( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) let X be set ; ::_thesis: ( H is_unif_conv_on X iff ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) thus ( H is_unif_conv_on X implies ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) ) ::_thesis: ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) implies H is_unif_conv_on X ) proof assume A1: H is_unif_conv_on X ; ::_thesis: ( X common_on_dom H & H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) then consider f being PartFunc of D,REAL such that A2: X = dom f and A3: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by Def12; thus X common_on_dom H by A1, Def12; ::_thesis: ( H is_point_conv_on X & ( for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) ) A4: now__::_thesis:_for_x_being_Element_of_D_st_x_in_X_holds_ for_p_being_Real_st_p_>_0_holds_ ex_k_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_n_>=_k_holds_ abs_(((H_._n)_._x)_-_(f_._x))_<_p let x be Element of D; ::_thesis: ( x in X implies for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume A5: x in X ; ::_thesis: for p being Real st p > 0 holds ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let p be Real; ::_thesis: ( p > 0 implies ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p ) assume p > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p then consider k being Element of NAT such that A6: for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < p by A3; take k = k; ::_thesis: for n being Element of NAT st n >= k holds abs (((H . n) . x) - (f . x)) < p let n be Element of NAT ; ::_thesis: ( n >= k implies abs (((H . n) . x) - (f . x)) < p ) assume n >= k ; ::_thesis: abs (((H . n) . x) - (f . x)) < p hence abs (((H . n) . x) - (f . x)) < p by A5, A6; ::_thesis: verum end; thus H is_point_conv_on X by A1, Th22; ::_thesis: for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r then A7: f = lim (H,X) by A2, A4, Th21; let r be Real; ::_thesis: ( 0 < r implies ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) assume r > 0 ; ::_thesis: ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r then consider k being Element of NAT such that A8: for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - (f . x)) < r by A3; take k ; ::_thesis: for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r let n be Element of NAT ; ::_thesis: for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r let x be Element of D; ::_thesis: ( n >= k & x in X implies abs (((H . n) . x) - ((lim (H,X)) . x)) < r ) assume ( n >= k & x in X ) ; ::_thesis: abs (((H . n) . x) - ((lim (H,X)) . x)) < r hence abs (((H . n) . x) - ((lim (H,X)) . x)) < r by A7, A8; ::_thesis: verum end; assume that A9: X common_on_dom H and A10: H is_point_conv_on X and A11: for r being Real st 0 < r holds ex k being Element of NAT st for n being Element of NAT for x being Element of D st n >= k & x in X holds abs (((H . n) . x) - ((lim (H,X)) . x)) < r ; ::_thesis: H is_unif_conv_on X dom (lim (H,X)) = X by A10, Def13; hence H is_unif_conv_on X by A9, A11, Def12; ::_thesis: verum end; theorem :: SEQFUNC:44 for X being set for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) holds (lim (H,X)) | X is continuous proof let X be set ; ::_thesis: for H being Functional_Sequence of REAL,REAL st H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) holds (lim (H,X)) | X is continuous let H be Functional_Sequence of REAL,REAL; ::_thesis: ( H is_unif_conv_on X & ( for n being Element of NAT holds (H . n) | X is continuous ) implies (lim (H,X)) | X is continuous ) set l = lim (H,X); assume that A1: H is_unif_conv_on X and A2: for n being Element of NAT holds (H . n) | X is continuous ; ::_thesis: (lim (H,X)) | X is continuous A3: H is_point_conv_on X by A1, Th22; then A4: dom (lim (H,X)) = X by Def13; A5: X common_on_dom H by A1, Def12; for x0 being real number st x0 in dom ((lim (H,X)) | X) holds (lim (H,X)) | X is_continuous_in x0 proof let x0 be real number ; ::_thesis: ( x0 in dom ((lim (H,X)) | X) implies (lim (H,X)) | X is_continuous_in x0 ) assume x0 in dom ((lim (H,X)) | X) ; ::_thesis: (lim (H,X)) | X is_continuous_in x0 then A6: x0 in X by RELAT_1:57; reconsider x0 = x0 as Real by XREAL_0:def_1; for r being real number st 0 < r holds ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) ) proof let r be real number ; ::_thesis: ( 0 < r implies ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) ) ) assume 0 < r ; ::_thesis: ex s being real number st ( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) ) then A7: 0 < r / 3 by XREAL_1:222; reconsider r = r as Real by XREAL_0:def_1; consider k being Element of NAT such that A8: for n being Element of NAT for x1 being Real st n >= k & x1 in X holds abs (((H . n) . x1) - ((lim (H,X)) . x1)) < r / 3 by A1, A7, Th43; consider k1 being Element of NAT such that A9: for n being Element of NAT st n >= k1 holds abs (((H . n) . x0) - ((lim (H,X)) . x0)) < r / 3 by A3, A6, A7, Th21; set m = max (k,k1); set h = H . (max (k,k1)); A10: X c= dom (H . (max (k,k1))) by A5, Def9; A11: dom ((H . (max (k,k1))) | X) = (dom (H . (max (k,k1)))) /\ X by RELAT_1:61 .= X by A10, XBOOLE_1:28 ; (H . (max (k,k1))) | X is continuous by A2; then (H . (max (k,k1))) | X is_continuous_in x0 by A6, A11, FCONT_1:def_2; then consider s being real number such that A12: 0 < s and A13: for x1 being real number st x1 in dom ((H . (max (k,k1))) | X) & abs (x1 - x0) < s holds abs ((((H . (max (k,k1))) | X) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A7, FCONT_1:3; reconsider s = s as Real by XREAL_0:def_1; take s ; ::_thesis: ( 0 < s & ( for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) ) thus 0 < s by A12; ::_thesis: for x1 being real number st x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s holds abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r let x1 be real number ; ::_thesis: ( x1 in dom ((lim (H,X)) | X) & abs (x1 - x0) < s implies abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r ) assume that A14: x1 in dom ((lim (H,X)) | X) and A15: abs (x1 - x0) < s ; ::_thesis: abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r A16: dom ((lim (H,X)) | X) = (dom (lim (H,X))) /\ X by RELAT_1:61 .= X by A4 ; then abs ((((H . (max (k,k1))) | X) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A11, A13, A14, A15; then abs (((H . (max (k,k1))) . x1) - (((H . (max (k,k1))) | X) . x0)) < r / 3 by A16, A11, A14, FUNCT_1:47; then A17: abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) < r / 3 by A6, FUNCT_1:49; abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)) < r / 3 by A9, XXREAL_0:25; then ( abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) <= (abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0))) + (abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) & (abs (((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0))) + (abs (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) < (r / 3) + (r / 3) ) by A17, COMPLEX1:56, XREAL_1:8; then A18: abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0))) < (r / 3) + (r / 3) by XXREAL_0:2; abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) = abs ((((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1)) + ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) ; then A19: abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) <= (abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) + (abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) by COMPLEX1:56; abs (((H . (max (k,k1))) . x1) - ((lim (H,X)) . x1)) < r / 3 by A8, A16, A14, XXREAL_0:25; then abs (- (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) < r / 3 ; then abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1)) < r / 3 by COMPLEX1:52; then (abs (((lim (H,X)) . x1) - ((H . (max (k,k1))) . x1))) + (abs ((((H . (max (k,k1))) . x1) - ((H . (max (k,k1))) . x0)) + (((H . (max (k,k1))) . x0) - ((lim (H,X)) . x0)))) < (r / 3) + ((r / 3) + (r / 3)) by A18, XREAL_1:8; then abs (((lim (H,X)) . x1) - ((lim (H,X)) . x0)) < ((r / 3) + (r / 3)) + (r / 3) by A19, XXREAL_0:2; then abs ((((lim (H,X)) | X) . x1) - ((lim (H,X)) . x0)) < r by A14, FUNCT_1:47; hence abs ((((lim (H,X)) | X) . x1) - (((lim (H,X)) | X) . x0)) < r by A4, RELAT_1:68; ::_thesis: verum end; hence (lim (H,X)) | X is_continuous_in x0 by FCONT_1:3; ::_thesis: verum end; hence (lim (H,X)) | X is continuous by FCONT_1:def_2; ::_thesis: verum end;