lopban11.miz



    begin

    theorem :: LOPBAN11:1

    

     NDIFF825: for n be Nat, r be Real st 0 < r holds ex s be Real st 0 < s & s < r & ( sqrt ((s * s) * n)) < r

    proof

      let n be Nat, r be Real;

      assume

       A1: 0 < r;

      per cases ;

        suppose

         A2: 0 = n;

        set s = (r / 2);

        take s;

        thus 0 < s & s < r & ( sqrt ((s * s) * n)) < r by A1, A2, SQUARE_1: 17, XREAL_1: 216;

      end;

        suppose

         A3: 0 <> n;

        set s = (r / (n + 1));

        take s;

        set s = (r / (n + 1));

        

         A4: (n + 0 ) < (n + 1) by XREAL_1: 8;

        thus 0 < s by A1;

        ( 0 + 1) <= n by A3, NAT_1: 13;

        then (1 * n) <= (n * n) by XREAL_1: 66;

        then

         A6: ((s * s) * n) <= ((s * s) * (n * n)) by XREAL_1: 66;

         0 < 1 & ( 0 + 1) < (n + 1) by A3, XREAL_1: 8;

        then (1 / (n + 1)) < 1 by XREAL_1: 191;

        then ((1 / (n + 1)) * r) < (r * 1) by A1, XREAL_1: 68;

        hence s < r;

        ( sqrt ((s * s) * n)) <= ( sqrt ((s * n) ^2 )) by A6, SQUARE_1: 26;

        then

         A8: ( sqrt ((s * s) * n)) <= (s * n) by A1, SQUARE_1: 22;

        (n / (n + 1)) < 1 by A4, XREAL_1: 191;

        then ((n / (n + 1)) * r) < (r * 1) by A1, XREAL_1: 68;

        hence ( sqrt ((s * s) * n)) < r by A8, XXREAL_0: 2;

      end;

    end;

    theorem :: LOPBAN11:2

    

     LM03: for R1,R2 be FinSequence of REAL , n,i be Nat, r be Real st i in ( dom R1) & R1 = (n |-> 1 qua Real) & R2 = (R1 +* (i,r)) holds ( Product R2) = r

    proof

      let R1,R2 be FinSequence of REAL , n,i be Nat, r be Real;

      assume that

       A1: i in ( dom R1) and

       A2: R1 = (n |-> 1 qua Real) and

       A3: R2 = (R1 +* (i,r));

      i in ( Seg n) by A1, A2, FUNCT_2:def 1;

      then

       A4: (R1 . i) = 1 by A2, FUNCOP_1: 7;

      

       A5: ( Product R1) = 1 by A2, RVSUM_1: 102;

      

      thus ( Product R2) = ((( Product R1) * r) / (R1 . i)) by A1, A2, A3, RVSUM_3: 25

      .= r by A4, A5;

    end;

    theorem :: LOPBAN11:3

    for F be FinSequence of REAL st (for k be Element of NAT st k in ( dom F) holds 0 <= (F . k)) holds 0 <= ( Product F)

    proof

      defpred P[ Nat] means for F be FinSequence of REAL st (for k be Element of NAT st k in ( dom F) holds 0 <= (F . k)) & ( len F) = $1 holds 0 <= ( Product F);

      let F be FinSequence of REAL ;

      

       A1: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A2: P[n];

        for F be FinSequence of REAL st (for k be Element of NAT st k in ( dom F) holds 0 <= (F . k)) & ( len F) = (n + 1) holds 0 <= ( Product F)

        proof

          let F be FinSequence of REAL ;

          assume

           A3: for k be Element of NAT st k in ( dom F) holds 0 <= (F . k);

          assume

           A4: ( len F) = (n + 1);

          then

          consider F1,F2 be FinSequence of REAL such that

           A5: ( len F1) = n and

           A6: ( len F2) = 1 and

           A7: F = (F1 ^ F2) by FINSEQ_2: 23;

          1 in ( Seg 1);

          then 1 in ( dom F2) by A6, FINSEQ_1:def 3;

          then

           A8: (F . (n + 1)) = (F2 . 1) by A5, A7, FINSEQ_1:def 7;

          for k be Element of NAT st k in ( dom F1) holds 0 <= (F1 . k)

          proof

            let k be Element of NAT ;

            assume

             A9: k in ( dom F1);

            then 0 <= (F . k) by A3, A7, FINSEQ_2: 15;

            hence thesis by A7, A9, FINSEQ_1:def 7;

          end;

          then

           A10: 0 <= ( Product F1) by A2, A5;

          set x = (F2 . 1);

          ( Seg (n + 1)) = ( dom F) by A4, FINSEQ_1:def 3;

          then

           A11: 0 <= x by A3, A8, FINSEQ_1: 3;

          ( Product F) = ( Product (F1 ^ <*x*>)) by A6, A7, FINSEQ_1: 40

          .= (( Product F1) * x) by RVSUM_1: 96;

          hence thesis by A10, A11;

        end;

        hence thesis;

      end;

      

       A12: P[ 0 ]

      proof

        let F be FinSequence of REAL such that for k be Element of NAT st k in ( dom F) holds 0 <= (F . k);

        assume ( len F) = 0 ;

        then F = ( <*> REAL );

        hence thesis by RVSUM_1: 94;

      end;

      

       A13: for n be Nat holds P[n] from NAT_1:sch 2( A12, A1);

      

       A14: ex n be Element of NAT st n = ( len F);

      assume for k be Element of NAT st k in ( dom F) holds 0 <= (F . k);

      hence thesis by A13, A14;

    end;

    reserve X,G for RealNormSpace-Sequence,

Y for RealNormSpace;

    reserve f for MultilinearOperator of X, Y;

    theorem :: LOPBAN11:4

    

     DCARXX: ( dom ( carr X)) = ( dom X)

    proof

      ( dom ( carr X)) = ( Seg ( len ( carr X))) by FINSEQ_1:def 3;

      

      hence ( dom ( carr X)) = ( Seg ( len X)) by PRVECT_1:def 11

      .= ( dom X) by FINSEQ_1:def 3;

    end;

    theorem :: LOPBAN11:5

    

     ZERXI: for z be Element of ( product X) st z = ( 0. ( product X)) holds for i be Element of ( dom X) holds (z . i) = ( 0. (X . i))

    proof

      let z be Element of ( product X);

      assume

       A1: z = ( 0. ( product X));

      let i be Element of ( dom X);

      

       A2: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      reconsider j = i as Element of ( dom ( carr X)) by DCARXX;

      (( zeros X) . j) = ( 0. (X . j)) by PRVECT_1:def 14;

      hence (z . i) = ( 0. (X . i)) by A1, A2;

    end;

    theorem :: LOPBAN11:6

    

     FXZER: (f . ( 0. ( product X))) = ( 0. Y)

    proof

      

       A1: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      reconsider z = ( 0. ( product X)) as Element of ( product ( carr X)) by A1;

      set i = the Element of ( dom X);

      (z . i) = ( 0. (X . i)) by ZERXI;

      hence (f . ( 0. ( product X))) = ( 0. Y) by LOPBAN10: 36;

    end;

    theorem :: LOPBAN11:7

    

     PSPROD: for F be FinSequence of REAL st for i be Element of ( dom F) holds (F . i) > 0 holds ( Product F) > 0

    proof

      let F be FinSequence of REAL ;

      assume for i be Element of ( dom F) holds (F . i) > 0 ;

      then for j be Element of NAT st j in ( dom F) holds (F . j) > 0 ;

      hence ( Product F) > 0 by NAT_4: 42;

    end;

    theorem :: LOPBAN11:8

    

     Th42: for X be RealNormSpace-Sequence, Y be RealNormSpace st Y is complete holds for seq be sequence of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace such that

       A1: Y is complete;

      let vseq be sequence of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) such that

       A2: vseq is Cauchy_sequence_by_Norm;

      defpred P[ set, set] means ex xseq be sequence of Y st (for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . $1)) & xseq is convergent & $2 = ( lim xseq);

      

       A3: for x be Element of ( product X) holds ex y be Element of Y st P[x, y]

      proof

        let x be Element of ( product X);

        deffunc F( Nat) = (( modetrans ((vseq . $1),X,Y)) . x);

        consider xseq be sequence of Y such that

         A4: for n be Element of NAT holds (xseq . n) = F(n) from FUNCT_2:sch 4;

        

         A5: for n be Nat holds (xseq . n) = F(n)

        proof

          let n be Nat;

          n in NAT by ORDINAL1:def 12;

          hence thesis by A4;

        end;

        take ( lim xseq);

        

         A6: for m,k be Nat holds ||.((xseq . m) - (xseq . k)).|| <= ( ||.((vseq . m) - (vseq . k)).|| * ( NrProduct x))

        proof

          let m,k be Nat;

          reconsider h1 = ((vseq . m) - (vseq . k)) as Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

          k in NAT by ORDINAL1:def 12;

          then

           A7: (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A4;

          

           a8: (vseq . m) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

          

           a9: (vseq . k) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

          m in NAT by ORDINAL1:def 12;

          then (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A4;

          then ((xseq . m) - (xseq . k)) = (h1 . x) by A7, a8, a9, LOPBAN10: 52;

          hence thesis by LOPBAN10: 45;

        end;

        now

          let e be Real such that

           A10: e > 0 ;

          now

            per cases ;

              case

               A11: ex i be Element of ( dom X) st (x . i) = ( 0. (X . i));

              reconsider k = 0 as Nat;

              take k;

              thus for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e

              proof

                let n,m be Nat such that n >= k and m >= k;

                m in NAT by ORDINAL1:def 12;

                

                then

                 A12: (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A4

                .= ( 0. Y) by A11, LOPBAN10: 36;

                n in NAT by ORDINAL1:def 12;

                

                then (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) by A4

                .= ( 0. Y) by A11, LOPBAN10: 36;

                hence thesis by A10, A12;

              end;

            end;

              case not ex i be Element of ( dom X) st (x . i) = ( 0. (X . i));

              then

               A13: ( NrProduct x) > 0 by LOPBAN10: 27;

              then

              consider k be Nat such that

               A15: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < (e / ( NrProduct x)) by A2, A10, RSSPACE3: 8;

              take k;

              thus for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e

              proof

                let n,m be Nat such that

                 A16: n >= k and

                 A17: m >= k;

                 ||.((vseq . n) - (vseq . m)).|| < (e / ( NrProduct x)) by A15, A16, A17;

                then

                 A18: ( ||.((vseq . n) - (vseq . m)).|| * ( NrProduct x)) < ((e / ( NrProduct x)) * ( NrProduct x)) by A13, XREAL_1: 68;

                

                 A19: ((e / ( NrProduct x)) * ( NrProduct x)) = (e * ((( NrProduct x) " ) * ( NrProduct x)))

                .= (e * 1) by A13, XCMPLX_0:def 7

                .= e;

                 ||.((xseq . n) - (xseq . m)).|| <= ( ||.((vseq . n) - (vseq . m)).|| * ( NrProduct x)) by A6;

                hence thesis by A18, A19, XXREAL_0: 2;

              end;

            end;

          end;

          hence ex k be Nat st for n,m be Nat st n >= k & m >= k holds ||.((xseq . n) - (xseq . m)).|| < e;

        end;

        then xseq is Cauchy_sequence_by_Norm by RSSPACE3: 8;

        hence thesis by A1, A5;

      end;

      consider f be Function of the carrier of ( product X), the carrier of Y such that

       A20: for x be Element of ( product X) holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

      reconsider tseq = f as Function of ( product X), Y;

      

       A21: for u be Point of ( product X), i be Element of ( dom X), x be Point of (X . i) holds ex xseqi be sequence of Y st (for n be Nat holds (xseqi . n) = ((( modetrans ((vseq . n),X,Y)) * ( reproj (i,u))) . x)) & xseqi is convergent & ((tseq * ( reproj (i,u))) . x) = ( lim xseqi)

      proof

        let u be Point of ( product X), i be Element of ( dom X), x be Point of (X . i);

        reconsider v = (( reproj (i,u)) . x) as Point of ( product X);

        consider xseq be sequence of Y such that

         A22: (for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . v)) & xseq is convergent & (tseq . v) = ( lim xseq) by A20;

        

         A23: ( dom ( reproj (i,u))) = the carrier of (X . i) by FUNCT_2:def 1;

        take xseq;

        thus for n be Nat holds (xseq . n) = ((( modetrans ((vseq . n),X,Y)) * ( reproj (i,u))) . x)

        proof

          let n be Nat;

          

          thus (xseq . n) = (( modetrans ((vseq . n),X,Y)) . v) by A22

          .= ((vseq . n) . (( reproj (i,u)) . x)) by LOPBAN10:def 13

          .= (((vseq . n) * ( reproj (i,u))) . x) by A23, FUNCT_1: 13

          .= ((( modetrans ((vseq . n),X,Y)) * ( reproj (i,u))) . x) by LOPBAN10:def 13;

        end;

        thus xseq is convergent by A22;

        thus ((tseq * ( reproj (i,u))) . x) = ( lim xseq) by A22, A23, FUNCT_1: 13;

      end;

      now

        let i be Element of ( dom X), u be Point of ( product X);

        set tseqiu = (tseq * ( reproj (i,u)));

        deffunc H( Nat) = (( modetrans ((vseq . $1),X,Y)) * ( reproj (i,u)));

         A24:

        now

          let x,y be Point of (X . i);

          consider xseq be sequence of Y such that

           A25: for n be Nat holds (xseq . n) = ( H(n) . x) and

           A26: xseq is convergent and

           A27: (tseqiu . x) = ( lim xseq) by A21;

          consider zseq be sequence of Y such that

           A28: for n be Nat holds (zseq . n) = ( H(n) . (x + y)) and zseq is convergent and

           A29: (tseqiu . (x + y)) = ( lim zseq) by A21;

          consider yseq be sequence of Y such that

           A30: for n be Nat holds (yseq . n) = ( H(n) . y) and

           A31: yseq is convergent and

           A32: (tseqiu . y) = ( lim yseq) by A21;

          now

            let n be Nat;

            

             A33: H(n) is LinearOperator of (X . i), Y by LOPBAN10:def 6;

            

            thus (zseq . n) = ( H(n) . (x + y)) by A28

            .= (( H(n) . x) + ( H(n) . y)) by A33, VECTSP_1:def 20

            .= ((xseq . n) + ( H(n) . y)) by A25

            .= ((xseq . n) + (yseq . n)) by A30;

          end;

          then zseq = (xseq + yseq) by NORMSP_1:def 2;

          hence (tseqiu . (x + y)) = ((tseqiu . x) + (tseqiu . y)) by A26, A27, A29, A31, A32, NORMSP_1: 25;

        end;

        now

          let x be Point of (X . i);

          let a be Real;

          consider xseq be sequence of Y such that

           A34: for n be Nat holds (xseq . n) = ( H(n) . x) and

           A35: xseq is convergent and

           A36: (tseqiu . x) = ( lim xseq) by A21;

          consider zseq be sequence of Y such that

           A37: for n be Nat holds (zseq . n) = ( H(n) . (a * x)) and zseq is convergent and

           A38: (tseqiu . (a * x)) = ( lim zseq) by A21;

          now

            let n be Nat;

            

             A39: H(n) is LinearOperator of (X . i), Y by LOPBAN10:def 6;

            

            thus (zseq . n) = ( H(n) . (a * x)) by A37

            .= (a * ( H(n) . x)) by A39, LOPBAN_1:def 5

            .= (a * (xseq . n)) by A34;

          end;

          then zseq = (a * xseq) by NORMSP_1:def 5;

          hence (tseqiu . (a * x)) = (a * (tseqiu . x)) by A35, A36, A38, NORMSP_1: 28;

        end;

        hence (tseq * ( reproj (i,u))) is LinearOperator of (X . i), Y by A24, LOPBAN_1:def 5, VECTSP_1:def 20;

      end;

      then

      reconsider tseq as MultilinearOperator of X, Y by LOPBAN10:def 6;

       B39:

      now

        let e1 be Real such that

         A40: e1 > 0 ;

        reconsider e = e1 as Real;

        consider k be Nat such that

         A41: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, A40, RSSPACE3: 8;

        reconsider k as Nat;

        take k;

        now

          let m be Nat;

          assume m >= k;

          then

           A42: ||.((vseq . m) - (vseq . k)).|| < e by A41;

          

           A43: ||.(vseq . m).|| = ( ||.vseq.|| . m) by NORMSP_0:def 4;

          

           A44: ||.(vseq . k).|| = ( ||.vseq.|| . k) by NORMSP_0:def 4;

           |.( ||.(vseq . m).|| - ||.(vseq . k).||).| <= ||.((vseq . m) - (vseq . k)).|| by NORMSP_1: 9;

          hence |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1 by A42, A43, A44, XXREAL_0: 2;

        end;

        hence for m be Nat st m >= k holds |.(( ||.vseq.|| . m) - ( ||.vseq.|| . k)).| < e1;

      end;

      then

       A45: ||.vseq.|| is convergent by SEQ_4: 41;

      

       A46: tseq is Lipschitzian

      proof

        take ( lim ||.vseq.||);

         A47:

        now

          let x be Point of ( product X);

          consider xseq be sequence of Y such that

           A48: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) and

           A49: xseq is convergent and

           A50: (tseq . x) = ( lim xseq) by A20;

          

           A51: ||.(tseq . x).|| = ( lim ||.xseq.||) by A49, A50, LOPBAN_1: 20;

          

           A52: for m be Nat holds ||.(xseq . m).|| <= ( ||.(vseq . m).|| * ( NrProduct x))

          proof

            let m be Nat;

            

             A53: (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A48;

            (vseq . m) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

            hence thesis by A53, LOPBAN10: 45;

          end;

          

           A54: for n be Nat holds ( ||.xseq.|| . n) <= ((( NrProduct x) (#) ||.vseq.||) . n)

          proof

            let n be Nat;

            

             A55: ( ||.xseq.|| . n) = ||.(xseq . n).|| by NORMSP_0:def 4;

            

             A56: ||.(vseq . n).|| = ( ||.vseq.|| . n) by NORMSP_0:def 4;

             ||.(xseq . n).|| <= ( ||.(vseq . n).|| * ( NrProduct x)) by A52;

            hence thesis by A55, A56, SEQ_1: 9;

          end;

          

           A58: ( lim (( NrProduct x) (#) ||.vseq.||)) = (( lim ||.vseq.||) * ( NrProduct x)) by B39, SEQ_2: 8, SEQ_4: 41;

           ||.xseq.|| is convergent by A49, A50, LOPBAN_1: 20;

          hence ||.(tseq . x).|| <= (( lim ||.vseq.||) * ( NrProduct x)) by A45, A51, A54, A58, SEQ_2: 18;

        end;

        now

          let n be Nat;

           ||.(vseq . n).|| >= 0 ;

          hence ( ||.vseq.|| . n) >= 0 by NORMSP_0:def 4;

        end;

        hence thesis by B39, A47, SEQ_2: 17, SEQ_4: 41;

      end;

      

       A59: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds for x be Point of ( product X) holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= (e * ( NrProduct x))

      proof

        let e be Real;

        assume e > 0 ;

        then

        consider k be Nat such that

         A60: for n,m be Nat st n >= k & m >= k holds ||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3: 8;

        take k;

        now

          let n be Nat such that

           A61: n >= k;

          now

            let x be Point of ( product X);

            consider xseq be sequence of Y such that

             A62: for n be Nat holds (xseq . n) = (( modetrans ((vseq . n),X,Y)) . x) and

             A63: xseq is convergent and

             A64: (tseq . x) = ( lim xseq) by A20;

            

             A65: for m,k be Nat holds ||.((xseq . m) - (xseq . k)).|| <= ( ||.((vseq . m) - (vseq . k)).|| * ( NrProduct x))

            proof

              let m,k be Nat;

              reconsider h1 = ((vseq . m) - (vseq . k)) as Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

              

               A66: (xseq . k) = (( modetrans ((vseq . k),X,Y)) . x) by A62;

              

               a67: (vseq . m) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

              

               a68: (vseq . k) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

              (xseq . m) = (( modetrans ((vseq . m),X,Y)) . x) by A62;

              then ((xseq . m) - (xseq . k)) = (h1 . x) by A66, a67, a68, LOPBAN10: 52;

              hence thesis by LOPBAN10: 45;

            end;

            

             A69: for m be Nat st m >= k holds ||.((xseq . n) - (xseq . m)).|| <= (e * ( NrProduct x))

            proof

              let m be Nat;

              assume m >= k;

              then

               A70: ||.((vseq . n) - (vseq . m)).|| < e by A60, A61;

              

               A71: ||.((xseq . n) - (xseq . m)).|| <= ( ||.((vseq . n) - (vseq . m)).|| * ( NrProduct x)) by A65;

              ( ||.((vseq . n) - (vseq . m)).|| * ( NrProduct x)) <= (e * ( NrProduct x)) by A70, XREAL_1: 64;

              hence thesis by A71, XXREAL_0: 2;

            end;

             ||.((xseq . n) - (tseq . x)).|| <= (e * ( NrProduct x))

            proof

              deffunc F( Nat) = ||.((xseq . $1) - (xseq . n)).||;

              consider rseq be Real_Sequence such that

               A72: for m be Nat holds (rseq . m) = F(m) from SEQ_1:sch 1;

              now

                let x be object;

                assume x in NAT ;

                then

                reconsider k = x as Nat;

                

                thus (rseq . x) = ||.((xseq . k) - (xseq . n)).|| by A72

                .= ||.((xseq - (xseq . n)) . k).|| by NORMSP_1:def 4

                .= ( ||.(xseq - (xseq . n)).|| . x) by NORMSP_0:def 4;

              end;

              then

               A73: rseq = ||.(xseq - (xseq . n)).|| by FUNCT_2: 12;

              

               A74: (xseq - (xseq . n)) is convergent by A63, NORMSP_1: 21;

              ( lim (xseq - (xseq . n))) = ((tseq . x) - (xseq . n)) by A63, A64, NORMSP_1: 27;

              then

               A75: ( lim rseq) = ||.((tseq . x) - (xseq . n)).|| by A73, A74, LOPBAN_1: 41;

              for m be Nat st m >= k holds (rseq . m) <= (e * ( NrProduct x))

              proof

                let m be Nat such that

                 A76: m >= k;

                (rseq . m) = ||.((xseq . m) - (xseq . n)).|| by A72

                .= ||.((xseq . n) - (xseq . m)).|| by NORMSP_1: 7;

                hence thesis by A69, A76;

              end;

              then ( lim rseq) <= (e * ( NrProduct x)) by A73, A74, LOPBAN_1: 41, RSSPACE2: 5;

              hence thesis by A75, NORMSP_1: 7;

            end;

            hence ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= (e * ( NrProduct x)) by A62;

          end;

          hence for x be Point of ( product X) holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= (e * ( NrProduct x));

        end;

        hence thesis;

      end;

      reconsider tseq as Lipschitzian MultilinearOperator of X, Y by A46;

      reconsider tv = tseq as Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) by LOPBAN10:def 11;

      

       A77: for e be Real st e > 0 holds ex k be Nat st for n be Nat st n >= k holds ||.((vseq . n) - tv).|| <= e

      proof

        let e be Real such that

         A78: e > 0 ;

        consider k be Nat such that

         A79: for n be Nat st n >= k holds for x be Point of ( product X) holds ||.((( modetrans ((vseq . n),X,Y)) . x) - (tseq . x)).|| <= (e * ( NrProduct x)) by A59, A78;

        now

          set g1 = tseq;

          let n be Nat such that

           A80: n >= k;

          reconsider h1 = ((vseq . n) - tv) as Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

          set f1 = ( modetrans ((vseq . n),X,Y));

           A81:

          now

            let t be Point of ( product X);

            assume for i be Element of ( dom X) holds ||.(t . i).|| <= 1;

            then 0 <= ( NrProduct t) & ( NrProduct t) <= 1 by LOPBAN10: 35;

            then

             A82: (e * ( NrProduct t)) <= (e * 1) by A78, XREAL_1: 64;

            

             A83: ||.((f1 . t) - (g1 . t)).|| <= (e * ( NrProduct t)) by A79, A80;

            (vseq . n) is Lipschitzian MultilinearOperator of X, Y by LOPBAN10:def 11;

            then ||.(h1 . t).|| = ||.((f1 . t) - (g1 . t)).|| by LOPBAN10: 52;

            hence ||.(h1 . t).|| <= e by A82, A83, XXREAL_0: 2;

          end;

           A84:

          now

            let r be Real;

            assume r in ( PreNorms h1);

            then ex t be Point of ( product X) st r = ||.(h1 . t).|| & for i be Element of ( dom X) holds ||.(t . i).|| <= 1;

            hence r <= e by A81;

          end;

          (for s be Real st s in ( PreNorms h1) holds s <= e) implies ( upper_bound ( PreNorms h1)) <= e by SEQ_4: 45;

          hence ||.((vseq . n) - tv).|| <= e by A84, LOPBAN10: 43;

        end;

        hence thesis;

      end;

      for e be Real st e > 0 holds ex m be Nat st for n be Nat st n >= m holds ||.((vseq . n) - tv).|| < e

      proof

        let e be Real such that

         A86: e > 0 ;

        consider m be Nat such that

         A87: for n be Nat st n >= m holds ||.((vseq . n) - tv).|| <= (e / 2) by A77, A86;

        

         A88: (e / 2) < e by A86, XREAL_1: 216;

        now

          let n be Nat;

          assume n >= m;

          then ||.((vseq . n) - tv).|| <= (e / 2) by A87;

          hence ||.((vseq . n) - tv).|| < e by A88, XXREAL_0: 2;

        end;

        hence thesis;

      end;

      hence thesis by NORMSP_1:def 6;

    end;

    theorem :: LOPBAN11:9

    

     Th43: for X be RealNormSpace-Sequence holds for Y be RealBanachSpace holds ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) is RealBanachSpace

    proof

      let X be RealNormSpace-Sequence;

      let Y be RealBanachSpace;

      for seq be sequence of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds seq is convergent by Th42;

      hence thesis by LOPBAN_1:def 15;

    end;

    registration

      let X be RealNormSpace-Sequence;

      let Y be RealBanachSpace;

      cluster ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) -> complete;

      coherence by Th43;

    end

    begin

    theorem :: LOPBAN11:10

    

     NDIFF823: for n be Nat, F be Element of ( REAL n), s be Real st for i be Nat st i in ( dom F) holds 0 <= (F . i) & (F . i) <= s holds |.F.| <= ( sqrt ((s * s) * ( len F)))

    proof

      let n be Nat, F be Element of ( REAL n), s be Real;

      assume

       A1: for i be Nat st i in ( dom F) holds 0 <= (F . i) & (F . i) <= s;

      

       A2: 0 <= ( Sum ( sqr F)) by RVSUM_1: 86;

      set G = (( len F) |-> s);

      

       A3: ( sqr G) = (( len F) |-> (s ^2 )) by RVSUM_1: 56;

      ( len F) is natural Number & s is Element of REAL by XREAL_0:def 1;

      then

      reconsider G as Element of (( len F) -tuples_on REAL ) by FINSEQ_2: 112;

      reconsider F0 = F as Element of (( len F) -tuples_on REAL ) by FINSEQ_2: 92;

      for j be Nat st j in ( Seg ( len F0)) holds (( sqr F0) . j) <= (( sqr G) . j)

      proof

        let j be Nat;

        assume

         A4: j in ( Seg ( len F0));

        then

         A5: j in ( dom F) by FINSEQ_1:def 3;

        

         A6: (( sqr F0) . j) = ((F . j) ^2 ) by VALUED_1: 11;

        

         A7: (( sqr G) . j) = ((G . j) ^2 ) by VALUED_1: 11;

        

         A8: 0 <= (F0 . j) by A1, A5;

        (F0 . j) <= s by A1, A5;

        then (F0 . j) <= (G . j) by A4, FINSEQ_2: 57;

        hence thesis by A6, A7, A8, SQUARE_1: 15;

      end;

      then ( Sum ( sqr F0)) <= ( Sum ( sqr G)) by RVSUM_1: 82;

      then ( Sum ( sqr F)) <= ((s * s) * ( len F)) by A3, RVSUM_1: 80;

      hence thesis by A2, SQUARE_1: 26;

    end;

    theorem :: LOPBAN11:11

    

     LM02: for X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y, K be Real st ( 0 <= K & for x be Point of ( product X) holds ||.(f . x).|| <= (K * ( NrProduct x))) holds for v0,v1 be Point of ( product X), Cv0,Cv1 be FinSequence, i be Element of ( dom X) st Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & for j be Element of ( dom X) st i <> j holds (Cv1 . j) = (Cv0 . j) holds ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 1) |^ ( len X)) * K) * ||.((v1 - v0) . i).||)

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y, K be Real;

      assume

       A1: 0 <= K & for x be Point of ( product X) holds ||.(f . x).|| <= (K * ( NrProduct x));

      let v0,v1 be Point of ( product X), Cv0,Cv1 be FinSequence, i be Element of ( dom X);

      assume

       A2: Cv0 = v0 & Cv1 = v1 & ||.(v1 - v0).|| <= 1 & for j be Element of ( dom X) st i <> j holds (Cv1 . j) = (Cv0 . j);

      f is Function of ( product X), Y & f is Multilinear;

      then

       A3: (f * ( reproj (i,v0))) is LinearOperator of (X . i), Y;

      

       A4: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      then

       A5: ex g be Function st Cv1 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A2, CARD_3:def 5;

      

       A6: ex g be Function st (( reproj (i,v0)) . (v1 . i)) = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A4, CARD_3:def 5;

      for x be object st x in ( dom v1) holds (v1 . x) = ((( reproj (i,v0)) . (v1 . i)) . x)

      proof

        let x be object;

        assume x in ( dom v1);

        then

        reconsider j = x as Element of ( dom X) by A2, A5, DCARXX;

        per cases ;

          suppose j = i;

          hence (v1 . x) = ((( reproj (i,v0)) . (v1 . i)) . x) by LOPBAN10: 15;

        end;

          suppose

           A8: j <> i;

          

          then ((( reproj (i,v0)) . (v1 . i)) . j) = (v0 . j) by LOPBAN10: 16

          .= (v1 . j) by A2, A8;

          hence (v1 . x) = ((( reproj (i,v0)) . (v1 . i)) . x);

        end;

      end;

      then

       A10: v1 = (( reproj (i,v0)) . (v1 . i)) by A2, A5, A6, FUNCT_1: 2;

      reconsider v3 = (( reproj (i,v0)) . ((v1 . i) - (v0 . i))) as Point of ( product X);

      ((f /. v1) - (f /. v0)) = ((f . (( reproj (i,v0)) . (v1 . i))) - (f . (( reproj (i,v0)) . (v0 . i)))) by A10, LOPBAN10: 17

      .= (((f * ( reproj (i,v0))) . (v1 . i)) - (f . (( reproj (i,v0)) . (v0 . i)))) by FUNCT_2: 15

      .= (((f * ( reproj (i,v0))) . (v1 . i)) - ((f * ( reproj (i,v0))) . (v0 . i))) by FUNCT_2: 15

      .= (((f * ( reproj (i,v0))) . (v1 . i)) + (( - 1) * ((f * ( reproj (i,v0))) . (v0 . i)))) by RLVECT_1: 16

      .= (((f * ( reproj (i,v0))) . (v1 . i)) + ((f * ( reproj (i,v0))) . (( - 1) * (v0 . i)))) by A3, LOPBAN_1:def 5

      .= ((f * ( reproj (i,v0))) . ((v1 . i) + (( - 1) * (v0 . i)))) by A3, VECTSP_1:def 20

      .= ((f * ( reproj (i,v0))) . ((v1 . i) - (v0 . i))) by RLVECT_1: 16

      .= (f . v3) by FUNCT_2: 15;

      then

       A12: ||.((f /. v1) - (f /. v0)).|| <= (K * ( NrProduct v3)) by A1;

      1 is Element of REAL by XREAL_0:def 1;

      then

      reconsider R1 = (( len X) |-> 1 qua Real) as FinSequence of REAL by FINSEQ_2: 63;

      

       A13: ( dom R1) = ( Seg ( len X)) by FUNCT_2:def 1;

      i in ( dom X);

      then

       A14: i in ( dom R1) by A13, FINSEQ_1:def 3;

      reconsider Nv1v0 = ||.((v1 - v0) . i).|| as Element of REAL ;

      reconsider R2 = (R1 +* (i,Nv1v0)) as FinSequence of REAL ;

      ( ||.v0.|| + 1) is Element of REAL by XREAL_0:def 1;

      then

      reconsider R3 = (( len X) |-> ( ||.v0.|| + 1)) as FinSequence of REAL by FINSEQ_2: 63;

      set R4 = ( mlt (R2,R3));

      ( dom R2) = ( dom R1) by FUNCT_7: 30;

      then ( dom R2) = ( Seg ( len X)) & ( dom R3) = ( Seg ( len X)) by FUNCT_2:def 1;

      then

       A15: ( len R2) = ( len X) & ( len R3) = ( len X) by FINSEQ_1:def 3;

      then R2 is Element of (( len X) -tuples_on REAL ) & R3 is Element of (( len X) -tuples_on REAL ) by FINSEQ_2: 92;

      then

       A16: ( Product R4) = (( Product R2) * ( Product R3)) by RVSUM_1: 107;

      

       A17: ( Product R2) = ||.((v1 - v0) . i).|| by A14, LM03;

      

       A18: ( Product R3) = (( ||.v0.|| + 1) to_power ( len X)) by NAT_4: 55

      .= (( ||.v0.|| + 1) |^ ( len X));

      consider Nx be FinSequence of REAL such that

       A19: ( dom Nx) = ( dom X) & (for i be Element of ( dom X) holds (Nx . i) = ||.(v3 . i).||) & ( NrProduct v3) = ( Product Nx) by LOPBAN10:def 9;

      ( dom Nx) = ( Seg ( len X)) by A19, FINSEQ_1:def 3;

      then

       A20: ( len Nx) = ( len X) by FINSEQ_1:def 3;

      ( dom R4) = (( dom R2) /\ ( dom R3)) by VALUED_1:def 4

      .= (( Seg ( len R2)) /\ ( dom R3)) by FINSEQ_1:def 3

      .= (( Seg ( len R2)) /\ ( Seg ( len R3))) by FINSEQ_1:def 3

      .= ( Seg ( len X)) by A15;

      then

       A21: ( len R4) = ( len X) by FINSEQ_1:def 3;

      for k be Element of NAT st k in ( dom Nx) holds (Nx . k) <= (R4 . k) & 0 <= (Nx . k)

      proof

        let k be Element of NAT ;

        assume k in ( dom Nx);

        then

         A22: k in ( Seg ( len Nx)) by FINSEQ_1:def 3;

        then

        reconsider j = k as Element of ( dom X) by A20, FINSEQ_1:def 3;

        

         A24: (Nx . k) = ||.(v3 . j).|| by A19;

        

         A26: (R4 . k) = ((R2 . k) * (R3 . j)) by RVSUM_1: 60

        .= ((R2 . k) * ( ||.v0.|| + 1)) by A20, A22, FUNCOP_1: 7;

        now

          per cases ;

            suppose

             A27: j = i;

            (v3 . j) = ((v1 . i) - (v0 . i)) by A27, LOPBAN10: 15

            .= ((v1 - v0) . i) by LOPBAN10: 26;

            then

             A29: (Nx . k) = ||.((v1 - v0) . i).|| by A19, A27;

            (1 + 0 ) <= ( ||.v0.|| + 1) by XREAL_1: 7;

            then ( ||.((v1 - v0) . i).|| * 1) <= ( ||.((v1 - v0) . i).|| * ( ||.v0.|| + 1)) by XREAL_1: 66;

            hence (Nx . k) <= (R4 . k) by A13, A20, A22, A26, A27, A29, FUNCT_7: 31;

          end;

            suppose

             A30: j <> i;

            

            then

             A31: (R2 . k) = (R1 . j) by FUNCT_7: 32

            .= 1 by A20, A22, FUNCOP_1: 7;

             ||.(v0 . j).|| <= ||.v0.|| by A4, PRVECT_2: 10;

            then ( ||.(v0 . j).|| + 0 ) <= ( ||.v0.|| + 1) by XREAL_1: 7;

            hence (Nx . k) <= (R4 . k) by A24, A26, A30, A31, LOPBAN10: 16;

          end;

        end;

        hence thesis by A24;

      end;

      then ( NrProduct v3) <= ( ||.((v1 - v0) . i).|| * (( ||.v0.|| + 1) |^ ( len X))) by A16, A17, A18, A19, A20, A21, FINSEQ_9: 34;

      then (K * ( NrProduct v3)) <= (K * ((( ||.v0.|| + 1) |^ ( len X)) * ||.((v1 - v0) . i).||)) by A1, XREAL_1: 66;

      hence thesis by A12, XXREAL_0: 2;

    end;

    theorem :: LOPBAN11:12

    

     LM01: for X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y, K be Real st ( 0 <= K & for x be Point of ( product X) holds ||.(f . x).|| <= (K * ( NrProduct x))) holds for v0 be Point of ( product X) holds ex M be Real st 0 <= M & for v1 be Point of ( product X) st ||.(v1 - v0).|| <= 1 holds ex F be FinSequence of REAL st ( dom F) = ( dom X) & ||.((f /. v1) - (f /. v0)).|| <= ((M * K) * ( Sum F)) & for i be Element of ( dom X) holds (F . i) = ||.((v1 - v0) . i).||

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y, K be Real;

      assume that

       A1: 0 <= K and

       A2: for x be Point of ( product X) holds ||.(f . x).|| <= (K * ( NrProduct x));

      

       A3: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      let v0 be Point of ( product X);

      consider g be Function such that

       A4: v0 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

      ( dom g) = ( Seg ( len ( carr X))) by A4, FINSEQ_1:def 3;

      then

      reconsider Cv0 = v0 as FinSequence by A4, FINSEQ_1:def 2;

      set L = ( ||.v0.|| + 3);

      set M = (L |^ ( len X));

      take M;

      thus 0 <= M by POWER: 3;

      defpred P[ Nat] means for v0,v1 be Point of ( product X), Cv0,Cv1 be FinSequence st ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & $1 <= ( len X) & (Cv1 | (( len X) -' $1)) = (Cv0 | (( len X) -' $1)) holds ex F be FinSequence of REAL st ( dom F) = ( Seg $1) & ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) & for n be Nat st n in ( Seg $1) holds ex i be Element of ( dom X) st i = ((( len X) -' $1) + n) & (F . n) = ||.((v1 - v0) . i).||;

      

       A6: P[ 0 ]

      proof

        let v0,v1 be Point of ( product X), Cv0,Cv1 be FinSequence;

        assume

         A7: ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & 0 <= ( len X) & (Cv1 | (( len X) -' 0 )) = (Cv0 | (( len X) -' 0 ));

        

         A8: (( len X) -' 0 ) = ((( len X) + 0 ) -' 0 )

        .= ( len X) by NAT_D: 34;

        reconsider F = ( <*> REAL ) as FinSequence of REAL ;

        take F;

        thus ( dom F) = ( Seg 0 );

        consider g be Function such that

         A9: v0 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

        

         A10: ( dom g) = ( Seg ( len ( carr X))) by A9, FINSEQ_1:def 3;

        then

        reconsider Cv0 = v0 as FinSequence by A9, FINSEQ_1:def 2;

        

         A11: ( len Cv0) = ( len ( carr X)) by A9, A10, FINSEQ_1:def 3

        .= ( len X) by PRVECT_1:def 11;

        consider g be Function such that

         A12: v1 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

        ( dom Cv1) = ( Seg ( len ( carr X))) by A7, A12, FINSEQ_1:def 3;

        

        then

         A14: ( len Cv1) = ( len ( carr X)) by FINSEQ_1:def 3

        .= ( len X) by PRVECT_1:def 11;

        Cv1 = (Cv0 | ( len X)) by A7, A8, A14, FINSEQ_1: 58

        .= Cv0 by A11, FINSEQ_1: 58;

        then ((f /. v1) - (f /. v0)) = ( 0. Y) by A7, RLVECT_1: 15;

        hence ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) by RVSUM_1: 72;

        thus for n be Nat st n in ( Seg 0 ) holds ex i be Element of ( dom X) st i = ((( len X) -' 0 ) + n) & (F . n) = ||.((v1 - v0) . i).||;

      end;

      

       A16: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A17: P[k];

        let v0,v1 be Point of ( product X), Cv0,Cv1 be FinSequence;

        assume

         A18: ||.(v1 - v0).|| <= 1 & v0 = Cv0 & v1 = Cv1 & (k + 1) <= ( len X) & (Cv1 | (( len X) -' (k + 1))) = (Cv0 | (( len X) -' (k + 1)));

        consider g be Function such that

         A19: v0 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

        ( dom g) = ( Seg ( len ( carr X))) by A19, FINSEQ_1:def 3;

        then

        reconsider Cv0 = v0 as FinSequence by A19, FINSEQ_1:def 2;

        ( dom Cv0) = ( Seg ( len ( carr X))) by A19, FINSEQ_1:def 3;

        

        then

         A21: ( len Cv0) = ( len ( carr X)) by FINSEQ_1:def 3

        .= ( len X) by PRVECT_1:def 11;

        

        then

         A22: ( dom Cv0) = ( Seg ( len X)) by FINSEQ_1:def 3

        .= ( dom X) by FINSEQ_1:def 3;

        consider g1 be Function such that

         A23: v1 = g1 & ( dom g1) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g1 . i) in (( carr X) . i) by A3, CARD_3:def 5;

        ( dom g1) = ( Seg ( len ( carr X))) by A23, FINSEQ_1:def 3;

        then

        reconsider Cv1 = v1 as FinSequence by A23, FINSEQ_1:def 2;

        1 <= (1 + k) by NAT_1: 11;

        then 1 <= ( len X) by A18, XXREAL_0: 2;

        then ( len X) in ( Seg ( len X));

        then

        reconsider i = ( len X) as Element of ( dom X) by FINSEQ_1:def 3;

        per cases ;

          suppose

           A25: k = 0 ;

          then

           A26: (( len X) -' (k + 1)) = (( len X) - 1) by A18, XREAL_0:def 2;

          for j be Element of ( dom X) st i <> j holds (Cv1 . j) = (Cv0 . j)

          proof

            let j be Element of ( dom X);

            j in ( dom X);

            then j in ( Seg ( len X)) by FINSEQ_1:def 3;

            then

             A27: 1 <= j & j <= ( len X) by FINSEQ_1: 1;

            assume i <> j;

            then j < ( len X) by A27, XXREAL_0: 1;

            then (j + 1) <= ( len X) by NAT_1: 13;

            then ((j + 1) - 1) <= (( len X) - 1) by XREAL_1: 9;

            then

             A28: j in ( Seg (( len X) -' (k + 1))) by A26, A27;

            

            thus (Cv1 . j) = ((Cv0 | (( len X) -' (k + 1))) . j) by A18, A28, FUNCT_1: 49

            .= (Cv0 . j) by A28, FUNCT_1: 49;

          end;

          then

           A29: ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 1) |^ ( len X)) * K) * ||.((v1 - v0) . i).||) by A1, A2, A18, LM02;

          set F = <* ||.((v1 - v0) . i).||*>;

          ( rng F) c= REAL ;

          then

          reconsider F as FinSequence of REAL by FINSEQ_1:def 4;

          take F;

          

          thus ( dom F) = ( Seg ( len F)) by FINSEQ_1:def 3

          .= ( Seg (k + 1)) by A25, FINSEQ_1: 40;

          

           A31: ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 1) |^ ( len X)) * K) * ( Sum F)) by A29, RVSUM_1: 73;

          (( ||.v0.|| + 1) + 0 ) <= (( ||.v0.|| + 1) + 2) by XREAL_1: 7;

          then

           A32: (( ||.v0.|| + 1) |^ ( len X)) <= (( ||.v0.|| + 3) |^ ( len X)) by PREPOWER: 9;

           0 <= ( Sum F) by RVSUM_1: 73;

          then ((( ||.v0.|| + 1) |^ ( len X)) * (K * ( Sum F))) <= ((( ||.v0.|| + 3) |^ ( len X)) * (K * ( Sum F))) by A1, A32, XREAL_1: 64;

          hence ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) by A31, XXREAL_0: 2;

          thus for n be Nat st n in ( Seg (k + 1)) holds ex j be Element of ( dom X) st j = ((( len X) -' (k + 1)) + n) & (F . n) = ||.((v1 - v0) . j).||

          proof

            let n be Nat;

            assume

             A33: n in ( Seg (k + 1));

            

            then

             A34: ((( len X) -' (k + 1)) + n) = ((( len X) - 1) + 1) by A25, A26, FINSEQ_1: 2, TARSKI:def 1

            .= i;

            take i;

            n = 1 by A25, A33, FINSEQ_1: 2, TARSKI:def 1;

            hence thesis by A34, FINSEQ_1: 40;

          end;

        end;

          suppose k <> 0 ;

          

           A35: ((k + 1) - k) <= (( len X) - k) by A18, XREAL_1: 13;

          

           A36: (( len X) - k) <= (( len X) - 0 ) by XREAL_1: 13;

          (( len X) - k) in NAT by A35, INT_1: 3;

          then (( len X) - k) in ( Seg ( len X)) by A35, A36;

          then

          reconsider k1 = (( len X) - k) as Element of ( dom X) by FINSEQ_1:def 3;

          (Cv0 . k1) = (v0 . k1);

          then

          reconsider Cv0k1 = (Cv0 . k1) as Point of (X . k1);

          k <= (k + 1) by NAT_1: 11;

          then

           A38: k <= ( len X) by A18, XXREAL_0: 2;

          reconsider v2 = (( reproj (k1,v1)) . Cv0k1) as Point of ( product X);

          consider g be Function such that

           A39: v2 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

          

           A40: ( dom g) = ( Seg ( len ( carr X))) by A39, FINSEQ_1:def 3;

          then

          reconsider Cv2 = v2 as FinSequence by A39, FINSEQ_1:def 2;

          

           A41: ( len Cv2) = ( len ( carr X)) by A39, A40, FINSEQ_1:def 3

          .= ( len X) by PRVECT_1:def 11;

          reconsider w12 = (v1 - v2) as Element of ( product ( carr X)) by A3;

          reconsider w02 = (v2 - v0) as Element of ( product ( carr X)) by A3;

          reconsider w10 = (v1 - v0) as Element of ( product ( carr X)) by A3;

           ||.(v2 - v0).|| <= ||.(v1 - v0).||

          proof

            

             A42: ||.(v2 - v0).|| = |.( normsequence (X,w02)).| by A3, PRVECT_2:def 12;

            

             A43: ||.(v1 - v0).|| = |.( normsequence (X,w10)).| by A3, PRVECT_2:def 12;

            

             A44: 0 <= ( Sum ( sqr ( normsequence (X,w02)))) by RVSUM_1: 86;

            for j be Nat st j in ( Seg ( len X)) holds (( sqr ( normsequence (X,w02))) . j) <= (( sqr ( normsequence (X,w10))) . j)

            proof

              let j be Nat;

              assume

               A45: j in ( Seg ( len X));

              reconsider i = j as Element of ( dom X) by A45, FINSEQ_1:def 3;

              

               A46: (( sqr ( normsequence (X,w02))) . j) = ((( normsequence (X,w02)) . j) ^2 ) by VALUED_1: 11

              .= ( ||.((v2 - v0) . i).|| ^2 ) by PRVECT_2:def 11;

              

               A47: (( sqr ( normsequence (X,w10))) . j) = ((( normsequence (X,w10)) . j) ^2 ) by VALUED_1: 11

              .= ( ||.((v1 - v0) . i).|| ^2 ) by PRVECT_2:def 11;

              

               A48: ((v2 - v0) . i) = ((v2 . i) - (v0 . i)) by LOPBAN10: 26;

              

               A49: ((v1 - v0) . i) = ((v1 . i) - (v0 . i)) by LOPBAN10: 26;

               ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).||

              proof

                per cases ;

                  suppose

                   A50: i = k1;

                  (v2 . i) = (v0 . i) by A50, LOPBAN10: 15;

                  then ((v2 . i) - (v0 . i)) = ( 0. (X . i)) by RLVECT_1: 15;

                  hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by A48;

                end;

                  suppose i <> k1;

                  hence ||.((v2 - v0) . i).|| <= ||.((v1 - v0) . i).|| by A48, A49, LOPBAN10: 16;

                end;

              end;

              hence thesis by A46, A47, SQUARE_1: 15;

            end;

            hence thesis by A42, A43, A44, SQUARE_1: 26, RVSUM_1: 82;

          end;

          then

           A51: ||.(v2 - v0).|| <= 1 by A18, XXREAL_0: 2;

          

           A52: (( len X) -' k) = k1 by XREAL_0:def 2;

          ( len (Cv0 | (( len X) -' k))) = k1 by A21, A36, A52, FINSEQ_1: 59;

          then

           A53: ( dom (Cv0 | (( len X) -' k))) = ( Seg k1) by FINSEQ_1:def 3;

          ( len (Cv2 | (( len X) -' k))) = k1 by A36, A41, A52, FINSEQ_1: 59;

          then

           A54: ( dom (Cv2 | (( len X) -' k))) = ( Seg k1) by FINSEQ_1:def 3;

          

           A55: (( len X) -' (k + 1)) = (( len X) - (k + 1)) by A18, XREAL_0:def 2, XREAL_1: 48;

          for j be Nat st j in ( dom (Cv0 | (( len X) -' k))) holds ((Cv0 | (( len X) -' k)) . j) = ((Cv2 | (( len X) -' k)) . j)

          proof

            let j be Nat;

            assume

             A56: j in ( dom (Cv0 | (( len X) -' k)));

            then

             A57: ((Cv0 | (( len X) -' k)) . j) = (Cv0 . j) by FUNCT_1: 47;

            

             A59: 1 <= j & j <= k1 by A53, A56, FINSEQ_1: 1;

            per cases ;

              suppose j = k1;

              then (Cv0 . j) = (Cv2 . j) by LOPBAN10: 15;

              hence ((Cv0 | (( len X) -' k)) . j) = ((Cv2 | (( len X) -' k)) . j) by A53, A54, A56, A57, FUNCT_1: 47;

            end;

              suppose

               A61: j <> k1;

              then j < k1 by A59, XXREAL_0: 1;

              then (j + 1) <= k1 by NAT_1: 13;

              then ((j + 1) - 1) <= (k1 - 1) by XREAL_1: 13;

              then

               A62: j in ( Seg (( len X) -' (k + 1))) by A55, A59;

              j in ( dom X) by A22, A56, RELAT_1: 60, TARSKI:def 3;

              

              then (v2 . j) = (Cv1 . j) by A61, LOPBAN10: 16

              .= ((Cv0 | (( len X) -' (k + 1))) . j) by A18, A62, FUNCT_1: 49

              .= (v0 . j) by A62, FUNCT_1: 49;

              hence ((Cv0 | (( len X) -' k)) . j) = ((Cv2 | (( len X) -' k)) . j) by A53, A54, A56, A57, FUNCT_1: 47;

            end;

          end;

          then

           A63: (Cv0 | (( len X) -' k)) = (Cv2 | (( len X) -' k)) by A53, A54, FINSEQ_1: 13;

          consider F1 be FinSequence of REAL such that

           A64: ( dom F1) = ( Seg k) & ||.((f /. v2) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F1)) & for n be Nat st n in ( Seg k) holds ex i be Element of ( dom X) st i = ((( len X) -' k) + n) & (F1 . n) = ||.((v2 - v0) . i).|| by A17, A38, A51, A63;

           ||.(v1 - v2).|| <= ||.(v1 - v0).||

          proof

            

             A65: ||.(v1 - v2).|| = |.( normsequence (X,w12)).| by A3, PRVECT_2:def 12;

            

             A66: ||.(v1 - v0).|| = |.( normsequence (X,w10)).| by A3, PRVECT_2:def 12;

            

             A67: 0 <= ( Sum ( sqr ( normsequence (X,w12)))) by RVSUM_1: 86;

            for j be Nat st j in ( Seg ( len X)) holds (( sqr ( normsequence (X,w12))) . j) <= (( sqr ( normsequence (X,w10))) . j)

            proof

              let j be Nat;

              assume

               A68: j in ( Seg ( len X));

              reconsider i = j as Element of ( dom X) by A68, FINSEQ_1:def 3;

              

               A69: (( sqr ( normsequence (X,w12))) . j) = ((( normsequence (X,w12)) . j) ^2 ) by VALUED_1: 11

              .= ( ||.((v1 - v2) . i).|| ^2 ) by PRVECT_2:def 11;

              

               A70: (( sqr ( normsequence (X,w10))) . j) = ((( normsequence (X,w10)) . j) ^2 ) by VALUED_1: 11

              .= ( ||.((v1 - v0) . i).|| ^2 ) by PRVECT_2:def 11;

              

               A71: ((v1 - v2) . i) = ((v1 . i) - (v2 . i)) by LOPBAN10: 26;

               ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).||

              proof

                per cases ;

                  suppose i = k1;

                  then (v2 . i) = (v0 . i) by LOPBAN10: 15;

                  hence ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).|| by A71, LOPBAN10: 26;

                end;

                  suppose i <> k1;

                  then (v2 . i) = (v1 . i) by LOPBAN10: 16;

                  then ((v1 . i) - (v2 . i)) = ( 0. (X . i)) by RLVECT_1: 15;

                  hence ||.((v1 - v2) . i).|| <= ||.((v1 - v0) . i).|| by A71;

                end;

              end;

              hence thesis by A69, A70, SQUARE_1: 15;

            end;

            hence thesis by A65, A66, A67, RVSUM_1: 82, SQUARE_1: 26;

          end;

          then

           A74: ||.(v1 - v2).|| <= 1 by A18, XXREAL_0: 2;

          for j be Element of ( dom X) st k1 <> j holds (Cv1 . j) = (Cv2 . j) by LOPBAN10: 16;

          then

           A75: ||.((f /. v1) - (f /. v2)).|| <= (((( ||.v2.|| + 1) |^ ( len X)) * K) * ||.((v1 - v2) . k1).||) by A1, A2, A74, LM02;

          v2 = (v1 + (v2 - v1)) by RLVECT_4: 1;

          then

           A76: ||.v2.|| <= ( ||.v1.|| + ||.(v2 - v1).||) by NORMSP_1:def 1;

           ||.(v2 - v1).|| <= 1 by A74, NORMSP_1: 7;

          then ( ||.v1.|| + ||.(v2 - v1).||) <= ( ||.v1.|| + 1) by XREAL_1: 7;

          then

           A77: ||.v2.|| <= ( ||.v1.|| + 1) by A76, XXREAL_0: 2;

          v1 = ((v1 - v0) + v0) by RLVECT_4: 1;

          then ||.v1.|| <= ( ||.v0.|| + ||.(v1 - v0).||) by NORMSP_1:def 1;

          then

           A78: ||.v1.|| <= ( ||.v0.|| + ||.(v0 - v1).||) by NORMSP_1: 7;

           ||.(v0 - v1).|| <= 1 by A18, NORMSP_1: 7;

          then ( ||.v0.|| + ||.(v0 - v1).||) <= ( ||.v0.|| + 1) by XREAL_1: 7;

          then ||.v1.|| <= ( ||.v0.|| + 1) by A78, XXREAL_0: 2;

          then ( ||.v1.|| + 1) <= (( ||.v0.|| + 1) + 1) by XREAL_1: 7;

          then ||.v2.|| <= ( ||.v0.|| + 2) by A77, XXREAL_0: 2;

          then

           A79: ( ||.v2.|| + 1) <= (( ||.v0.|| + 2) + 1) by XREAL_1: 7;

          

           A80: (( ||.v2.|| + 1) |^ ( len X)) <= (( ||.v0.|| + 3) |^ ( len X)) by A79, PREPOWER: 9;

          

           A81: 0 < (( ||.v2.|| + 1) |^ ( len X)) by PREPOWER: 6;

          ((v1 - v2) . k1) = ((v1 . k1) - (v2 . k1)) by LOPBAN10: 26

          .= ((v1 . k1) - (v0 . k1)) by LOPBAN10: 15

          .= ((v1 - v0) . k1) by LOPBAN10: 26;

          then ((( ||.v2.|| + 1) |^ ( len X)) * (K * ||.((v1 - v2) . k1).||)) <= ((( ||.v0.|| + 3) |^ ( len X)) * (K * ||.((v1 - v0) . k1).||)) by A1, A80, A81, XREAL_1: 66;

          then

           A84: ||.((f /. v1) - (f /. v2)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ||.((v1 - v0) . k1).||) by A75, XXREAL_0: 2;

          set F = ( <* ||.((v1 - v0) . k1).||*> ^ F1);

          ( rng F) c= REAL ;

          then

          reconsider F as FinSequence of REAL by FINSEQ_1:def 4;

          k is Element of NAT by ORDINAL1:def 12;

          then

           A85: ( len F1) = k by A64, FINSEQ_1:def 3;

          ( len F) = (( len F1) + ( len <* ||.((v1 - v0) . k1).||*>)) by FINSEQ_1: 22

          .= (k + 1) by A85, FINSEQ_1: 40;

          then

           A86: ( dom F) = ( Seg (k + 1)) by FINSEQ_1:def 3;

          

           A87: for n be Nat st n in ( Seg (k + 1)) holds ex i be Element of ( dom X) st i = ((( len X) -' (k + 1)) + n) & (F . n) = ||.((v1 - v0) . i).||

          proof

            let n be Nat;

            assume n in ( Seg (k + 1));

            then

             A88: 1 <= n & n <= (k + 1) by FINSEQ_1: 1;

            per cases ;

              suppose

               A89: n = 1;

              

              then

               A90: ((( len X) -' (k + 1)) + n) = ((( len X) - (k + 1)) + 1) by A18, XREAL_0:def 2, XREAL_1: 48

              .= k1;

              take k1;

              thus thesis by A89, A90, FINSEQ_1: 41;

            end;

              suppose n <> 1;

              then 1 < n by A88, XXREAL_0: 1;

              then

               A91: (1 + 1) <= n by NAT_1: 13;

              

               A93: ((( len X) - (k + 1)) + n) <= ((( len X) - (k + 1)) + (k + 1)) by A88, XREAL_1: 7;

              

               A94: ((( len X) - (k + 1)) + 2) <= ((( len X) - (k + 1)) + n) by A91, XREAL_1: 7;

              (1 + 0 ) <= (1 + (( len X) - k)) by A35, XREAL_1: 7;

              then 1 <= ((( len X) -' (k + 1)) + n) by A55, A94, XXREAL_0: 2;

              then ((( len X) -' (k + 1)) + n) in ( Seg ( len X)) by A55, A93;

              then

              reconsider i = ((( len X) -' (k + 1)) + n) as Element of ( dom X) by FINSEQ_1:def 3;

              take i;

              thus i = ((( len X) -' (k + 1)) + n);

              

               A95: (2 - 1) <= (n - 1) by A91, XREAL_1: 9;

              

               A96: (n - 1) <= ((k + 1) - 1) by A88, XREAL_1: 9;

              reconsider n1 = (n - 1) as Element of NAT by A88, INT_1: 3;

              

               A97: n1 in ( Seg k) by A95, A96;

              

               A98: ( len <* ||.((v1 - v0) . k1).||*>) = 1 by FINSEQ_1: 40;

              

               A100: (F . n) = (F . (1 + n1))

              .= (F1 . n1) by A85, A95, A96, A98, FINSEQ_1: 65;

              consider i1 be Element of ( dom X) such that

               A101: i1 = ((( len X) -' k) + n1) & (F1 . n1) = ||.((v2 - v0) . i1).|| by A64, A97;

              

               A102: i1 = ((( len X) - (k + 1)) + n) by A52, A101

              .= i by A18, XREAL_0:def 2, XREAL_1: 48;

              

               A105: (k1 + 0 ) < (k1 + 1) by XREAL_1: 8;

              

               A106: (k1 + 1) <= (k1 + n1) by A95, XREAL_1: 7;

              ((v2 - v0) . i) = ((v2 . i) - (v0 . i)) by LOPBAN10: 26

              .= ((v1 . i) - (v0 . i)) by A52, A101, A102, A105, A106, LOPBAN10: 16

              .= ((v1 - v0) . i) by LOPBAN10: 26;

              hence (F . n) = ||.((v1 - v0) . i).|| by A100, A101, A102;

            end;

          end;

          ((f /. v1) - (f /. v0)) = ((((f /. v1) - (f /. v2)) + (f /. v2)) - (f /. v0)) by RLVECT_4: 1

          .= (((f /. v1) - (f /. v2)) + ((f /. v2) - (f /. v0))) by RLVECT_1: 28;

          then

           A107: ||.((f /. v1) - (f /. v0)).|| <= ( ||.((f /. v1) - (f /. v2)).|| + ||.((f /. v2) - (f /. v0)).||) by NORMSP_1:def 1;

          

           A108: ( ||.((f /. v1) - (f /. v2)).|| + ||.((f /. v2) - (f /. v0)).||) <= ((((( ||.v0.|| + 3) |^ ( len X)) * K) * ||.((v1 - v0) . k1).||) + (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F1))) by A64, A84, XREAL_1: 7;

          ((((( ||.v0.|| + 3) |^ ( len X)) * K) * ||.((v1 - v0) . k1).||) + (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F1))) = (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( ||.((v1 - v0) . k1).|| + ( Sum F1)))

          .= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) by RVSUM_1: 76;

          hence ex F be FinSequence of REAL st ( dom F) = ( Seg (k + 1)) & ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) & for n be Nat st n in ( Seg (k + 1)) holds ex i be Element of ( dom X) st i = ((( len X) -' (k + 1)) + n) & (F . n) = ||.((v1 - v0) . i).|| by A86, A87, A107, A108, XXREAL_0: 2;

        end;

      end;

      

       A109: for n be Nat holds P[n] from NAT_1:sch 2( A6, A16);

      let v1 be Point of ( product X);

      assume

       A110: ||.(v1 - v0).|| <= 1;

      consider g be Function such that

       A111: v1 = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

      ( dom g) = ( Seg ( len ( carr X))) by A111, FINSEQ_1:def 3;

      then

      reconsider Cv1 = v1 as FinSequence by A111, FINSEQ_1:def 2;

      

       A112: (( len X) -' ( len X)) = (( 0 + ( len X)) -' ( len X))

      .= 0 by NAT_D: 34;

      (Cv1 | (( len X) -' ( len X))) = {} by A112

      .= (Cv0 | (( len X) -' ( len X))) by A112;

      then

      consider F be FinSequence of REAL such that

       A113: ( dom F) = ( Seg ( len X)) & ||.((f /. v1) - (f /. v0)).|| <= (((( ||.v0.|| + 3) |^ ( len X)) * K) * ( Sum F)) & for n be Nat st n in ( Seg ( len X)) holds ex i be Element of ( dom X) st i = ((( len X) -' ( len X)) + n) & (F . n) = ||.((v1 - v0) . i).|| by A109, A110;

      for i be Element of ( dom X) holds (F . i) = ||.((v1 - v0) . i).||

      proof

        let i be Element of ( dom X);

        i in ( dom X);

        then

         A116: i in ( Seg ( len X)) by FINSEQ_1:def 3;

        reconsider n = i as Nat;

        consider j be Element of ( dom X) such that

         A117: j = ((( len X) -' ( len X)) + n) & (F . n) = ||.((v1 - v0) . j).|| by A113, A116;

        thus thesis by A112, A117;

      end;

      hence thesis by A113, FINSEQ_1:def 3;

    end;

    theorem :: LOPBAN11:13

    

     NDIFF824: for x be Point of ( product X), r be Real st 0 < r holds ex s be FinSequence of REAL , Y be non empty non-empty FinSequence st ( dom s) = ( dom X) & ( dom Y) = ( dom X) & ( product Y) c= ( Ball (x,r)) & for i be Element of ( dom X) holds 0 < (s . i) & (s . i) < r & (Y . i) = ( Ball ((x . i),(s . i)))

    proof

      let x be Point of ( product X), r be Real;

      assume

       A1: 0 < r;

      

       A2: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      consider s0 be Real such that

       A3: 0 < s0 & s0 < r and

       A4: ( sqrt ((s0 * s0) * ( len X))) < r by A1, NDIFF825;

      set CST = (( len X) |-> s0);

      ( len X) is natural Number & s0 is Element of REAL by XREAL_0:def 1;

      then

      reconsider CST as Element of (( len X) -tuples_on REAL ) by FINSEQ_2: 112;

      

       A5: for i be Element of ( dom X) holds 0 < (CST . i) & (CST . i) < r

      proof

        let i be Element of ( dom X);

        i in ( dom X);

        then i in ( Seg ( len X)) by FINSEQ_1:def 3;

        hence thesis by A3, FINSEQ_2: 57;

      end;

      defpred P1[ object, object] means ex i be Element of ( dom X) st $1 = i & $2 = ( Ball ((x . i),(CST . i)));

      

       A6: for n be Nat st n in ( Seg ( len X)) holds ex d be object st P1[n, d]

      proof

        let n be Nat;

        assume n in ( Seg ( len X));

        then

        reconsider i = n as Element of ( dom X) by FINSEQ_1:def 3;

        set d = ( Ball ((x . i),(CST . i)));

        take d;

        thus thesis;

      end;

      consider Y be FinSequence such that

       A7: ( dom Y) = ( Seg ( len X)) & for n be Nat st n in ( Seg ( len X)) holds P1[n, (Y . n)] from FINSEQ_1:sch 1( A6);

       not {} in ( rng Y)

      proof

        assume {} in ( rng Y);

        then

        consider z be object such that

         A9: z in ( dom Y) & {} = (Y . z) by FUNCT_1:def 3;

        reconsider n = z as Nat by A9;

        consider i be Element of ( dom X) such that

         A10: n = i & (Y . n) = ( Ball ((x . i),(CST . i))) by A7, A9;

         0 < (CST . i) by A5;

        hence contradiction by A9, A10, NDIFF_8: 14;

      end;

      then

      reconsider Y as non empty non-empty FinSequence by A7, FINSEQ_1:def 3, RELAT_1:def 9;

      take CST, Y;

      

      thus ( dom CST) = ( Seg ( len X)) by FUNCT_2:def 1

      .= ( dom X) by FINSEQ_1:def 3;

      thus

       A12: ( dom Y) = ( dom X) by A7, FINSEQ_1:def 3;

      

       A14: for i be Element of ( dom X) holds (Y . i) = ( Ball ((x . i),(CST . i)))

      proof

        let i be Element of ( dom X);

        

         A13: i in ( dom X);

        reconsider n = i as Nat;

        n in ( Seg ( len X)) by A13, FINSEQ_1:def 3;

        then ex i be Element of ( dom X) st n = i & (Y . n) = ( Ball ((x . i),(CST . i))) by A7;

        hence (Y . i) = ( Ball ((x . i),(CST . i)));

      end;

      for z be object st z in ( product Y) holds z in ( Ball (x,r))

      proof

        let z be object;

        assume z in ( product Y);

        then

        consider g be Function such that

         A15: z = g & ( dom g) = ( dom Y) & for i be object st i in ( dom Y) holds (g . i) in (Y . i) by CARD_3:def 5;

        

         A16: ( dom ( carr X)) = ( dom X) by DCARXX;

        

         A17: ( dom g) = ( dom ( carr X)) by A12, A15, DCARXX;

        

         A18: for i0 be object st i0 in ( dom ( carr X)) holds ((g . i0) in (( carr X) . i0) & ex i be Element of ( dom X) st i0 = i & (g . i) in ( Ball ((x . i),(CST . i))) & (g . i) in the carrier of (X . i))

        proof

          let i0 be object;

          assume i0 in ( dom ( carr X));

          then

          reconsider i = i0 as Element of ( dom X) by DCARXX;

          (g . i) in (Y . i) by A12, A15;

          then

           A19: (g . i) in ( Ball ((x . i),(CST . i))) by A14;

          then (g . i) in the carrier of (X . i);

          hence thesis by A19, PRVECT_1:def 11;

        end;

        then

         A20: for i0 be object st i0 in ( dom ( carr X)) holds (g . i0) in (( carr X) . i0);

        then

        reconsider x1 = g as Point of ( product X) by A2, A17, CARD_3:def 5;

        reconsider y1 = g as Element of ( product ( carr X)) by A20, A17, CARD_3:def 5;

        reconsider xx1 = (x - x1) as Element of ( product ( carr X)) by A2;

        

         A21: ||.(x - x1).|| = |.( normsequence (X,xx1)).| by A2, PRVECT_2:def 12;

        

         A22: ( len ( normsequence (X,xx1))) = ( len X) by PRVECT_2:def 11;

        

        then

         A23: ( dom ( normsequence (X,xx1))) = ( Seg ( len X)) by FINSEQ_1:def 3

        .= ( dom X) by FINSEQ_1:def 3;

        now

          let i0 be Nat;

          assume i0 in ( dom ( normsequence (X,xx1)));

          then

          reconsider i = i0 as Element of ( dom X) by A23;

          reconsider xx1i = (xx1 . i) as Point of (X . i);

          reconsider yi = (x . i) as Point of (X . i);

          reconsider y1i = (y1 . i) as Point of (X . i);

          i in ( dom X);

          then

           A24: i in ( Seg ( len X)) by FINSEQ_1:def 3;

          

           A25: (( normsequence (X,xx1)) . i) = ||.xx1i.|| by PRVECT_2:def 11;

          hence 0 <= (( normsequence (X,xx1)) . i0);

          

           A26: (xx1 . i) = ((x . i) - (y1 . i)) by LOPBAN10: 26;

          ex j be Element of ( dom X) st i = j & (g . j) in ( Ball ((x . j),(CST . j))) & (g . j) in the carrier of (X . j) by A16, A18;

          then ex y be Point of (X . i) st y = y1i & ||.((x . i) - y).|| < (CST . i);

          hence (( normsequence (X,xx1)) . i0) <= s0 by A24, A25, A26, FINSEQ_2: 57;

        end;

        then |.( normsequence (X,xx1)).| <= ( sqrt ((s0 * s0) * ( len X))) by A22, NDIFF823;

        then ||.(x - x1).|| < r by A4, A21, XXREAL_0: 2;

        hence z in ( Ball (x,r)) by A15;

      end;

      hence thesis by A5, A14, TARSKI:def 3;

    end;

    theorem :: LOPBAN11:14

    for X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y holds (f is_continuous_on the carrier of ( product X) iff f is_continuous_in ( 0. ( product X))) & (f is_continuous_on the carrier of ( product X) iff f is Lipschitzian)

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace, f be MultilinearOperator of X, Y;

      

       A1: ( dom f) = the carrier of ( product X) by FUNCT_2:def 1;

      

       A2: (f /. ( 0. ( product X))) = ( 0. Y) by FXZER;

      

       A3: ( product X) = NORMSTR (# ( product ( carr X)), ( zeros X), [:( addop X):], [:( multop X):], ( productnorm X) #) by PRVECT_2: 6;

      

       A4: f is_continuous_in ( 0. ( product X)) implies f is Lipschitzian

      proof

        assume f is_continuous_in ( 0. ( product X));

        then

        consider s be Real such that

         A5: 0 < s & for z be Point of ( product X) st z in ( dom f) & ||.(z - ( 0. ( product X))).|| < s holds ||.((f /. z) - (f /. ( 0. ( product X)))).|| < 1 by NFCONT_1: 7;

        set z = ( 0. ( product X));

        consider s1 be FinSequence of REAL , Balls be non empty non-empty FinSequence such that

         A6: ( dom s1) = ( dom X) & ( dom X) = ( dom Balls) & ( product Balls) c= ( Ball (( 0. ( product X)),s)) & for i be Element of ( dom X) holds 0 < (s1 . i) & (s1 . i) < s & (Balls . i) = ( Ball ((z . i),(s1 . i))) by A5, NDIFF824;

        defpred P1[ object, object] means ex i be Element of ( dom X) st $1 = i & $2 = ((s1 . i) / 2);

        

         A7: for n be Nat st n in ( Seg ( len X)) holds ex d be Element of REAL st P1[n, d]

        proof

          let n be Nat;

          assume n in ( Seg ( len X));

          then

          reconsider i = n as Element of ( dom X) by FINSEQ_1:def 3;

          reconsider si = ((s1 . i) / 2) as Element of REAL by XREAL_0:def 1;

          take si;

          thus P1[n, si];

        end;

        consider s2 be FinSequence of REAL such that

         A8: ( len s2) = ( len X) & for n be Nat st n in ( Seg ( len X)) holds P1[n, (s2 /. n)] from FINSEQ_4:sch 1( A7);

        

         A9: ( dom s2) = ( Seg ( len X)) by A8, FINSEQ_1:def 3

        .= ( dom X) by FINSEQ_1:def 3;

        

         A11: for i be Element of ( dom X) holds (s2 . i) = ((s1 . i) / 2)

        proof

          let i be Element of ( dom X);

          i in ( dom X);

          then i in ( Seg ( len X)) by FINSEQ_1:def 3;

          then ex j be Element of ( dom X) st i = j & (s2 /. i) = ((s1 . j) / 2) by A8;

          hence (s2 . i) = ((s1 . i) / 2) by A9, PARTFUN1:def 6;

        end;

        

         A12: for i be Element of ( dom X) holds 0 < (s2 . i) & (s2 . i) < (s1 . i)

        proof

          let i be Element of ( dom X);

          (s2 . i) = ((s1 . i) / 2) & 0 < (s1 . i) by A6, A11;

          hence 0 < (s2 . i) & (s2 . i) < (s1 . i) by XREAL_1: 216;

        end;

        ( dom s2) = ( Seg ( len X)) by A9, FINSEQ_1:def 3;

        then

         A13: ( len s2) = ( len X) by FINSEQ_1:def 3;

         A14:

        now

          let x be Point of ( product X);

          assume

           A15: for i be Element of ( dom X) holds ||.(x . i).|| <= (s2 . i);

          ex g be Function st x = g & ( dom g) = ( dom ( carr X)) & for i be object st i in ( dom ( carr X)) holds (g . i) in (( carr X) . i) by A3, CARD_3:def 5;

          then

           A16: ( dom x) = ( dom X) by DCARXX;

          now

            let i0 be object;

            assume i0 in ( dom X);

            then

            reconsider i = i0 as Element of ( dom X);

            

             A18: (z . i) = ( 0. (X . i)) by ZERXI;

             ||.((x . i) - ( 0. (X . i))).|| <= (s2 . i) by A15;

            then

             A19: ||.(( 0. (X . i)) - (x . i)).|| <= (s2 . i) by NORMSP_1: 7;

            (s2 . i) = ((s1 . i) / 2) & 0 < (s1 . i) by A6, A11;

            then 0 < (s2 . i) & (s2 . i) < (s1 . i) by XREAL_1: 216;

            then ||.(( 0. (X . i)) - (x . i)).|| < (s1 . i) by A19, XXREAL_0: 2;

            then (x . i) in ( Ball (( 0. (X . i)),(s1 . i)));

            hence (x . i0) in (Balls . i0) by A6, A18;

          end;

          then x in ( product Balls) by A6, A16, CARD_3:def 5;

          then x in ( Ball (( 0. ( product X)),s)) by A6;

          then ex p be Point of ( product X) st x = p & ||.(( 0. ( product X)) - p).|| < s;

          then

           A20: ||.(x - ( 0. ( product X))).|| < s by NORMSP_1: 7;

           ||.((f /. x) - (f /. ( 0. ( product X)))).|| < 1 by A1, A5, A20;

          hence ||.(f /. x).|| < 1 by A2;

        end;

        

         A21: 0 < ( Product s2) by A9, A12, PSPROD;

        set K = (1 / ( Product s2));

        now

          let x be Point of ( product X);

          consider F be FinSequence of REAL such that

           A23: ( dom F) = ( dom X) & (for i be Element of ( dom X) holds (F . i) = ||.(x . i).||) & ( NrProduct x) = ( Product F) by LOPBAN10:def 9;

          thus ||.(f . x).|| <= (K * ( NrProduct x))

          proof

            per cases ;

              suppose

               A24: for i be Element of ( dom X) holds (x . i) <> ( 0. (X . i));

              then

               A25: 0 < ( NrProduct x) by LOPBAN10: 27;

              consider d be FinSequence of REAL such that

               A26: ( dom d) = ( dom X) & for i be Element of ( dom X) holds (d . i) = ( ||.(x . i).|| " ) by LOPBAN10: 37;

              ( dom d) = ( Seg ( len X)) by A26, FINSEQ_1:def 3;

              then

               A27: ( len d) = ( len X) by FINSEQ_1:def 3;

              set F1 = ( mlt (s2,d));

              

               A28: for i be Element of ( dom F) holds (d . i) = ((F . i) " )

              proof

                let i be Element of ( dom F);

                reconsider j = i as Element of ( dom X) by A23;

                (d . j) = ( ||.(x . j).|| " ) by A26;

                hence thesis by A23;

              end;

              

               A32: ( dom F1) = (( dom X) /\ ( dom X)) by A9, A26, VALUED_1:def 4

              .= ( dom X);

              s2 is Element of (( len X) -tuples_on REAL ) & d is Element of (( len X) -tuples_on REAL ) by A13, A27, FINSEQ_2: 92;

              

              then

               A33: ( Product F1) = (( Product s2) * ( Product d)) by RVSUM_1: 107

              .= (( Product s2) * (( Product F) " )) by A23, A26, LOPBAN10: 40, A28;

              consider x1 be Element of ( product X) such that

               A34: for i be Element of ( dom X) holds (x1 . i) = ((F1 /. i) * (x . i)) by LOPBAN10: 38;

              

               A35: for i be Element of ( dom X) holds ||.(x1 . i).|| <= (s2 . i)

              proof

                let i be Element of ( dom X);

                

                 A36: (x1 . i) = ((F1 /. i) * (x . i)) by A34;

                

                 A37: (F1 /. i) = (F1 . i) by A32, PARTFUN1:def 6

                .= ((s2 . i) * (d . i)) by RVSUM_1: 60

                .= ((s2 . i) * ((F . i) " )) by A23, A28;

                

                 A39: (x1 . i) = (((s2 . i) * ( ||.(x . i).|| " )) * (x . i)) by A23, A36, A37;

                

                 A41: 0 <= (s2 . i) by A12;

                

                 A42: |.((s2 . i) * ( ||.(x . i).|| " )).| = ((s2 . i) * ( ||.(x . i).|| " )) by A41, COMPLEX1: 43;

                (x . i) <> ( 0. (X . i)) by A24;

                then

                 A43: ||.(x . i).|| <> 0 by NORMSP_0:def 5;

                 ||.(x1 . i).|| = (((s2 . i) * ( ||.(x . i).|| " )) * ||.(x . i).||) by A39, A42, NORMSP_1:def 1

                .= ((s2 . i) * (( ||.(x . i).|| " ) * ||.(x . i).||))

                .= ((s2 . i) * 1) by A43, XCMPLX_0:def 7;

                hence thesis;

              end;

              

               A44: ||.(f /. x1).|| < 1 by A14, A35;

              

               A45: |.(( Product F) " ).| = (( Product F) " ) by A23, ABSVALUE:def 1;

              

               A46: |.(( Product s2) * (( Product F) " )).| = ( |.( Product s2).| * |.(( Product F) " ).|) by COMPLEX1: 65

              .= (( Product s2) * (( Product F) " )) by A21, A45, COMPLEX1: 43;

              (f . x1) = ((( Product s2) * (( Product F) " )) * (f . x)) by A32, A33, A34, LOPBAN10: 39;

              then ||.(f . x1).|| = ((( Product s2) * (( Product F) " )) * ||.(f . x).||) by A46, NORMSP_1:def 1;

              then ((( Product s2) * ((( Product F) " ) * ||.(f . x).||)) / ( Product s2)) < (1 / ( Product s2)) by A21, A44, XREAL_1: 74;

              then ((( Product F) " ) * ||.(f . x).||) < K by A21, XCMPLX_1: 89;

              then (( Product F) * ((( Product F) " ) * ||.(f . x).||)) < (K * ( Product F)) by A23, A25, XREAL_1: 68;

              then ((( Product F) * (( Product F) " )) * ||.(f . x).||) < (K * ( Product F));

              then (1 * ||.(f . x).||) < (K * ( Product F)) by A23, A25, XCMPLX_0:def 7;

              hence ||.(f . x).|| <= (K * ( NrProduct x)) by A23;

            end;

              suppose

               A47: ex i be Element of ( dom X) st (x . i) = ( 0. (X . i));

              then

               A48: (f . x) = ( 0. Y) by LOPBAN10: 36;

              consider i be Element of ( dom X) such that

               A49: (x . i) = ( 0. (X . i)) by A47;

              

               A50: (F . i) = ||.(x . i).|| by A23;

              (F . i) = 0 by A49, A50;

              then ( Product F) = 0 by A23, RVSUM_1: 103;

              hence ||.(f . x).|| <= (K * ( NrProduct x)) by A23, A48;

            end;

          end;

        end;

        hence f is Lipschitzian by A21;

      end;

      f is Lipschitzian implies f is_continuous_on the carrier of ( product X)

      proof

        assume f is Lipschitzian;

        then

        consider K be Real such that

         A52: 0 <= K and

         A53: for x be Point of ( product X) holds ||.(f . x).|| <= (K * ( NrProduct x));

        for v0 be Point of ( product X) holds for r be Real st v0 in the carrier of ( product X) & 0 < r holds ex s be Real st 0 < s & for v1 be Point of ( product X) st v1 in the carrier of ( product X) & ||.(v1 - v0).|| < s holds ||.((f /. v1) - (f /. v0)).|| < r

        proof

          let v0 be Point of ( product X), r0 be Real;

          assume

           A54: v0 in the carrier of ( product X) & 0 < r0;

          set r = (r0 / 2);

          

           A58: 0 < r & r < r0 by A54, XREAL_1: 216;

          set L = ( ||.v0.|| + 1);

          consider M be Real such that

           A59: 0 <= M & for v1 be Point of ( product X) st ||.(v1 - v0).|| <= 1 holds ex F be FinSequence of REAL st ( dom F) = ( dom X) & ||.((f /. v1) - (f /. v0)).|| <= ((M * K) * ( Sum F)) & for i be Element of ( dom X) holds (F . i) = ||.((v1 - v0) . i).|| by A52, A53, LM01;

          set BL = (((M * K) * ( len X)) + 1);

          set s = ( min ((r / BL),1));

          

           A64: 0 < s & s <= 1 & s <= (r / BL) by A52, A54, A59, XXREAL_0: 17, XXREAL_0: 21;

          ( 0 + ((M * K) * ( len X))) <= BL by XREAL_1: 7;

          then (((M * K) * ( len X)) * s) <= ((r / BL) * BL) by A52, A59, A64, XREAL_1: 66;

          then

           A65: (((M * K) * ( len X)) * s) <= r by A52, A59, XCMPLX_1: 87;

          take s;

          thus 0 < s by A52, A54, A59, XXREAL_0: 21;

          let v1 be Point of ( product X);

          assume

           A66: v1 in the carrier of ( product X) & ||.(v1 - v0).|| < s;

          reconsider w1 = (v1 - v0) as Element of ( product X);

          consider H be FinSequence of REAL such that

           A67: ( dom H) = ( dom X) & ||.((f /. v1) - (f /. v0)).|| <= ((M * K) * ( Sum H)) & for i be Element of ( dom X) holds (H . i) = ||.(w1 . i).|| by A59, A64, A66, XXREAL_0: 2;

          for i be Nat st i in ( dom H) holds 0 <= (H . i)

          proof

            let i be Nat;

            assume i in ( dom H);

            then

            reconsider j = i as Element of ( dom X) by A67;

            (H . j) = ||.(w1 . j).|| by A67;

            hence thesis;

          end;

          then

           A68: 0 <= ( Sum H) by RVSUM_1: 84;

          

           A69: for i be Element of ( dom X) holds ||.(w1 . i).|| < s

          proof

            let i be Element of ( dom X);

             ||.(w1 . i).|| <= ||.(v1 - v0).|| by A3, PRVECT_2: 10;

            hence ||.(w1 . i).|| < s by A66, XXREAL_0: 2;

          end;

          set CST = (( len H) |-> s);

          

           A71: H is Element of (( len H) -tuples_on REAL ) by FINSEQ_2: 92;

          ( len H) is natural Number & s is Element of REAL by XREAL_0:def 1;

          then

          reconsider CST as Element of (( len H) -tuples_on REAL ) by FINSEQ_2: 112;

          ( dom H) = ( Seg ( len X)) by A67, FINSEQ_1:def 3;

          then

           A72: ( len H) = ( len X) by FINSEQ_1:def 3;

          for i be Nat st i in ( Seg ( len H)) holds (H . i) <= (CST . i)

          proof

            let i0 be Nat;

            assume

             A73: i0 in ( Seg ( len H));

            then

            reconsider i = i0 as Element of ( dom X) by A67, FINSEQ_1:def 3;

            

             A74: ||.(w1 . i).|| < s by A69;

            (H . i) <= s by A67, A74;

            hence thesis by A73, FINSEQ_2: 57;

          end;

          then ( Sum H) <= ( Sum CST) by A71, RVSUM_1: 82;

          then ( Sum H) <= (s * ( len X)) by A72, RVSUM_1: 80;

          then ((M * K) * ( Sum H)) <= ((M * K) * (s * ( len X))) by A52, A59, A68, XREAL_1: 66;

          then ||.((f /. v1) - (f /. v0)).|| <= ((M * K) * (s * ( len X))) by A67, XXREAL_0: 2;

          then ||.((f /. v1) - (f /. v0)).|| <= r by A65, XXREAL_0: 2;

          hence ||.((f /. v1) - (f /. v0)).|| < r0 by A58, XXREAL_0: 2;

        end;

        hence f is_continuous_on the carrier of ( product X) by A1, NFCONT_1: 19;

      end;

      hence thesis by A4;

    end;