seqfunc2.miz



    begin

    reserve D for non empty set,

D1,D2,x,y,Z for set,

n,k for Nat,

p,x1,r for Real,

f for Function,

Y for RealNormSpace,

G,H,H1,H2,J for Functional_Sequence of D, the carrier of Y;

    theorem :: SEQFUNC2:1

    f is Functional_Sequence of D1, D2 iff (( dom f) = NAT & for x st x in NAT holds (f . x) is PartFunc of D1, D2)

    proof

      thus f is Functional_Sequence of D1, D2 implies (( dom f) = NAT & for x st x in NAT holds (f . x) is PartFunc of D1, D2)

      proof

        assume

         A1: f is Functional_Sequence of D1, D2;

        hence ( dom f) = NAT by FUNCT_2:def 1;

        let x;

        assume x in NAT ;

        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 thesis by A2, PARTFUN1: 46;

      end;

      assume that

       A3: ( dom f) = NAT and

       A4: for x st x in NAT holds (f . x) is PartFunc of D1, D2;

      now

        let y be object;

        assume y in ( rng f);

        then

        consider x be object 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;

      end;

      then ( rng f) c= ( PFuncs (D1,D2));

      hence thesis by A3, FUNCT_2:def 1, RELSET_1: 4;

    end;

    definition

      let D;

      let Y be non empty NORMSTR;

      let H be Functional_Sequence of D, the carrier of Y;

      let r be Real;

      :: SEQFUNC2:def1

      func r (#) H -> Functional_Sequence of D, the carrier of Y means

      : Def1: for n be Nat holds (it . n) = (r (#) (H . n));

      existence

      proof

        deffunc U( Nat) = (r (#) (H . $1));

        thus ex f be Functional_Sequence of D, the carrier of Y st for n be Nat holds (f . n) = U(n) from SEQFUNC:sch 1;

      end;

      uniqueness

      proof

        let H1,H2 be Functional_Sequence of D, the carrier of Y such that

         A1: for n be Nat holds (H1 . n) = (r (#) (H . n)) and

         A2: for n be Nat holds (H2 . n) = (r (#) (H . n));

        now

          let n be Element of NAT ;

          (H1 . n) = (r (#) (H . n)) by A1;

          hence (H1 . n) = (H2 . n) by A2;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

    end

    definition

      let D;

      let Y be RealNormSpace;

      let H be Functional_Sequence of D, the carrier of Y;

      :: SEQFUNC2:def2

      func - H -> Functional_Sequence of D, the carrier of Y means

      : Def3: for n be Nat holds (it . n) = ( - (H . n));

      existence

      proof

        take (( - 1) (#) H);

        let n be Nat;

        for n be Nat holds ((( - 1) (#) H) . n) = ( - (H . n))

        proof

          let n be Nat;

          

          thus ((( - 1) (#) H) . n) = (( - 1) (#) (H . n)) by Def1

          .= ( - (H . n)) by VFUNCT_1: 23;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let H1,H2 be Functional_Sequence of D, the carrier of Y such that

         A3: for n be Nat holds (H1 . n) = ( - (H . n)) and

         A4: for n be Nat holds (H2 . n) = ( - (H . n));

        now

          let n be Element of NAT ;

          (H1 . n) = ( - (H . n)) by A3;

          hence (H1 . n) = (H2 . n) by A4;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

      involutiveness

      proof

        let G,H be Functional_Sequence of D, the carrier of Y such that

         A5: for n be Nat holds (G . n) = ( - (H . n));

        let n be Nat;

        

        thus (H . n) = ( - ( - (H . n))) by VFUNCT_1: 24

        .= ( - (G . n)) by A5;

      end;

    end

    definition

      let D;

      let Y be non empty NORMSTR;

      let H be Functional_Sequence of D, the carrier of Y;

      :: SEQFUNC2:def3

      func ||.H.|| -> Functional_Sequence of D, REAL means

      : Def4: for n be Nat holds (it . n) = ||.(H . n).||;

      existence

      proof

        deffunc U( Nat) = ||.(H . $1).||;

        thus ex f be Functional_Sequence of D, REAL st for n be Nat holds (f . n) = U(n) from SEQFUNC:sch 1;

      end;

      uniqueness

      proof

        let H1,H2 be Functional_Sequence of D, REAL such that

         A6: for n be Nat holds (H1 . n) = ||.(H . n).|| and

         A7: for n be Nat holds (H2 . n) = ||.(H . n).||;

        now

          let n be Element of NAT ;

          (H2 . n) = ||.(H . n).|| by A7;

          hence (H1 . n) = (H2 . n) by A6;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

    end

    definition

      let D;

      let Y be non empty NORMSTR;

      let G,H be Functional_Sequence of D, the carrier of Y;

      :: SEQFUNC2:def4

      func G + H -> Functional_Sequence of D, the carrier of Y means

      : Def5: for n be Nat holds (it . n) = ((G . n) + (H . n));

      existence

      proof

        deffunc U( Nat) = ((G . $1) + (H . $1));

        thus ex f be Functional_Sequence of D, the carrier of Y st for n be Nat holds (f . n) = U(n) from SEQFUNC:sch 1;

      end;

      uniqueness

      proof

        let H1,H2 be Functional_Sequence of D, the carrier of Y such that

         A1: for n be Nat holds (H1 . n) = ((G . n) + (H . n)) and

         A2: for n be Nat holds (H2 . n) = ((G . n) + (H . n));

        now

          let n be Element of NAT ;

          (H1 . n) = ((G . n) + (H . n)) by A1;

          hence (H1 . n) = (H2 . n) by A2;

        end;

        hence H1 = H2 by FUNCT_2: 63;

      end;

    end

    definition

      let D;

      let Y be RealNormSpace;

      let G,H be Functional_Sequence of D, the carrier of Y;

      :: SEQFUNC2:def5

      func G - H -> Functional_Sequence of D, the carrier of Y equals (G + ( - H));

      correctness ;

    end

    theorem :: SEQFUNC2:2

    

     Th3: H1 = (G - H) iff for n holds (H1 . n) = ((G . n) - (H . n))

    proof

      thus H1 = (G - H) implies for n holds (H1 . n) = ((G . n) - (H . n))

      proof

        assume

         A1: H1 = (G - H);

        let n;

        

        thus (H1 . n) = ((G . n) + (( - H) . n)) by A1, Def5

        .= ((G . n) + ( - (H . n))) by Def3

        .= ((G . n) - (H . n)) by VFUNCT_1: 25;

      end;

      assume

       A2: for n holds (H1 . n) = ((G . n) - (H . n));

      now

        let n be Element of NAT ;

        

        thus (H1 . n) = ((G . n) - (H . n)) by A2

        .= ((G . n) + ( - (H . n))) by VFUNCT_1: 25

        .= ((G . n) + (( - H) . n)) by Def3

        .= ((G - H) . n) by Def5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:3

    (G + H) = (H + G) & ((G + H) + J) = (G + (H + J))

    proof

      now

        let n be Element of NAT ;

        

        thus ((G + H) . n) = ((H . n) + (G . n)) by Def5

        .= ((H + G) . n) by Def5;

      end;

      hence (G + H) = (H + G) by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        

        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 VFUNCT_1: 5

        .= ((G . n) + ((H + J) . n)) by Def5

        .= ((G + (H + J)) . n) by Def5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:4

    ( - H) = (( - 1) (#) H)

    proof

      now

        let n be Element of NAT ;

        

        thus (( - H) . n) = ( - (H . n)) by Def3

        .= (( - 1) (#) (H . n)) by VFUNCT_1: 23

        .= ((( - 1) (#) H) . n) by Def1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:5

    (r (#) (G + H)) = ((r (#) G) + (r (#) H)) & (r (#) (G - H)) = ((r (#) G) - (r (#) H))

    proof

      now

        let n be Element of NAT ;

        

        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 VFUNCT_1: 13

        .= (((r (#) G) . n) + (r (#) (H . n))) by Def1

        .= (((r (#) G) . n) + ((r (#) H) . n)) by Def1

        .= (((r (#) G) + (r (#) H)) . n) by Def5;

      end;

      hence (r (#) (G + H)) = ((r (#) G) + (r (#) H)) by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        

        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 VFUNCT_1: 15

        .= (((r (#) G) . n) - (r (#) (H . n))) by Def1

        .= (((r (#) G) . n) - ((r (#) H) . n)) by Def1

        .= (((r (#) G) - (r (#) H)) . n) by Th3;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:6

    ((r * p) (#) H) = (r (#) (p (#) H))

    proof

      now

        let n be Element of NAT ;

        

        thus (((r * p) (#) H) . n) = ((r * p) (#) (H . n)) by Def1

        .= (r (#) (p (#) (H . n))) by VFUNCT_1: 14

        .= (r (#) ((p (#) H) . n)) by Def1

        .= ((r (#) (p (#) H)) . n) by Def1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:7

    (1 (#) H) = H

    proof

      now

        let n be Element of NAT ;

        

        thus ((1 (#) H) . n) = (1 (#) (H . n)) by Def1

        .= (H . n) by VFUNCT_1: 18;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:8

     ||.(r (#) H).|| = ( |.r.| (#) ||.H.||)

    proof

      now

        let n be Element of NAT ;

        

        thus ( ||.(r (#) H).|| . n) = ||.((r (#) H) . n).|| by Def4

        .= ||.(r (#) (H . n)).|| by Def1

        .= ( |.r.| (#) ||.(H . n).||) by VFUNCT_1: 22

        .= ( |.r.| (#) ( ||.H.|| . n)) by Def4

        .= (( |.r.| (#) ||.H.||) . n) by SEQFUNC:def 1;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    begin

    reserve x for Element of D,

X for set,

S1,S2 for sequence of Y,

f for PartFunc of D, the carrier of Y;

    definition

      let D;

      let Y be non empty NORMSTR;

      let H be Functional_Sequence of D, the carrier of Y;

      let x;

      :: SEQFUNC2:def6

      func H # x -> sequence of the carrier of Y means

      : Def10: for n holds (it . n) = ((H . n) /. x);

      existence

      proof

        deffunc U( Nat) = ((H . $1) /. x);

        consider f be sequence of the carrier of Y such that

         A1: for n be Element of NAT holds (f . n) = U(n) from FUNCT_2:sch 4;

        reconsider f as sequence of the carrier of Y;

        take f;

        for n holds (f . n) = ((H . n) /. x)

        proof

          let n be Nat;

          n is Element of NAT by ORDINAL1:def 12;

          hence (f . n) = ((H . n) /. x) by A1;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be sequence of the carrier of Y such that

         A2: for n holds (S1 . n) = ((H . n) /. x) and

         A3: for n holds (S2 . n) = ((H . n) /. x);

        now

          let n be Element of NAT ;

          (S1 . n) = ((H . n) /. x) by A2;

          hence (S1 . n) = (S2 . n) by A3;

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    definition

      let D, Y, H, X;

      :: SEQFUNC2:def7

      pred H is_point_conv_on X means X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p;

    end

    theorem :: SEQFUNC2:9

    

     Th18: H is_point_conv_on X iff X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x)

    proof

      thus H is_point_conv_on X implies X common_on_dom H & ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x)

      proof

        assume

         A1: H is_point_conv_on X;

        hence X common_on_dom H;

        consider f such that

         A2: X = ( dom f) and

         A3: for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p by A1;

        take f;

        thus X = ( dom f) by A2;

        let x;

        assume

         A4: x in X;

        then

         X4: (f /. x) = (f . x) by A2, PARTFUN1:def 6;

         A5:

        now

          let p be Real;

          assume

           A6: p > 0 ;

          consider k such that

           A7: for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p by A3, A4, A6;

          take k;

          let n be Nat;

          assume n >= k;

          then ||.(((H . n) /. x) - (f /. x)).|| < p by A7;

          hence ||.(((H # x) . n) - (f /. x)).|| < p by Def10;

        end;

        hence (H # x) is convergent by NORMSP_1:def 6;

        hence thesis by X4, A5, NORMSP_1:def 7;

      end;

      assume

       A8: X common_on_dom H;

      given f such that

       A9: X = ( dom f) and

       A10: for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x);

      ex f st X = ( dom f) & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p

      proof

        take f;

        thus X = ( dom f) by A9;

        let x;

        assume

         X10: x in X;

        then

         A11: (H # x) is convergent & ( lim (H # x)) = (f . x) by A10;

        

         X11: (f /. x) = (f . x) by PARTFUN1:def 6, X10, A9;

        let p;

        assume p > 0 ;

        then

        consider k be Nat such that

         A12: for n be Nat st n >= k holds ||.(((H # x) . n) - (f /. x)).|| < p by A11, NORMSP_1:def 7, X11;

        take k;

        let n;

        assume n >= k;

        then ||.(((H # x) . n) - (f /. x)).|| < p by A12;

        hence thesis by Def10;

      end;

      hence thesis by A8;

    end;

    theorem :: SEQFUNC2:10

    

     Th19: H is_point_conv_on X iff X common_on_dom H & for x st x in X holds (H # x) is convergent

    proof

      defpred X[ set] means $1 in X;

      deffunc U( Element of D) = ( In (( lim (H # $1)),the carrier of Y));

      consider f such that

       A1: for x holds x in ( dom f) iff X[x] and

       A2: for x st x in ( dom f) holds (f . x) = U(x) from SEQ_1:sch 3;

      thus H is_point_conv_on X implies X common_on_dom H & for x st x in X holds (H # x) is convergent

      proof

        assume

         A3: H is_point_conv_on X;

        hence X common_on_dom H;

        let x;

        assume

         A4: x in X;

        ex f st X = ( dom f) & for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x) by A3, Th18;

        hence thesis by A4;

      end;

      assume that

       A5: X common_on_dom H and

       A6: for x st x in X holds (H # x) is convergent;

      now

        take f;

        thus

         A7: X = ( dom f)

        proof

          thus X c= ( dom f)

          proof

            let x be object such that

             A8: x in X;

            X c= ( dom (H . 0 )) by A5;

            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 thesis;

          end;

          let x be object;

          assume x in ( dom f);

          hence thesis by A1;

        end;

        let x;

        assume

         A9: x in X;

        hence (H # x) is convergent by A6;

        ( In (( lim (H # x)),the carrier of Y)) = ( lim (H # x)) by SUBSET_1:def 8;

        hence (f . x) = ( lim (H # x)) by A2, A7, A9;

      end;

      hence thesis by A5, Th18;

    end;

    begin

    definition

      let D, Y, H, X;

      :: SEQFUNC2:def8

      pred H is_unif_conv_on X means X common_on_dom H & ex f st X = ( dom f) & for p st p > 0 holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p;

    end

    definition

      let D, Y, H, X;

      assume

       A1: H is_point_conv_on X;

      :: SEQFUNC2:def9

      func lim (H,X) -> PartFunc of D, the carrier of Y means

      : Def13: ( dom it ) = X & for x st x in ( dom it ) holds (it . x) = ( lim (H # x));

      existence

      proof

        consider f such that

         A2: X = ( dom f) and

         A3: for x st x in X holds (H # x) is convergent & ( lim (H # x)) = (f . x) by A1, Th18;

        take f;

        thus ( dom f) = X by A2;

        let x;

        assume x in ( dom f);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        deffunc U( Element of D) = ( lim (H # $1));

        thus for f1,f2 be PartFunc of D, the carrier of Y st ( dom f1) = X & (for x st x in ( dom f1) holds (f1 . x) = U(x)) & ( dom f2) = X & for x st x in ( dom f2) holds (f2 . x) = U(x) holds f1 = f2 from SEQ_1:sch 4;

      end;

    end

    theorem :: SEQFUNC2:11

    

     Th20: H is_point_conv_on X implies (f = ( lim (H,X)) iff ( dom f) = X & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p)

    proof

      assume

       A1: H is_point_conv_on X;

      thus f = ( lim (H,X)) implies ( dom f) = X & for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p

      proof

        assume

         A2: f = ( lim (H,X));

        hence

         A3: ( dom f) = X by A1, Def13;

        let x;

        assume

         A4: x in X;

        then

         A5: (H # x) is convergent by A1, Th19;

        

         X6: (f /. x) = (f . x) by PARTFUN1:def 6, A4, A3;

        let p;

        assume

         A6: p > 0 ;

        (f . x) = ( lim (H # x)) by A1, A2, A3, A4, Def13;

        then

        consider k be Nat such that

         A7: for n be Nat st n >= k holds ||.(((H # x) . n) - (f /. x)).|| < p by X6, A5, A6, NORMSP_1:def 7;

        take k;

        let n;

        assume n >= k;

        then ||.(((H # x) . n) - (f /. x)).|| < p by A7;

        hence thesis by Def10;

      end;

      assume that

       A8: ( dom f) = X and

       A9: for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p;

      now

        let x such that

         A10: x in ( dom f);

        

         X10: (f /. x) = (f . x) by A10, PARTFUN1:def 6;

         A11:

        now

          let p be Real;

          assume

           A12: p > 0 ;

          then

          consider k such that

           A13: for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p by A8, A9, A10;

          take k;

          let n be Nat;

          assume n >= k;

          then ||.(((H . n) /. x) - (f /. x)).|| < p by A13;

          hence ||.(((H # x) . n) - (f /. x)).|| < p by Def10;

        end;

        then (H # x) is convergent by NORMSP_1:def 6;

        hence (f . x) = ( lim (H # x)) by X10, A11, NORMSP_1:def 7;

      end;

      hence thesis by A1, A8, Def13;

    end;

    theorem :: SEQFUNC2:12

    

     Th21: H is_unif_conv_on X implies H is_point_conv_on X

    proof

      assume

       A1: H is_unif_conv_on X;

      now

        consider f such that

         A3: X = ( dom f) and

         A4: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p by A1;

        take f;

        thus X = ( dom f) by A3;

        let x;

        assume

         A5: x in X;

        let p;

        assume p > 0 ;

        then

        consider k such that

         A6: for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p by A4;

        take k;

        let n;

        assume n >= k;

        hence ||.(((H . n) /. x) - (f /. x)).|| < p by A5, A6;

      end;

      hence thesis by A1;

    end;

    theorem :: SEQFUNC2:13

    

     Th22: Z c= X & Z <> {} & X common_on_dom H implies Z common_on_dom H

    proof

      assume that

       A1: Z c= X and

       A2: Z <> {} and

       A3: X common_on_dom H;

      now

        let n;

        X c= ( dom (H . n)) by A3;

        hence Z c= ( dom (H . n)) by A1;

      end;

      hence thesis by A2;

    end;

    theorem :: SEQFUNC2:14

    Z c= X & Z <> {} & H is_point_conv_on X implies H is_point_conv_on Z & (( lim (H,X)) | Z) = ( lim (H,Z))

    proof

      assume that

       A1: Z c= X and

       A2: Z <> {} and

       A3: H is_point_conv_on X;

      consider f such that

       A4: X = ( dom f) and

       A5: for x st x in X holds for p st p > 0 holds ex k st for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p by A3;

      now

        take g = (f | Z);

        thus

         A7: Z = ( dom g) by A1, A4, RELAT_1: 62;

        let x;

        assume

         A8: x in Z;

        then

         X8: (f /. x) = (f . x) by A1, A4, PARTFUN1:def 6;

        (g /. x) = (g . x) by A7, A8, PARTFUN1:def 6;

        then

         X10: (g /. x) = (f /. x) by A7, A8, FUNCT_1: 47, X8;

        let p;

        assume p > 0 ;

        then

        consider k such that

         A9: for n st n >= k holds ||.(((H . n) /. x) - (f /. x)).|| < p by A1, A5, A8;

        take k;

        let n;

        assume n >= k;

        hence ||.(((H . n) /. x) - (g /. x)).|| < p by A9, X10;

      end;

      hence

       A10: H is_point_conv_on Z by A1, A2, A3, Th22;

       A11:

      now

        let x;

        assume

         A12: x in ( dom (( lim (H,X)) | Z));

        then

         A13: x in (( dom ( lim (H,X))) /\ Z) by RELAT_1: 61;

        then

         A14: x in ( dom ( lim (H,X))) by XBOOLE_0:def 4;

        x in Z by A13, XBOOLE_0:def 4;

        then

         A15: x in ( dom ( lim (H,Z))) by A10, Def13;

        

        thus ((( lim (H,X)) | Z) . x) = (( lim (H,X)) . x) by A12, FUNCT_1: 47

        .= ( lim (H # x)) by A3, A14, Def13

        .= (( lim (H,Z)) . x) by A10, A15, Def13;

      end;

      ( dom ( lim (H,X))) = X by A3, Def13;

      then (( dom ( lim (H,X))) /\ Z) = Z by A1, XBOOLE_1: 28;

      then ( dom (( lim (H,X)) | Z)) = Z by RELAT_1: 61;

      then ( dom (( lim (H,X)) | Z)) = ( dom ( lim (H,Z))) by A10, Def13;

      hence thesis by A11, PARTFUN1: 5;

    end;

    theorem :: SEQFUNC2:15

    Z c= X & Z <> {} & H is_unif_conv_on X implies H is_unif_conv_on Z

    proof

      assume that

       A1: Z c= X and

       A2: Z <> {} and

       A3: H is_unif_conv_on X;

      consider f such that

       A4: ( dom f) = X and

       A5: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p by A3;

      now

        take g = (f | Z);

        

        thus

         A7: ( dom g) = (( dom f) /\ Z) by RELAT_1: 61

        .= Z by A1, A4, XBOOLE_1: 28;

        let p;

        assume p > 0 ;

        then

        consider k such that

         A8: for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p by A5;

        take k;

        let n, x;

        assume that

         A9: n >= k and

         A10: x in Z;

        x in Z & x in ( dom f) by A7, A10, RELAT_1: 57;

        

        then (f /. x) = (f . x) by PARTFUN1:def 6

        .= (g . x) by A7, A10, FUNCT_1: 47

        .= (g /. x) by A10, A7, PARTFUN1:def 6;

        hence ||.(((H . n) /. x) - (g /. x)).|| < p by A1, A8, A9, A10;

      end;

      hence thesis by A1, A2, A3, Th22;

    end;

    theorem :: SEQFUNC2:16

    

     Th25: X common_on_dom H implies for x be set st x in X holds {x} common_on_dom H

    proof

      assume

       A1: X common_on_dom H;

      let x be set;

      assume

       A2: x in X;

      thus {x} <> {} ;

      now

        let n;

        X c= ( dom (H . n)) by A1;

        hence {x} c= ( dom (H . n)) by A2, ZFMISC_1: 31;

      end;

      hence thesis;

    end;

    theorem :: SEQFUNC2:17

    H is_point_conv_on X implies for x be set st x in X holds {x} common_on_dom H by Th25;

    theorem :: SEQFUNC2:18

    

     Th27: {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)

    proof

      assume that

       A1: {x} common_on_dom H1 and

       A2: {x} common_on_dom H2;

      now

        let n be Element of NAT ;

        

         A3: {x} c= ( dom (H2 . n)) by A2;

        x in {x} & {x} c= ( dom (H1 . n)) by A1, 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 VFUNCT_1:def 1;

        

         X4: ( dom ((H1 . n) + (H2 . n))) = ( dom ((H1 + H2) . n)) by Def5;

        

        thus (((H1 # x) + (H2 # x)) . n) = (((H1 # x) . n) + ((H2 # x) . n)) by NORMSP_1:def 2

        .= (((H1 . n) /. x) + ((H2 # x) . n)) by Def10

        .= (((H1 . n) /. x) + ((H2 . n) /. x)) by Def10

        .= (((H1 . n) + (H2 . n)) /. x) by A4, VFUNCT_1:def 1

        .= (((H1 . n) + (H2 . n)) . x) by A4, PARTFUN1:def 6

        .= (((H1 + H2) . n) . x) by Def5

        .= (((H1 + H2) . n) /. x) by A4, X4, PARTFUN1:def 6

        .= (((H1 + H2) # x) . n) by Def10;

      end;

      hence ((H1 # x) + (H2 # x)) = ((H1 + H2) # x) by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        

         A5: {x} c= ( dom (H2 . n)) by A2;

        x in {x} & {x} c= ( dom (H1 . n)) by A1, 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 VFUNCT_1:def 2;

        

         X6: ( dom ((H1 . n) - (H2 . n))) = ( dom ((H1 - H2) . n)) by Th3;

        

        thus (((H1 # x) - (H2 # x)) . n) = (((H1 # x) . n) - ((H2 # x) . n)) by NORMSP_1:def 3

        .= (((H1 . n) /. x) - ((H2 # x) . n)) by Def10

        .= (((H1 . n) /. x) - ((H2 . n) /. x)) by Def10

        .= (((H1 . n) - (H2 . n)) /. x) by A6, VFUNCT_1:def 2

        .= (((H1 . n) - (H2 . n)) . x) by A6, PARTFUN1:def 6

        .= (((H1 - H2) . n) . x) by Th3

        .= (((H1 - H2) . n) /. x) by X6, A6, PARTFUN1:def 6

        .= (((H1 - H2) # x) . n) by Def10;

      end;

      hence ((H1 # x) - (H2 # x)) = ((H1 - H2) # x) by FUNCT_2: 63;

    end;

    reserve x for Element of D;

    theorem :: SEQFUNC2:19

    

     Th28: {x} common_on_dom H implies ( ||.H.|| # x) = ||.(H # x).|| & (( - H) # x) = (( - 1) * (H # x))

    proof

      assume

       AS1: {x} common_on_dom H;

      now

        let n be Element of NAT ;

        x in {x} & {x} c= ( dom (H . n)) by AS1, TARSKI:def 1;

        then x in ( dom (H . n));

        then

         A2: x in ( dom ||.(H . n).||) by NORMSP_0:def 2;

        

        thus (( ||.H.|| # x) . n) = (( ||.H.|| . n) . x) by SEQFUNC:def 10

        .= ( ||.(H . n).|| . x) by Def4

        .= ||.((H . n) /. x).|| by A2, NORMSP_0:def 2

        .= ||.((H # x) . n).|| by Def10

        .= ( ||.(H # x).|| . n) by NORMSP_0:def 4;

      end;

      hence ( ||.H.|| # x) = ||.(H # x).|| by FUNCT_2: 63;

      now

        let n be Element of NAT ;

        x in {x} & {x} c= ( dom (H . n)) by AS1, TARSKI:def 1;

        then x in ( dom (H . n));

        then

         A2: x in ( dom ( - (H . n))) by VFUNCT_1:def 5;

        

        thus ((( - H) # x) . n) = ((( - H) . n) /. x) by Def10

        .= (( - (H . n)) /. x) by Def3

        .= ( - ((H . n) /. x)) by A2, VFUNCT_1:def 5

        .= ( - ((H # x) . n)) by Def10

        .= (( - 1) * ((H # x) . n)) by RLVECT_1: 16

        .= ((( - 1) * (H # x)) . n) by NORMSP_1:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:20

    

     Th29: {x} common_on_dom H implies ((r (#) H) # x) = (r * (H # x))

    proof

      assume

       A1: {x} common_on_dom H;

      now

        let n be Element of NAT ;

        x in {x} & {x} c= ( dom (H . n)) by A1, TARSKI:def 1;

        then x in ( dom (H . n));

        then

         A2: x in ( dom (r (#) (H . n))) by VFUNCT_1:def 4;

        

         X2: ((r (#) H) . n) = (r (#) (H . n)) by Def1;

        

        thus (((r (#) H) # x) . n) = (((r (#) H) . n) /. x) by Def10

        .= (r * ((H . n) /. x)) by X2, A2, VFUNCT_1:def 4

        .= (r * ((H # x) . n)) by Def10

        .= ((r * (H # x)) . n) by NORMSP_1:def 5;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: SEQFUNC2:21

    

     Th30: X common_on_dom H1 & X common_on_dom H2 implies for x st x in X holds ((H1 # x) + (H2 # x)) = ((H1 + H2) # x) & ((H1 # x) - (H2 # x)) = ((H1 - H2) # x)

    proof

      assume

       A1: X common_on_dom H1 & X common_on_dom H2;

      let x;

      assume x in X;

      then {x} common_on_dom H1 & {x} common_on_dom H2 by A1, Th25;

      hence thesis by Th27;

    end;

    theorem :: SEQFUNC2:22

     {x} common_on_dom H implies ( ||.H.|| # x) = ||.(H # x).|| & (( - H) # x) = (( - 1) * (H # x)) by Th28;

    theorem :: SEQFUNC2:23

    

     Th32: X common_on_dom H implies for x st x in X holds ((r (#) H) # x) = (r * (H # x))

    proof

      assume

       A1: X common_on_dom H;

      let x;

      assume x in X;

      then {x} common_on_dom H by A1, Th25;

      hence thesis by Th29;

    end;

    theorem :: SEQFUNC2:24

    H1 is_point_conv_on X & H2 is_point_conv_on X implies for x st x in X holds ((H1 # x) + (H2 # x)) = ((H1 + H2) # x) & ((H1 # x) - (H2 # x)) = ((H1 - H2) # x) by Th30;

    theorem :: SEQFUNC2:25

     {x} common_on_dom H implies ( ||.H.|| # x) = ||.(H # x).|| & (( - H) # x) = (( - 1) * (H # x)) by Th28;

    theorem :: SEQFUNC2:26

    H is_point_conv_on X implies for x st x in X holds ((r (#) H) # x) = (r * (H # x)) by Th32;

    theorem :: SEQFUNC2:27

    

     Th36: X common_on_dom H1 & X common_on_dom H2 implies X common_on_dom (H1 + H2) & X common_on_dom (H1 - H2)

    proof

      assume that

       A1: X common_on_dom H1 and

       A2: X common_on_dom H2;

      now

        let n;

        X c= ( dom (H1 . n)) & X c= ( dom (H2 . n)) by A1, A2;

        then X c= (( dom (H1 . n)) /\ ( dom (H2 . n))) by XBOOLE_1: 19;

        then X c= ( dom ((H1 . n) + (H2 . n))) by VFUNCT_1:def 1;

        hence X c= ( dom ((H1 + H2) . n)) by Def5;

      end;

      hence X common_on_dom (H1 + H2) by A1;

      now

        let n;

        X c= ( dom (H1 . n)) & X c= ( dom (H2 . n)) by A1, A2;

        then X c= (( dom (H1 . n)) /\ ( dom (H2 . n))) by XBOOLE_1: 19;

        then X c= ( dom ((H1 . n) - (H2 . n))) by VFUNCT_1:def 2;

        hence X c= ( dom ((H1 - H2) . n)) by Th3;

      end;

      hence X common_on_dom (H1 - H2) by A1;

    end;

    theorem :: SEQFUNC2:28

    

     Th37: X common_on_dom H implies X common_on_dom ||.H.|| & X common_on_dom ( - H)

    proof

      assume

       A1: X common_on_dom H;

      now

        let n;

        ( dom (H . n)) = ( dom ||.(H . n).||) by NORMSP_0:def 3

        .= ( dom ( ||.H.|| . n)) by Def4;

        hence X c= ( dom ( ||.H.|| . n)) by A1;

      end;

      hence X common_on_dom ||.H.|| by A1;

      now

        let n;

        ( dom (H . n)) = ( dom ( - (H . n))) by VFUNCT_1:def 5

        .= ( dom (( - H) . n)) by Def3;

        hence X c= ( dom (( - H) . n)) by A1;

      end;

      hence thesis by A1;

    end;

    theorem :: SEQFUNC2:29

    

     Th38: X common_on_dom H implies X common_on_dom (r (#) H)

    proof

      assume

       A1: X common_on_dom H;

      now

        let n;

        ( dom (H . n)) = ( dom (r (#) (H . n))) by VFUNCT_1:def 4

        .= ( dom ((r (#) H) . n)) by Def1;

        hence X c= ( dom ((r (#) H) . n)) by A1;

      end;

      hence thesis by A1;

    end;

    theorem :: SEQFUNC2:30

    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)))

    proof

      assume that

       A1: H1 is_point_conv_on X and

       A2: H2 is_point_conv_on X;

       A3:

      now

        let x;

        assume

         A4: x in X;

        then (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;

        then ((H1 # x) + (H2 # x)) is convergent by NORMSP_1: 19;

        hence ((H1 + H2) # x) is convergent by A1, A2, A4, Th30;

      end;

       A5:

      now

        let x;

        assume

         A6: x in X;

        then (H1 # x) is convergent & (H2 # x) is convergent by A1, A2, Th19;

        then ((H1 # x) - (H2 # x)) is convergent by NORMSP_1: 20;

        hence ((H1 - H2) # x) is convergent by A1, A2, A6, Th30;

      end;

      thus

       A8: (H1 + H2) is_point_conv_on X by A1, A2, A3, Th36, Th19;

       A9:

      now

        let x;

        assume

         A10: x in ( dom (( lim (H1,X)) + ( lim (H2,X))));

        then

         A11: x in (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VFUNCT_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, Th19;

        

         X15: (( lim (H1,X)) . x) = (( lim (H1,X)) /. x) by A13, PARTFUN1:def 6;

        

         X16: (( lim (H2,X)) . x) = (( lim (H2,X)) /. x) by A12, PARTFUN1:def 6;

        

        thus ((( lim (H1,X)) + ( lim (H2,X))) . x) = ((( lim (H1,X)) + ( lim (H2,X))) /. x) by A10, PARTFUN1:def 6

        .= ((( lim (H1,X)) /. x) + (( lim (H2,X)) /. x)) by A10, VFUNCT_1:def 1

        .= (( lim (H1 # x)) + (( lim (H2,X)) /. x)) by X15, A1, A13, Def13

        .= (( lim (H1 # x)) + ( lim (H2 # x))) by X16, A2, A12, Def13

        .= ( lim ((H1 # x) + (H2 # x))) by A15, NORMSP_1: 25

        .= ( lim ((H1 + H2) # x)) by A1, A2, A14, Th30;

      end;

       A24:

      now

        let x;

        assume

         A25: x in ( dom (( lim (H1,X)) - ( lim (H2,X))));

        then

         A26: x in (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VFUNCT_1:def 2;

        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, Th19;

        

         X15: (( lim (H1,X)) . x) = (( lim (H1,X)) /. x) by A28, PARTFUN1:def 6;

        

         X16: (( lim (H2,X)) . x) = (( lim (H2,X)) /. x) by A27, PARTFUN1:def 6;

        

        thus ((( lim (H1,X)) - ( lim (H2,X))) . x) = ((( lim (H1,X)) - ( lim (H2,X))) /. x) by A25, PARTFUN1:def 6

        .= ((( lim (H1,X)) /. x) - (( lim (H2,X)) /. x)) by A25, VFUNCT_1:def 2

        .= (( lim (H1 # x)) - (( lim (H2,X)) /. x)) by X15, A1, A28, Def13

        .= (( lim (H1 # x)) - ( lim (H2 # x))) by X16, A2, A27, Def13

        .= ( lim ((H1 # x) - (H2 # x))) by A30, NORMSP_1: 26

        .= ( lim ((H1 - H2) # x)) by A1, A2, A29, Th30;

      end;

      ( dom (( lim (H1,X)) + ( lim (H2,X)))) = (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VFUNCT_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;

      X common_on_dom (H1 - H2) by A1, A2, Th36;

      hence

       A31: (H1 - H2) is_point_conv_on X by A5, Th19;

      ( dom (( lim (H1,X)) - ( lim (H2,X)))) = (( dom ( lim (H1,X))) /\ ( dom ( lim (H2,X)))) by VFUNCT_1:def 2

      .= (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;

    end;

    theorem :: SEQFUNC2:31

    H is_point_conv_on X implies ||.H.|| is_point_conv_on X & ( lim ( ||.H.||,X)) = ||.( lim (H,X)).|| & ( - H) is_point_conv_on X & ( lim (( - H),X)) = ( - ( lim (H,X)))

    proof

      assume

       A1: H is_point_conv_on X;

       A2:

      now

        let x;

        assume

         X0: x in X;

        then

         X1: {x} common_on_dom H by A1, Th25;

         ||.(H # x).|| is convergent by X0, A1, Th19, NORMSP_1: 23;

        hence ( ||.H.|| # x) is convergent by Th28, X1;

      end;

       A3:

      now

        let x;

        assume

         A30: x in ( dom ( - ( lim (H,X))));

        then

         A4: x in ( dom ( lim (H,X))) by VFUNCT_1:def 5;

        then

         A5: x in X by A1, Def13;

        

         X5: (( lim (H,X)) /. x) = (( lim (H,X)) . x) by A4, PARTFUN1:def 6;

        

         X1: {x} common_on_dom H by A5, A1, Th25;

        

        thus (( - ( lim (H,X))) . x) = (( - ( lim (H,X))) /. x) by A30, PARTFUN1:def 6

        .= ( - (( lim (H,X)) /. x)) by A30, VFUNCT_1:def 5

        .= ( - ( lim (H # x))) by X5, A1, A4, Def13

        .= (( - 1) * ( lim (H # x))) by RLVECT_1: 16

        .= ( lim (( - 1) * (H # x))) by A1, A5, Th19, NORMSP_1: 28

        .= ( lim (( - H) # x)) by Th28, X1;

      end;

      thus

       A7: ||.H.|| is_point_conv_on X by A1, Th37, A2, SEQFUNC: 20;

       A8:

      now

        let x;

        assume

         A91: x in ( dom ||.( lim (H,X)).||);

        then

         A9: x in ( dom ( lim (H,X))) by NORMSP_0:def 3;

        then

         A90: x in X by A1, Def13;

        then

         A10: (H # x) is convergent by A1, Th19;

        

         X1: {x} common_on_dom H by A90, A1, Th25;

        

         X10: (( lim (H,X)) /. x) = (( lim (H,X)) . x) by A9, PARTFUN1:def 6;

        

        thus ( ||.( lim (H,X)).|| . x) = ||.(( lim (H,X)) /. x).|| by A91, NORMSP_0:def 3

        .= ||.( lim (H # x)).|| by A1, A9, X10, Def13

        .= ( lim ||.(H # x).||) by A10, LOPBAN_1: 20

        .= ( lim ( ||.H.|| # x)) by Th28, X1;

      end;

       A11:

      now

        let x;

        assume

         A90: x in X;

        then

         X10: (( - 1) * (H # x)) is convergent by A1, Th19, NORMSP_1: 22;

         {x} common_on_dom H by A90, A1, Th25;

        hence (( - H) # x) is convergent by Th28, X10;

      end;

      ( dom ||.( lim (H,X)).||) = ( dom ( lim (H,X))) by NORMSP_0:def 3

      .= X by A1, Def13;

      hence ( lim ( ||.H.||,X)) = ||.( lim (H,X)).|| by A7, A8, SEQFUNC:def 13;

      thus

       A12: ( - H) is_point_conv_on X by A1, Th37, A11, Th19;

      ( dom ( - ( lim (H,X)))) = ( dom ( lim (H,X))) by VFUNCT_1:def 5

      .= X by A1, Def13;

      hence thesis by A12, A3, Def13;

    end;

    theorem :: SEQFUNC2:32

    H is_point_conv_on X implies (r (#) H) is_point_conv_on X & ( lim ((r (#) H),X)) = (r (#) ( lim (H,X)))

    proof

      assume

       A1: H is_point_conv_on X;

       A3:

      now

        let x;

        assume

         A4: x in ( dom (r (#) ( lim (H,X))));

        then

         A5: x in ( dom ( lim (H,X))) by VFUNCT_1:def 4;

        then

         A6: x in X by A1, Def13;

        

         X1: (( lim (H,X)) /. x) = (( lim (H,X)) . x) by PARTFUN1:def 6, A5;

        

         X2: ((r (#) ( lim (H,X))) . x) = ((r (#) ( lim (H,X))) /. x) by PARTFUN1:def 6, A4;

        

        thus ((r (#) ( lim (H,X))) . x) = (r * (( lim (H,X)) /. x)) by X2, A4, VFUNCT_1:def 4

        .= (r * ( lim (H # x))) by A1, A5, X1, Def13

        .= ( lim (r * (H # x))) by A6, A1, Th19, NORMSP_1: 28

        .= ( lim ((r (#) H) # x)) by A1, A6, Th32;

      end;

       A8:

      now

        let x;

        assume

         A9: x in X;

        then (r * (H # x)) is convergent by A1, Th19, NORMSP_1: 22;

        hence ((r (#) H) # x) is convergent by A1, A9, Th32;

      end;

      

       A10: (r (#) H) is_point_conv_on X by A1, Th38, A8, Th19;

      ( dom (r (#) ( lim (H,X)))) = ( dom ( lim (H,X))) by VFUNCT_1:def 4

      .= X by A1, Def13;

      hence thesis by A10, A3, Def13;

    end;

    theorem :: SEQFUNC2:33

    

     Th42: H is_unif_conv_on X iff X common_on_dom H & H is_point_conv_on X & for r st 0 < r holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (( lim (H,X)) /. x)).|| < r

    proof

      thus H is_unif_conv_on X implies X common_on_dom H & H is_point_conv_on X & for r st 0 < r holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (( lim (H,X)) /. x)).|| < r

      proof

        assume

         A1: H is_unif_conv_on X;

        then

        consider f such that

         A2: X = ( dom f) and

         A3: for p st p > 0 holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p;

        thus X common_on_dom H by A1;

         A4:

        now

          let x such that

           A5: x in X;

          let p;

          assume p > 0 ;

          then

          consider k such that

           A6: for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < p by A3;

          take k;

          let n;

          assume n >= k;

          hence ||.(((H . n) /. x) - (f /. x)).|| < p by A5, A6;

        end;

        thus H is_point_conv_on X by A1, Th21;

        then

         A7: f = ( lim (H,X)) by A2, A4, Th20;

        let r;

        assume r > 0 ;

        then

        consider k such that

         A8: for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (f /. x)).|| < r by A3;

        take k;

        let n, x;

        assume n >= k & x in X;

        hence thesis by A7, A8;

      end;

      assume that

       A9: X common_on_dom H and

       A10: H is_point_conv_on X and

       A11: for r st 0 < r holds ex k st for n, x st n >= k & x in X holds ||.(((H . n) /. x) - (( lim (H,X)) /. x)).|| < r;

      ( dom ( lim (H,X))) = X by A10, Def13;

      hence thesis by A9, A11;

    end;

    reserve V,W for RealNormSpace,

H for Functional_Sequence of the carrier of V, the carrier of W;

    theorem :: SEQFUNC2:34

    H is_unif_conv_on X & (for n holds ((H . n) | X) is_continuous_on X) implies ( lim (H,X)) is_continuous_on X

    proof

      set l = ( lim (H,X));

      assume that

       A1: H is_unif_conv_on X and

       A2: for n holds ((H . n) | X) is_continuous_on X;

      

       A3: H is_point_conv_on X by A1, Th21;

      then

       A4: ( dom l) = X by Def13;

      

       A5: X common_on_dom H by A1;

      for x0 be Point of V st x0 in X holds (l | X) is_continuous_in x0

      proof

        let x0 be Point of V;

        assume

         A6: x0 in X;

        then

         A60: x0 in ( dom (l | X)) by RELAT_1: 62, A4;

        for r be Real st 0 < r holds ex s be Real st 0 < s & for x1 be Point of V st x1 in ( dom (l | X)) & ||.(x1 - x0).|| < s holds ||.(((l | X) /. x1) - ((l | X) /. x0)).|| < r

        proof

          let r be Real;

          assume

           A7: 0 < r;

          reconsider r as Element of REAL by XREAL_0:def 1;

          consider k such that

           A8: for n holds for x1 be Element of V st n >= k & x1 in X holds ||.(((H . n) /. x1) - (l /. x1)).|| < (r / 3) by A1, A7, XREAL_1: 222, Th42;

           0 < (r / 3) by A7, XREAL_1: 222;

          then

          consider k1 be Nat such that

           A9: for n st n >= k1 holds ||.(((H . n) /. x0) - (l /. x0)).|| < (r / 3) by A3, A6, Th20;

          reconsider m = ( max (k,k1)) as Nat by TARSKI: 1;

          set h = (H . m);

          

           A11: ( dom (h | X)) = (( dom h) /\ X) by RELAT_1: 61

          .= X by A5, XBOOLE_1: 28;

          (h | X) is_continuous_on X by A2;

          then h is_continuous_on X by NFCONT_1: 21;

          then (h | X) is_continuous_in x0 by A6, NFCONT_1:def 7;

          then

          consider s be Real such that

           A12: 0 < s and

           A13: for x1 be Point of V st x1 in ( dom (h | X)) & ||.(x1 - x0).|| < s holds ||.(((h | X) /. x1) - ((h | X) /. x0)).|| < (r / 3) by A7, XREAL_1: 222, NFCONT_1: 7;

          take s;

          thus 0 < s by A12;

          let x1 be Point of V;

          assume that

           A14: x1 in ( dom (l | X)) and

           A15: ||.(x1 - x0).|| < s;

          

           A16: ( dom (l | X)) = (( dom l) /\ X) by RELAT_1: 61

          .= X by A4;

          then ||.(((h | X) /. x1) - ((h | X) /. x0)).|| < (r / 3) by A11, A13, A14, A15;

          then ||.((h /. x1) - ((h | X) /. x0)).|| < (r / 3) by A16, A11, A14, PARTFUN1: 80;

          then

           A17: ||.((h /. x1) - (h /. x0)).|| < (r / 3) by A11, A6, PARTFUN1: 80;

           ||.((h /. x0) - (l /. x0)).|| < (r / 3) by A9, XXREAL_0: 25;

          then ||.(((h /. x1) - (h /. x0)) + ((h /. x0) - (l /. x0))).|| <= ( ||.((h /. x1) - (h /. x0)).|| + ||.((h /. x0) - (l /. x0)).||) & ( ||.((h /. x1) - (h /. x0)).|| + ||.((h /. x0) - (l /. x0)).||) < ((r / 3) + (r / 3)) by A17, NORMSP_1:def 1, XREAL_1: 8;

          then

           A18: ||.(((h /. x1) - (h /. x0)) + ((h /. x0) - (l /. x0))).|| < ((r / 3) + (r / 3)) by XXREAL_0: 2;

           ||.((l /. x1) - (l /. x0)).|| = ||.((((l /. x1) - (h /. x1)) + (h /. x1)) - (l /. x0)).|| by RLVECT_4: 1

          .= ||.(((l /. x1) - (h /. x1)) + ((h /. x1) - (l /. x0))).|| by RLVECT_1: 28

          .= ||.(((l /. x1) - (h /. x1)) + ((((h /. x1) - (h /. x0)) + (h /. x0)) - (l /. x0))).|| by RLVECT_4: 1

          .= ||.(((l /. x1) - (h /. x1)) + (((h /. x1) - (h /. x0)) + ((h /. x0) - (l /. x0)))).|| by RLVECT_1: 28;

          then

           A19: ||.((l /. x1) - (l /. x0)).|| <= ( ||.((l /. x1) - (h /. x1)).|| + ||.(((h /. x1) - (h /. x0)) + ((h /. x0) - (l /. x0))).||) by NORMSP_1:def 1;

           ||.((h /. x1) - (l /. x1)).|| < (r / 3) by A8, A16, A14, XXREAL_0: 25;

          then ||.( - ((l /. x1) - (h /. x1))).|| < (r / 3) by RLVECT_1: 33;

          then ||.((l /. x1) - (h /. x1)).|| < (r / 3) by NORMSP_1: 2;

          then ( ||.((l /. x1) - (h /. x1)).|| + ||.(((h /. x1) - (h /. x0)) + ((h /. x0) - (l /. x0))).||) < ((r / 3) + ((r / 3) + (r / 3))) by A18, XREAL_1: 8;

          then ||.((l /. x1) - (l /. x0)).|| < (((r / 3) + (r / 3)) + (r / 3)) by A19, XXREAL_0: 2;

          then ||.(((l | X) /. x1) - (l /. x0)).|| < r by A14, PARTFUN1: 80;

          hence thesis by A4, RELAT_1: 68;

        end;

        hence thesis by NFCONT_1: 7, A60;

      end;

      hence thesis by NFCONT_1:def 7, A4;

    end;