lopban10.miz



    begin

    definition

      let X be non empty non-empty FinSequence;

      let i be object;

      let x be Element of ( product X);

      :: LOPBAN10:def1

      func reproj (i,x) -> Function of (X . i), ( product X) means

      : Def1: for r be object st r in (X . i) holds (it . r) = (x +* (i,r));

      existence

      proof

        deffunc H1( object) = (x +* (i,$1));

        

         A1: for r be object st r in (X . i) holds H1(r) in ( product X)

        proof

          let r be object;

          assume

           A2: r in (X . i);

          per cases ;

            suppose not i in ( dom x);

            then H1(r) = x by FUNCT_7:def 3;

            hence H1(r) in ( product X);

          end;

            suppose

             A4: i in ( dom x);

            consider g be Function such that

             A5: x = g & ( dom g) = ( dom X) & for j be object st j in ( dom X) holds (g . j) in (X . j) by CARD_3:def 5;

            

             A6: ( dom H1(r)) = ( dom X) by A5, FUNCT_7: 30;

            for j be object st j in ( dom X) holds ( H1(r) . j) in (X . j)

            proof

              let j be object;

              assume

               A7: j in ( dom X);

              per cases ;

                suppose j = i;

                hence ( H1(r) . j) in (X . j) by A2, A4, FUNCT_7: 31;

              end;

                suppose j <> i;

                then ( H1(r) . j) = (x . j) by FUNCT_7: 32;

                hence ( H1(r) . j) in (X . j) by A5, A7;

              end;

            end;

            hence H1(r) in ( product X) by A6, CARD_3:def 5;

          end;

        end;

        consider f be Function of (X . i), ( product X) such that

         A9: for r be object st r in (X . i) holds (f . r) = H1(r) from FUNCT_2:sch 2( A1);

        take f;

        thus thesis by A9;

      end;

      uniqueness

      proof

        let f,g be Function of (X . i), ( product X);

        assume that

         A10: for r be object st r in (X . i) holds (f . r) = (x +* (i,r)) and

         A11: for r be object st r in (X . i) holds (g . r) = (x +* (i,r));

        now

          let r be object;

          assume

           A12: r in (X . i);

          

          hence (f . r) = (x +* (i,r)) by A10

          .= (g . r) by A11, A12;

        end;

        hence f = g by FUNCT_2: 12;

      end;

    end

    theorem :: LOPBAN10:1

    

     Th1: for X be non empty non-empty FinSequence, x be Element of ( product X), i be Element of ( dom X), r be object st r in (X . i) holds ((( reproj (i,x)) . r) . i) = r

    proof

      let X be non empty non-empty FinSequence, x be Element of ( product X), i be Element of ( dom X), r be object;

      assume r in (X . i);

      then

       A1: (( reproj (i,x)) . r) = (x +* (i,r)) by Def1;

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

      hence ((( reproj (i,x)) . r) . i) = r by A1, FUNCT_7: 31;

    end;

    theorem :: LOPBAN10:2

    

     Th2: for X be non empty non-empty FinSequence, x be Element of ( product X), i,j be Element of ( dom X), r be object st r in (X . i) & i <> j holds ((( reproj (i,x)) . r) . j) = (x . j)

    proof

      let X be non empty non-empty FinSequence, x be Element of ( product X), i,j be Element of ( dom X), r be object;

      assume

       A1: r in (X . i) & i <> j;

      then (( reproj (i,x)) . r) = (x +* (i,r)) by Def1;

      hence thesis by A1, FUNCT_7: 32;

    end;

    theorem :: LOPBAN10:3

    

     Th2X: for X be non empty non-empty FinSequence, x be Element of ( product X), i be Element of ( dom X) holds (( reproj (i,x)) . (x . i)) = x

    proof

      let X be non empty non-empty FinSequence, x be Element of ( product X), i be Element of ( dom X);

      (( reproj (i,x)) . (x . i)) = (x +* (i,(x . i))) by Def1;

      hence (( reproj (i,x)) . (x . i)) = x by FUNCT_7: 35;

    end;

    definition

      let X be RealLinearSpace-Sequence;

      let i be Element of ( dom X);

      let x be Element of ( product X);

      :: LOPBAN10:def2

      func reproj (i,x) -> Function of (X . i), ( product X) means

      : Def20: ex x0 be Element of ( product ( carr X)) st x0 = x & it = ( reproj (i,x0));

      existence

      proof

        reconsider x0 = x as Element of ( product ( carr X));

        

         A1: ( reproj (i,x0)) is Function of (( carr X) . i), ( product ( carr X));

        (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

        hence thesis by A1;

      end;

      uniqueness ;

    end

    

     LemmaX: for X be RealLinearSpace-Sequence holds ( dom ( carr X)) = ( dom X)

    proof

      let X be RealLinearSpace-Sequence;

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

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

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

      hence thesis;

    end;

    theorem :: LOPBAN10:4

    

     Th3: for X be RealLinearSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F be Function st F = (( reproj (i,x)) . r) holds (F . i) = r

    proof

      let X be RealLinearSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F be Function;

      assume

       A1: F = (( reproj (i,x)) . r);

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      

       A3: (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def20;

      thus (F . i) = r by A1, A2, A3, A4, Th1;

    end;

    theorem :: LOPBAN10:5

    

     Th4: for X be RealLinearSpace-Sequence, i,j be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F,s be Function st F = (( reproj (i,x)) . r) & x = s & i <> j holds (F . j) = (s . j)

    proof

      let X be RealLinearSpace-Sequence, i,j be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F,s be Function;

      assume

       A1: F = (( reproj (i,x)) . r) & x = s & i <> j;

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      

       A3: (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def20;

      thus (F . j) = (s . j) by A1, A2, A3, A4, Th2;

    end;

    theorem :: LOPBAN10:6

    

     Th4X: for X be RealLinearSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), s be Function st x = s holds (( reproj (i,x)) . (s . i)) = x

    proof

      let X be RealLinearSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), s be Function;

      assume

       A1: x = s;

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def20;

      thus (( reproj (i,x)) . (s . i)) = x by A1, A2, A4, Th2X;

    end;

    definition

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace, f be Function of ( product X), Y;

      :: LOPBAN10:def3

      attr f is Multilinear means

      : Def3: for i be Element of ( dom X), x be Element of ( product X) holds (f * ( reproj (i,x))) is LinearOperator of (X . i), Y;

    end

    registration

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      cluster Multilinear for Function of ( product X), Y;

      correctness

      proof

        set g = (the carrier of ( product X) --> ( 0. Y));

        take g;

        now

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

          set F = (g * ( reproj (i,x)));

          for z be object st z in ( dom F) holds (F . z) = ( 0. Y)

          proof

            let z be object;

            assume z in ( dom F);

            then

             A2: z in the carrier of (X . i) by FUNCT_2:def 1;

            

            thus (F . z) = (g . (( reproj (i,x)) . z)) by A2, FUNCT_2: 15

            .= ( 0. Y) by A2, FUNCOP_1: 7, FUNCT_2: 5;

          end;

          then F = (( dom F) --> ( 0. Y)) by FUNCOP_1: 11;

          then

           A4: F = (the carrier of (X . i) --> ( 0. Y)) by FUNCT_2:def 1;

          reconsider f = (g * ( reproj (i,x))) as Function of the carrier of (X . i), Y;

           A5:

          now

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

            

            thus (f . (x + y)) = (( 0. Y) + ( 0. Y)) by A4, FUNCOP_1: 7

            .= ((f . x) + ( 0. Y)) by A4, FUNCOP_1: 7

            .= ((f . x) + (f . y)) by A4, FUNCOP_1: 7;

          end;

          now

            let x be VECTOR of (X . i);

            let r be Real;

            

            thus (f . (r * x)) = (r * ( 0. Y)) by A4, FUNCOP_1: 7

            .= (r * (f . x)) by A4, FUNCOP_1: 7;

          end;

          hence (g * ( reproj (i,x))) is LinearOperator of (X . i), Y by A5, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

        hence g is Multilinear;

      end;

    end

    definition

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      mode MultilinearOperator of X,Y is Multilinear Function of ( product X), Y;

    end

    theorem :: LOPBAN10:7

    

     LOPBAN73: for X,Y be RealLinearSpace holds for f be LinearOperator of X, Y holds ( 0. Y) = (f . ( 0. X))

    proof

      let X,Y be RealLinearSpace;

      let f be LinearOperator of X, Y;

      ((f /. ( 0. X)) + ( 0. Y)) = (f /. (( 0. X) + ( 0. X)))

      .= ((f /. ( 0. X)) + (f /. ( 0. X))) by VECTSP_1:def 20;

      hence ( 0. Y) = (f . ( 0. X)) by RLVECT_1: 8;

    end;

    theorem :: LOPBAN10:8

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace, g be MultilinearOperator of X, Y, t be Point of ( product X), s be Element of ( product ( carr X)) st s = t & ex i be Element of ( dom X) st (s . i) = ( 0. (X . i)) holds (g . t) = ( 0. Y)

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace, g be MultilinearOperator of X, Y, t be Point of ( product X), s be Element of ( product ( carr X));

      assume that

       A1: s = t and

       A2: ex i be Element of ( dom X) st (s . i) = ( 0. (X . i));

      consider i be Element of ( dom X) such that

       A3: (s . i) = ( 0. (X . i)) by A2;

      

       A7: ((g * ( reproj (i,t))) . ( 0. (X . i))) = (g . (( reproj (i,t)) . ( 0. (X . i)))) by FUNCT_2: 15

      .= (g . t) by A1, A3, Th4X;

      (g * ( reproj (i,t))) is LinearOperator of (X . i), Y by Def3;

      hence (g . t) = ( 0. Y) by A7, LOPBAN73;

    end;

    theorem :: LOPBAN10:9

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace, g be MultilinearOperator of X, Y, a be FinSequence of REAL st ( dom a) = ( dom X) holds for t,t1 be Point of ( product X), s,s1 be Element of ( product ( carr X)) st t = s & t1 = s1 & for i be Element of ( dom X) holds (s1 . i) = ((a /. i) * (s . i)) holds (g . t1) = (( Product a) * (g . t))

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace, g be MultilinearOperator of X, Y, a be FinSequence of REAL ;

      assume

       A1: ( dom a) = ( dom X);

      

       A4: ( dom ( carr X)) = ( dom X) by LemmaX;

      defpred P[ Nat] means for t,t1 be Point of ( product X), s,s1 be Element of ( product ( carr X)), b be FinSequence of REAL st t = s & t1 = s1 & b = (a | $1) & $1 <= ( len a) & (for i be Element of ( dom X) holds ((i in ( Seg $1) implies (s1 . i) = ((a /. i) * (s . i))) & ( not i in ( Seg $1) implies (s1 . i) = (s . i)))) holds (g . t1) = (( Product b) * (g . t));

      

       A6: P[ 0 ]

      proof

        let t,t1 be Point of ( product X), s,s1 be Element of ( product ( carr X)), b be FinSequence of REAL ;

        assume

         A7: t = s & t1 = s1 & b = (a | 0 ) & 0 <= ( len a) & for i be Element of ( dom X) holds ((i in ( Seg 0 ) implies (s1 . i) = ((a /. i) * (s . i))) & ( not i in ( Seg 0 ) implies (s1 . i) = (s . i)));

        

         A10: ex g be Function st s1 = g & ( dom g) = ( dom ( carr X)) & for y be object st y in ( dom ( carr X)) holds (g . y) in (( carr X) . y) by CARD_3:def 5;

        

         A11: ex g be Function st s = g & ( dom g) = ( dom ( carr X)) & for y be object st y in ( dom ( carr X)) holds (g . y) in (( carr X) . y) by CARD_3:def 5;

        s1 = s by A4, A7, A10, A11;

        hence (g . t1) = (( Product b) * (g . t)) by A7, RVSUM_1: 94, RLVECT_1:def 8;

      end;

      

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

      proof

        let k be Nat;

        assume

         A17: P[k];

        let t,t1 be Point of ( product X), s,s1 be Element of ( product ( carr X)), b be FinSequence of REAL ;

        assume

         A18: t = s & t1 = s1 & b = (a | (k + 1)) & (k + 1) <= ( len a) & for i be Element of ( dom X) holds ((i in ( Seg (k + 1)) implies (s1 . i) = ((a /. i) * (s . i))) & ( not i in ( Seg (k + 1)) implies (s1 . i) = (s . i)));

        reconsider b2 = (a | k) as FinSequence of REAL ;

        

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

        1 <= (k + 1) & (k + 1) <= ( len a) by A18, NAT_1: 11;

        then

         B20: (k + 1) in ( Seg ( len a));

        then

         A21: (k + 1) in ( dom a) by FINSEQ_1:def 3;

        

         A23: b2 = (b | k) by A18, FINSEQ_1: 82, NAT_1: 11;

        

         A25: b = (b2 ^ <*(b . (k + 1))*>) by A18, A23, FINSEQ_1: 59, FINSEQ_3: 55

        .= (b2 ^ <*(a . (k + 1))*>) by A18, FINSEQ_1: 4, FUNCT_1: 49

        .= (b2 ^ <*(a /. (k + 1))*>) by A21, PARTFUN1:def 6;

        defpred LP1[ object] means $1 in ( Seg k);

        deffunc F1( Element of ( dom X)) = ((a /. $1) * (s . $1));

        deffunc F2( Element of ( dom X)) = (s . $1);

        consider s2 be Function such that

         A26: ( dom s2) = ( dom X) & for i be Element of ( dom X) holds ( LP1[i] implies (s2 . i) = F1(i)) & ( not LP1[i] implies (s2 . i) = F2(i)) from PARTFUN1:sch 4;

        for y be object st y in ( dom ( carr X)) holds (s2 . y) in (( carr X) . y)

        proof

          let y be object;

          assume y in ( dom ( carr X));

          then

          reconsider i = y as Element of ( dom X) by LemmaX;

          per cases ;

            suppose LP1[i];

            then (s2 . y) = ((a /. i) * (s . i)) by A26;

            then (s2 . y) in the carrier of (X . i);

            hence (s2 . y) in (( carr X) . y) by PRVECT_1:def 11;

          end;

            suppose not LP1[i];

            then (s2 . y) = (s . i) by A26;

            then (s2 . y) in the carrier of (X . i);

            hence (s2 . y) in (( carr X) . y) by PRVECT_1:def 11;

          end;

        end;

        then

        reconsider s2 as Element of ( product ( carr X)) by A4, A26, CARD_3:def 5;

        reconsider t2 = s2 as Point of ( product X);

        reconsider k1 = (k + 1) as Element of ( dom X) by A1, B20, FINSEQ_1:def 3;

        (k + 0 ) < (k + 1) by XREAL_1: 8;

        then not k1 in ( Seg k) by FINSEQ_1: 1;

        then

         A30: (s2 . k1) = (s . k1) by A26;

        

         A31: (g * ( reproj (k1,t2))) is LinearOperator of (X . k1), Y by Def3;

        set RK = (( reproj (k1,t2)) . ((a /. k1) * (s . k1)));

        

         A32: ex g be Function st s1 = g & ( dom g) = ( dom ( carr X)) & for y be object st y in ( dom ( carr X)) holds (g . y) in (( carr X) . y) by CARD_3:def 5;

        

         A33: ex g be Function st RK = g & ( dom g) = ( dom ( carr X)) & for y be object st y in ( dom ( carr X)) holds (g . y) in (( carr X) . y) by CARD_3:def 5;

        reconsider RK as Function;

        

         A51: for x be object st x in ( dom s1) holds (s1 . x) = (RK . x)

        proof

          let x be object;

          assume x in ( dom s1);

          then

          reconsider i = x as Element of ( dom X) by LemmaX, A32;

          

           A38: (i in ( Seg k) implies (s2 . i) = ((a /. i) * (s . i))) & ( not i in ( Seg k) implies (s2 . i) = (s . i)) by A26;

          

           A40: i <> k1 implies (RK . i) = (s2 . i) by Th4;

          per cases ;

            suppose

             A41: i in ( Seg (k + 1));

            then

             A42: (s1 . i) = ((a /. i) * (s . i)) by A18;

            per cases ;

              suppose

               A43: i = (k + 1);

              

              then (RK . i) = ((a /. k1) * (s . k1)) by Th3

              .= (s1 . i) by A18, A41, A43;

              hence (s1 . x) = (RK . x);

            end;

              suppose

               A44: i <> (k + 1);

              1 <= i & i <= (k + 1) by A41, FINSEQ_1: 1;

              then 1 <= i & i < (k + 1) by A44, XXREAL_0: 1;

              then 1 <= i & i <= k by NAT_1: 13;

              hence (s1 . x) = (RK . x) by A38, A42, A44, Th4;

            end;

          end;

            suppose

             A46: not i in ( Seg (k + 1));

            i in ( dom X);

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

            then

             A47: 1 <= i & i <= ( len X) by FINSEQ_1: 1;

            

             A49: (k + 1) < i by A46, A47;

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

            then k < i by A49, XXREAL_0: 2;

            hence (s1 . x) = (RK . x) by A18, A38, A40, A46, A47, FINSEQ_1: 1;

          end;

        end;

        

         A54: (g . t1) = (g . (( reproj (k1,t2)) . ((a /. k1) * (s . k1)))) by A18, A32, A33, A51, FUNCT_1: 2

        .= ((g * ( reproj (k1,t2))) . ((a /. k1) * (s . k1))) by FUNCT_2: 15

        .= ((a /. k1) * ((g * ( reproj (k1,t2))) . (s . k1))) by A31, LOPBAN_1:def 5

        .= ((a /. (k + 1)) * (g . (( reproj (k1,t2)) . (s . k1)))) by FUNCT_2: 15

        .= ((a /. (k + 1)) * (g . t2)) by A30, Th4X;

        

        thus (g . t1) = ((a /. (k + 1)) * (( Product b2) * (g . t))) by A17, A18, A19, A26, A54, XXREAL_0: 2

        .= (((a /. (k + 1)) * ( Product b2)) * (g . t)) by RLVECT_1:def 7

        .= (( Product b) * (g . t)) by A25, RVSUM_1: 96;

      end;

      

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

      let t,t1 be Point of ( product X), s,s1 be Element of ( product ( carr X));

      assume

       A56: t = s & t1 = s1 & for i be Element of ( dom X) holds (s1 . i) = ((a /. i) * (s . i));

      set b = (a | ( len a));

      

       A57: b = a & ( len a) <= ( len a) by FINSEQ_2: 20;

      for i be Element of ( dom X) holds (i in ( Seg ( len a)) implies (s1 . i) = ((a /. i) * (s . i))) & ( not i in ( Seg ( len a)) implies (s1 . i) = (s . i))

      proof

        let i be Element of ( dom X);

        thus i in ( Seg ( len a)) implies (s1 . i) = ((a /. i) * (s . i)) by A56;

        thus not (i in ( Seg ( len a))) implies (s1 . i) = (s . i)

        proof

          assume not i in ( Seg ( len a));

          then not i in ( dom X) by A1, FINSEQ_1:def 3;

          hence (s1 . i) = (s . i);

        end;

      end;

      hence (g . t1) = (( Product a) * (g . t)) by A55, A56, A57;

    end;

    definition

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      :: LOPBAN10:def4

      func MultilinearOperators (X,Y) -> Subset of ( RealVectSpace (the carrier of ( product X),Y)) means

      : Def6: for x be set holds x in it iff x is MultilinearOperator of X, Y;

      existence

      proof

        defpred P[ object] means $1 is MultilinearOperator of X, Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( Funcs (the carrier of ( product X),the carrier of Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( Funcs (the carrier of ( product X),the carrier of Y)) by A1;

        hence IT is Subset of ( RealVectSpace (the carrier of ( product X),Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is MultilinearOperator of X, Y by A1;

        assume

         A2: x is MultilinearOperator of X, Y;

        then x in ( Funcs (the carrier of ( product X),the carrier of Y)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( RealVectSpace (the carrier of ( product X),Y));

        assume that

         A3: for x be set holds x in X1 iff x is MultilinearOperator of X, Y and

         A4: for x be set holds x in X2 iff x is MultilinearOperator of X, Y;

        

         A5: X2 c= X1

        proof

          let x be object;

          assume x in X2;

          then x is MultilinearOperator of X, Y by A4;

          hence thesis by A3;

        end;

        X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x is MultilinearOperator of X, Y by A3;

          hence thesis by A4;

        end;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

    end

    

     LM14: for X be RealLinearSpace, x1,x2,x3,x4 be Point of X holds ((x1 + x2) + (x3 + x4)) = ((x1 + x3) + (x2 + x4))

    proof

      let X be RealLinearSpace, x1,x2,x3,x4 be Point of X;

      

      thus ((x1 + x2) + (x3 + x4)) = (((x1 + x2) + x3) + x4) by RLVECT_1:def 3

      .= (((x1 + x3) + x2) + x4) by RLVECT_1:def 3

      .= ((x1 + x3) + (x2 + x4)) by RLVECT_1:def 3;

    end;

    registration

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      cluster ( MultilinearOperators (X,Y)) -> non empty functional;

      coherence

      proof

        set f = the MultilinearOperator of X, Y;

        f in ( MultilinearOperators (X,Y)) by Def6;

        hence ( MultilinearOperators (X,Y)) is non empty;

        let x be object;

        assume x in ( MultilinearOperators (X,Y));

        hence thesis;

      end;

      cluster ( MultilinearOperators (X,Y)) -> linearly-closed;

      coherence

      proof

        set W = ( MultilinearOperators (X,Y));

        

         A1: for v,u be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) st v in ( MultilinearOperators (X,Y)) & u in ( MultilinearOperators (X,Y)) holds (v + u) in ( MultilinearOperators (X,Y))

        proof

          let v,u be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) such that

           A2: v in W and

           A3: u in W;

          reconsider u1 = u as MultilinearOperator of X, Y by A3, Def6;

          reconsider v1 = v as MultilinearOperator of X, Y by A2, Def6;

          (v + u) is MultilinearOperator of X, Y

          proof

            reconsider L0 = (v + u) as Function of ( product X), Y by FUNCT_2: 66;

            now

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

              reconsider L = (L0 * ( reproj (i,x))) as Function of (X . i), Y;

              

               A4: (u1 * ( reproj (i,x))) is LinearOperator of (X . i), Y & (v1 * ( reproj (i,x))) is LinearOperator of (X . i), Y by Def3;

              

               A5: for x1,x2 be Point of (X . i) holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

              proof

                let x1,x2 be Point of (X . i);

                

                thus (L . (x1 + x2)) = (L0 . (( reproj (i,x)) . (x1 + x2))) by FUNCT_2: 15

                .= ((u1 . (( reproj (i,x)) . (x1 + x2))) + (v1 . (( reproj (i,x)) . (x1 + x2)))) by LOPBAN_1: 1

                .= (((u1 * ( reproj (i,x))) . (x1 + x2)) + (v1 . (( reproj (i,x)) . (x1 + x2)))) by FUNCT_2: 15

                .= (((u1 * ( reproj (i,x))) . (x1 + x2)) + ((v1 * ( reproj (i,x))) . (x1 + x2))) by FUNCT_2: 15

                .= ((((u1 * ( reproj (i,x))) . x1) + ((u1 * ( reproj (i,x))) . x2)) + ((v1 * ( reproj (i,x))) . (x1 + x2))) by A4, VECTSP_1:def 20

                .= ((((u1 * ( reproj (i,x))) . x1) + ((u1 * ( reproj (i,x))) . x2)) + (((v1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x2))) by A4, VECTSP_1:def 20

                .= ((((u1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x1)) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by LM14

                .= (((u1 . (( reproj (i,x)) . x1)) + ((v1 * ( reproj (i,x))) . x1)) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + ((u1 . (( reproj (i,x)) . x2)) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + ((u1 . (( reproj (i,x)) . x2)) + (v1 . (( reproj (i,x)) . x2)))) by FUNCT_2: 15

                .= ((L0 . (( reproj (i,x)) . x1)) + ((u1 . (( reproj (i,x)) . x2)) + (v1 . (( reproj (i,x)) . x2)))) by LOPBAN_1: 1

                .= ((L0 . (( reproj (i,x)) . x1)) + (L0 . (( reproj (i,x)) . x2))) by LOPBAN_1: 1

                .= ((L . x1) + ((u + v) . (( reproj (i,x)) . x2))) by FUNCT_2: 15

                .= ((L . x1) + (L . x2)) by FUNCT_2: 15;

              end;

              for x be Point of (X . i), a be Real holds (L . (a * x)) = (a * (L . x))

              proof

                let x1 be Point of (X . i), a be Real;

                

                thus (L . (a * x1)) = (L0 . (( reproj (i,x)) . (a * x1))) by FUNCT_2: 15

                .= ((u1 . (( reproj (i,x)) . (a * x1))) + (v1 . (( reproj (i,x)) . (a * x1)))) by LOPBAN_1: 1

                .= (((u1 * ( reproj (i,x))) . (a * x1)) + (v1 . (( reproj (i,x)) . (a * x1)))) by FUNCT_2: 15

                .= (((u1 * ( reproj (i,x))) . (a * x1)) + ((v1 * ( reproj (i,x))) . (a * x1))) by FUNCT_2: 15

                .= ((a * ((u1 * ( reproj (i,x))) . x1)) + ((v1 * ( reproj (i,x))) . (a * x1))) by A4, LOPBAN_1:def 5

                .= ((a * ((u1 * ( reproj (i,x))) . x1)) + (a * ((v1 * ( reproj (i,x))) . x1))) by A4, LOPBAN_1:def 5

                .= ((a * (u1 . (( reproj (i,x)) . x1))) + (a * ((v1 * ( reproj (i,x))) . x1))) by FUNCT_2: 15

                .= ((a * (u1 . (( reproj (i,x)) . x1))) + (a * (v1 . (( reproj (i,x)) . x1)))) by FUNCT_2: 15

                .= (a * ((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1)))) by RLVECT_1:def 5

                .= (a * (L0 . (( reproj (i,x)) . x1))) by LOPBAN_1: 1

                .= (a * (L . x1)) by FUNCT_2: 15;

              end;

              hence (L0 * ( reproj (i,x))) is LinearOperator of (X . i), Y by A5, LOPBAN_1:def 5, VECTSP_1:def 20;

            end;

            hence thesis by Def3;

          end;

          hence thesis by Def6;

        end;

        for b be Real holds for v be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) st v in W holds (b * v) in W

        proof

          let b be Real;

          let v be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) such that

           A9: v in W;

          reconsider v1 = v as MultilinearOperator of X, Y by A9, Def6;

          (b * v) is MultilinearOperator of X, Y

          proof

            reconsider L0 = (b * v) as Function of ( product X), Y by FUNCT_2: 66;

            now

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

              reconsider L = (L0 * ( reproj (i,x))) as Function of (X . i), Y;

              

               A10: (v1 * ( reproj (i,x))) is LinearOperator of (X . i), Y by Def3;

              

               A11: for x1,x2 be Point of (X . i) holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

              proof

                let x1,x2 be Point of (X . i);

                

                thus (L . (x1 + x2)) = (L0 . (( reproj (i,x)) . (x1 + x2))) by FUNCT_2: 15

                .= (b * (v1 . (( reproj (i,x)) . (x1 + x2)))) by LOPBAN_1: 2

                .= (b * ((v1 * ( reproj (i,x))) . (x1 + x2))) by FUNCT_2: 15

                .= (b * (((v1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x2))) by A10, VECTSP_1:def 20

                .= ((b * ((v1 * ( reproj (i,x))) . x1)) + (b * ((v1 * ( reproj (i,x))) . x2))) by RLVECT_1:def 5

                .= ((b * (v1 . (( reproj (i,x)) . x1))) + (b * ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= ((b * (v1 . (( reproj (i,x)) . x1))) + (b * (v1 . (( reproj (i,x)) . x2)))) by FUNCT_2: 15

                .= ((L0 . (( reproj (i,x)) . x1)) + (b * (v1 . (( reproj (i,x)) . x2)))) by LOPBAN_1: 2

                .= ((L0 . (( reproj (i,x)) . x1)) + (L0 . (( reproj (i,x)) . x2))) by LOPBAN_1: 2

                .= ((L . x1) + (L0 . (( reproj (i,x)) . x2))) by FUNCT_2: 15

                .= ((L . x1) + (L . x2)) by FUNCT_2: 15;

              end;

              for z be Point of (X . i), a be Real holds (L . (a * z)) = (a * (L . z))

              proof

                let x1 be Point of (X . i), a be Real;

                

                thus (L . (a * x1)) = (L0 . (( reproj (i,x)) . (a * x1))) by FUNCT_2: 15

                .= (b * (v1 . (( reproj (i,x)) . (a * x1)))) by LOPBAN_1: 2

                .= (b * ((v1 * ( reproj (i,x))) . (a * x1))) by FUNCT_2: 15

                .= (b * (a * ((v1 * ( reproj (i,x))) . x1))) by A10, LOPBAN_1:def 5

                .= ((b * a) * ((v1 * ( reproj (i,x))) . x1)) by RLVECT_1:def 7

                .= (a * (b * ((v1 * ( reproj (i,x))) . x1))) by RLVECT_1:def 7

                .= (a * (b * (v1 . (( reproj (i,x)) . x1)))) by FUNCT_2: 15

                .= (a * (L0 . (( reproj (i,x)) . x1))) by LOPBAN_1: 2

                .= (a * (L . x1)) by FUNCT_2: 15;

              end;

              hence (L0 * ( reproj (i,x))) is LinearOperator of (X . i), Y by A11, LOPBAN_1:def 5, VECTSP_1:def 20;

            end;

            hence thesis by Def3;

          end;

          hence thesis by Def6;

        end;

        hence thesis by A1, RLSUB_1:def 1;

      end;

    end

    definition

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      :: LOPBAN10:def5

      func R_VectorSpace_of_MultilinearOperators (X,Y) -> strict RLSStruct equals RLSStruct (# ( MultilinearOperators (X,Y)), ( Zero_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Add_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Mult_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))) #);

      coherence ;

    end

    theorem :: LOPBAN10:10

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace holds RLSStruct (# ( MultilinearOperators (X,Y)), ( Zero_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Add_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Mult_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))) #) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

    registration

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      cluster ( R_VectorSpace_of_MultilinearOperators (X,Y)) -> non empty;

      coherence ;

    end

    registration

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      cluster ( R_VectorSpace_of_MultilinearOperators (X,Y)) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by RSSPACE: 11;

    end

    registration

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      cluster ( R_VectorSpace_of_MultilinearOperators (X,Y)) -> constituted-Functions;

      coherence by MONOID_0: 80;

    end

    definition

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      let f be Element of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      let v be VECTOR of ( product X);

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as MultilinearOperator of X, Y by Def6;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN10:11

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace holds for f,g,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of ( product X) holds (h . x) = ((f . x) + (g . x))

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      let f,g,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      reconsider f9 = f, g9 = g, h9 = h as MultilinearOperator of X, Y by Def6;

      

       A1: ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h, g1 = g as VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) by RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (f + g);

        let x be Element of ( product X);

        h1 = (f1 + g1) by A1, A3, RLSUB_1: 13;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by LOPBAN_1: 1;

      end;

      now

        assume for x be Element of ( product X) holds (h9 . x) = ((f9 . x) + (g9 . x));

        then h1 = (f1 + g1) by LOPBAN_1: 1;

        hence h = (f + g) by A1, RLSUB_1: 13;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN10:12

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace holds for f,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of ( product X) holds (h . x) = (a * (f . x))

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      let f,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      reconsider f9 = f, h9 = h as MultilinearOperator of X, Y by Def6;

      let a be Real;

      

       A1: ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h as VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) by RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (a * f);

        let x be Element of ( product X);

        h1 = (a * f1) by A1, A3, RLSUB_1: 14;

        hence (h9 . x) = (a * (f9 . x)) by LOPBAN_1: 2;

      end;

      now

        assume for x be Element of ( product X) holds (h9 . x) = (a * (f9 . x));

        then h1 = (a * f1) by LOPBAN_1: 2;

        hence h = (a * f) by A1, RLSUB_1: 14;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN10:13

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace holds ( 0. ( R_VectorSpace_of_MultilinearOperators (X,Y))) = (the carrier of ( product X) --> ( 0. Y))

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      

       A1: ( 0. ( RealVectSpace (the carrier of ( product X),Y))) = (the carrier of ( product X) --> ( 0. Y));

      ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      hence thesis by A1, RLSUB_1: 11;

    end;

    theorem :: LOPBAN10:14

    for X be RealLinearSpace-Sequence, Y be RealLinearSpace holds (the carrier of ( product X) --> ( 0. Y)) is MultilinearOperator of X, Y

    proof

      let X be RealLinearSpace-Sequence, Y be RealLinearSpace;

      set f0 = (the carrier of ( product X) --> ( 0. Y));

      now

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

        set F = (f0 * ( reproj (i,u)));

        

         A1: ( dom F) = the carrier of (X . i) by FUNCT_2:def 1;

        

         A4: for z be object st z in ( dom F) holds (F . z) = ( 0. Y)

        proof

          let z be object;

          assume z in ( dom F);

          then

           A2: z in the carrier of (X . i) by FUNCT_2:def 1;

          

          thus (F . z) = (f0 . (( reproj (i,u)) . z)) by A2, FUNCT_2: 15

          .= ( 0. Y) by A2, FUNCT_2: 5, FUNCOP_1: 7;

        end;

        reconsider f = (f0 * ( reproj (i,u))) as Function of (X . i), Y;

        

         A5: f is homogeneous

        proof

          let x be VECTOR of (X . i), r be Real;

          

          thus (f . (r * x)) = (r * ( 0. Y)) by A1, A4

          .= (r * (f . x)) by A1, A4;

        end;

        now

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

          

          thus (f . (x + y)) = ( 0. Y) by A1, A4

          .= ((f . x) + ( 0. Y)) by A1, A4

          .= ((f . x) + (f . y)) by A1, A4;

        end;

        hence (f0 * ( reproj (i,u))) is LinearOperator of (X . i), Y by A5, VECTSP_1:def 20;

      end;

      hence thesis by Def3;

    end;

    begin

    

     Def2: for X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X) holds ex x0 be Element of ( product ( carr X)) st x0 = x & ( reproj (i,x)) = ( reproj (i,x0))

    proof

      let X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X);

      

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

      then

      reconsider x0 = x as Element of ( product ( carr X));

      take x0;

      

       A5: (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

      now

        let r be Element of (X . i);

        

        thus (( reproj (i,x)) . r) = (x +* (i,r)) by NDIFF_5:def 4

        .= (( reproj (i,x0)) . r) by A5, Def1;

      end;

      hence thesis by A1, A5, FUNCT_2: 63;

    end;

    theorem :: LOPBAN10:15

    

     Th3: for X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F be Function st F = (( reproj (i,x)) . r) holds (F . i) = r

    proof

      let X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F be Function;

      assume

       A1: F = (( reproj (i,x)) . r);

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      

       A3: (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def2;

      thus (F . i) = r by A1, A2, A3, A4, Th1;

    end;

    theorem :: LOPBAN10:16

    

     Th4: for X be RealNormSpace-Sequence, i,j be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F,s be Function st F = (( reproj (i,x)) . r) & x = s & i <> j holds (F . j) = (s . j)

    proof

      let X be RealNormSpace-Sequence, i,j be Element of ( dom X), x be Element of ( product X), r be Element of (X . i), F,s be Function;

      assume

       A1: F = (( reproj (i,x)) . r) & x = s & i <> j;

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      

       A3: (( carr X) . i) = the carrier of (X . i) by PRVECT_1:def 11;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def2;

      thus (F . j) = (s . j) by A1, A2, A3, A4, Th2;

    end;

    theorem :: LOPBAN10:17

    

     Th4X: for X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), s be Function st x = s holds (( reproj (i,x)) . (s . i)) = x

    proof

      let X be RealNormSpace-Sequence, i be Element of ( dom X), x be Element of ( product X), s be Function;

      assume

       A1: x = s;

      

       A2: ( dom ( carr X)) = ( dom X) by LemmaX;

      consider x0 be Element of ( product ( carr X)) such that

       A4: x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by Def2;

      thus (( reproj (i,x)) . (s . i)) = x by A1, A2, A4, Th2X;

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace, f be Function of ( product X), Y;

      :: LOPBAN10:def6

      attr f is Multilinear means

      : Def3: for i be Element of ( dom X), x be Element of ( product X) holds (f * ( reproj (i,x))) is LinearOperator of (X . i), Y;

    end

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster Multilinear for Function of ( product X), Y;

      correctness

      proof

        set g = (the carrier of ( product X) --> ( 0. Y));

        take g;

        now

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

          set F = (g * ( reproj (i,x)));

          

           A1: ( dom F) = the carrier of (X . i) by FUNCT_2:def 1;

          

           A4: for z be object st z in ( dom F) holds (F . z) = ( 0. Y)

          proof

            let z be object;

            assume z in ( dom F);

            then

             A2: z in the carrier of (X . i) by FUNCT_2:def 1;

            

            thus (F . z) = (g . (( reproj (i,x)) . z)) by A2, FUNCT_2: 15

            .= ( 0. Y) by A2, FUNCOP_1: 7, FUNCT_2: 5;

          end;

          reconsider f = (g * ( reproj (i,x))) as Function of the carrier of (X . i), Y;

           A5:

          now

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

            

            thus (f . (x + y)) = ( 0. Y) by A1, A4

            .= ((f . x) + ( 0. Y)) by A1, A4

            .= ((f . x) + (f . y)) by A1, A4;

          end;

          now

            let x be VECTOR of (X . i);

            let r be Real;

            

            thus (f . (r * x)) = (r * ( 0. Y)) by A1, A4

            .= (r * (f . x)) by A1, A4;

          end;

          hence (g * ( reproj (i,x))) is LinearOperator of (X . i), Y by A5, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

        hence g is Multilinear;

      end;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      mode MultilinearOperator of X,Y is Multilinear Function of ( product X), Y;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def7

      func MultilinearOperators (X,Y) -> Subset of ( RealVectSpace (the carrier of ( product X),Y)) means

      : Def6: for x be set holds x in it iff x is MultilinearOperator of X, Y;

      existence

      proof

        defpred P[ object] means $1 is MultilinearOperator of X, Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( Funcs (the carrier of ( product X),the carrier of Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( Funcs (the carrier of ( product X),the carrier of Y)) by A1;

        hence IT is Subset of ( RealVectSpace (the carrier of ( product X),Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is MultilinearOperator of X, Y by A1;

        assume

         A2: x is MultilinearOperator of X, Y;

        then x in ( Funcs (the carrier of ( product X),the carrier of Y)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( RealVectSpace (the carrier of ( product X),Y));

        assume that

         A3: for x be set holds x in X1 iff x is MultilinearOperator of X, Y and

         A4: for x be set holds x in X2 iff x is MultilinearOperator of X, Y;

        

         A5: X2 c= X1

        proof

          let x be object;

          assume x in X2;

          then x is MultilinearOperator of X, Y by A4;

          hence thesis by A3;

        end;

        X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x is MultilinearOperator of X, Y by A3;

          hence thesis by A4;

        end;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

    end

    

     LM14: for X be RealNormSpace, x1,x2,x3,x4 be Point of X holds ((x1 + x2) + (x3 + x4)) = ((x1 + x3) + (x2 + x4))

    proof

      let X be RealNormSpace, x1,x2,x3,x4 be Point of X;

      

      thus ((x1 + x2) + (x3 + x4)) = (((x1 + x2) + x3) + x4) by RLVECT_1:def 3

      .= (((x1 + x3) + x2) + x4) by RLVECT_1:def 3

      .= ((x1 + x3) + (x2 + x4)) by RLVECT_1:def 3;

    end;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster ( MultilinearOperators (X,Y)) -> non empty functional;

      coherence

      proof

        set f = the MultilinearOperator of X, Y;

        f in ( MultilinearOperators (X,Y)) by Def6;

        hence ( MultilinearOperators (X,Y)) is non empty;

        let x be object;

        assume x in ( MultilinearOperators (X,Y));

        hence thesis;

      end;

      cluster ( MultilinearOperators (X,Y)) -> linearly-closed;

      coherence

      proof

        set W = ( MultilinearOperators (X,Y));

        

         A1: for v,u be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) st v in ( MultilinearOperators (X,Y)) & u in ( MultilinearOperators (X,Y)) holds (v + u) in ( MultilinearOperators (X,Y))

        proof

          let v,u be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) such that

           A2: v in W and

           A3: u in W;

          reconsider u1 = u as MultilinearOperator of X, Y by A3, Def6;

          reconsider v1 = v as MultilinearOperator of X, Y by A2, Def6;

          (v + u) is MultilinearOperator of X, Y

          proof

            reconsider L0 = (v + u) as Function of ( product X), Y by FUNCT_2: 66;

            now

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

              reconsider L = (L0 * ( reproj (i,x))) as Function of (X . i), Y;

              

               A4: (u1 * ( reproj (i,x))) is LinearOperator of (X . i), Y & (v1 * ( reproj (i,x))) is LinearOperator of (X . i), Y by Def3;

              

               A5: for x1,x2 be Point of (X . i) holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

              proof

                let x1,x2 be Point of (X . i);

                

                thus (L . (x1 + x2)) = (L0 . (( reproj (i,x)) . (x1 + x2))) by FUNCT_2: 15

                .= ((u1 . (( reproj (i,x)) . (x1 + x2))) + (v1 . (( reproj (i,x)) . (x1 + x2)))) by LOPBAN_1: 1

                .= (((u1 * ( reproj (i,x))) . (x1 + x2)) + (v1 . (( reproj (i,x)) . (x1 + x2)))) by FUNCT_2: 15

                .= (((u1 * ( reproj (i,x))) . (x1 + x2)) + ((v1 * ( reproj (i,x))) . (x1 + x2))) by FUNCT_2: 15

                .= ((((u1 * ( reproj (i,x))) . x1) + ((u1 * ( reproj (i,x))) . x2)) + ((v1 * ( reproj (i,x))) . (x1 + x2))) by A4, VECTSP_1:def 20

                .= ((((u1 * ( reproj (i,x))) . x1) + ((u1 * ( reproj (i,x))) . x2)) + (((v1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x2))) by A4, VECTSP_1:def 20

                .= ((((u1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x1)) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by LM14

                .= (((u1 . (( reproj (i,x)) . x1)) + ((v1 * ( reproj (i,x))) . x1)) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + (((u1 * ( reproj (i,x))) . x2) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + ((u1 . (( reproj (i,x)) . x2)) + ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= (((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1))) + ((u1 . (( reproj (i,x)) . x2)) + (v1 . (( reproj (i,x)) . x2)))) by FUNCT_2: 15

                .= ((L0 . (( reproj (i,x)) . x1)) + ((u1 . (( reproj (i,x)) . x2)) + (v1 . (( reproj (i,x)) . x2)))) by LOPBAN_1: 1

                .= ((L0 . (( reproj (i,x)) . x1)) + (L0 . (( reproj (i,x)) . x2))) by LOPBAN_1: 1

                .= ((L . x1) + ((u + v) . (( reproj (i,x)) . x2))) by FUNCT_2: 15

                .= ((L . x1) + (L . x2)) by FUNCT_2: 15;

              end;

              for x be Point of (X . i), a be Real holds (L . (a * x)) = (a * (L . x))

              proof

                let x1 be Point of (X . i), a be Real;

                

                thus (L . (a * x1)) = (L0 . (( reproj (i,x)) . (a * x1))) by FUNCT_2: 15

                .= ((u1 . (( reproj (i,x)) . (a * x1))) + (v1 . (( reproj (i,x)) . (a * x1)))) by LOPBAN_1: 1

                .= (((u1 * ( reproj (i,x))) . (a * x1)) + (v1 . (( reproj (i,x)) . (a * x1)))) by FUNCT_2: 15

                .= (((u1 * ( reproj (i,x))) . (a * x1)) + ((v1 * ( reproj (i,x))) . (a * x1))) by FUNCT_2: 15

                .= ((a * ((u1 * ( reproj (i,x))) . x1)) + ((v1 * ( reproj (i,x))) . (a * x1))) by A4, LOPBAN_1:def 5

                .= ((a * ((u1 * ( reproj (i,x))) . x1)) + (a * ((v1 * ( reproj (i,x))) . x1))) by A4, LOPBAN_1:def 5

                .= ((a * (u1 . (( reproj (i,x)) . x1))) + (a * ((v1 * ( reproj (i,x))) . x1))) by FUNCT_2: 15

                .= ((a * (u1 . (( reproj (i,x)) . x1))) + (a * (v1 . (( reproj (i,x)) . x1)))) by FUNCT_2: 15

                .= (a * ((u1 . (( reproj (i,x)) . x1)) + (v1 . (( reproj (i,x)) . x1)))) by RLVECT_1:def 5

                .= (a * (L0 . (( reproj (i,x)) . x1))) by LOPBAN_1: 1

                .= (a * (L . x1)) by FUNCT_2: 15;

              end;

              hence (L0 * ( reproj (i,x))) is LinearOperator of (X . i), Y by A5, LOPBAN_1:def 5, VECTSP_1:def 20;

            end;

            hence thesis by Def3;

          end;

          hence thesis by Def6;

        end;

        for b be Real holds for v be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) st v in W holds (b * v) in W

        proof

          let b be Real;

          let v be VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) such that

           A9: v in W;

          reconsider v1 = v as MultilinearOperator of X, Y by A9, Def6;

          (b * v) is MultilinearOperator of X, Y

          proof

            reconsider L0 = (b * v) as Function of ( product X), Y by FUNCT_2: 66;

            now

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

              reconsider L = (L0 * ( reproj (i,x))) as Function of (X . i), Y;

              

               A10: (v1 * ( reproj (i,x))) is LinearOperator of (X . i), Y by Def3;

              

               A11: for x1,x2 be Point of (X . i) holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

              proof

                let x1,x2 be Point of (X . i);

                

                thus (L . (x1 + x2)) = (L0 . (( reproj (i,x)) . (x1 + x2))) by FUNCT_2: 15

                .= (b * (v1 . (( reproj (i,x)) . (x1 + x2)))) by LOPBAN_1: 2

                .= (b * ((v1 * ( reproj (i,x))) . (x1 + x2))) by FUNCT_2: 15

                .= (b * (((v1 * ( reproj (i,x))) . x1) + ((v1 * ( reproj (i,x))) . x2))) by A10, VECTSP_1:def 20

                .= ((b * ((v1 * ( reproj (i,x))) . x1)) + (b * ((v1 * ( reproj (i,x))) . x2))) by RLVECT_1:def 5

                .= ((b * (v1 . (( reproj (i,x)) . x1))) + (b * ((v1 * ( reproj (i,x))) . x2))) by FUNCT_2: 15

                .= ((b * (v1 . (( reproj (i,x)) . x1))) + (b * (v1 . (( reproj (i,x)) . x2)))) by FUNCT_2: 15

                .= ((L0 . (( reproj (i,x)) . x1)) + (b * (v1 . (( reproj (i,x)) . x2)))) by LOPBAN_1: 2

                .= ((L0 . (( reproj (i,x)) . x1)) + (L0 . (( reproj (i,x)) . x2))) by LOPBAN_1: 2

                .= ((L . x1) + (L0 . (( reproj (i,x)) . x2))) by FUNCT_2: 15

                .= ((L . x1) + (L . x2)) by FUNCT_2: 15;

              end;

              for z be Point of (X . i), a be Real holds (L . (a * z)) = (a * (L . z))

              proof

                let x1 be Point of (X . i), a be Real;

                

                thus (L . (a * x1)) = (L0 . (( reproj (i,x)) . (a * x1))) by FUNCT_2: 15

                .= (b * (v1 . (( reproj (i,x)) . (a * x1)))) by LOPBAN_1: 2

                .= (b * ((v1 * ( reproj (i,x))) . (a * x1))) by FUNCT_2: 15

                .= (b * (a * ((v1 * ( reproj (i,x))) . x1))) by A10, LOPBAN_1:def 5

                .= ((b * a) * ((v1 * ( reproj (i,x))) . x1)) by RLVECT_1:def 7

                .= (a * (b * ((v1 * ( reproj (i,x))) . x1))) by RLVECT_1:def 7

                .= (a * (b * (v1 . (( reproj (i,x)) . x1)))) by FUNCT_2: 15

                .= (a * (L0 . (( reproj (i,x)) . x1))) by LOPBAN_1: 2

                .= (a * (L . x1)) by FUNCT_2: 15;

              end;

              hence (L0 * ( reproj (i,x))) is LinearOperator of (X . i), Y by A11, LOPBAN_1:def 5, VECTSP_1:def 20;

            end;

            hence thesis by Def3;

          end;

          hence thesis by Def6;

        end;

        hence thesis by A1, RLSUB_1:def 1;

      end;

    end

    theorem :: LOPBAN10:18

    for X be RealNormSpace-Sequence, Y be RealNormSpace holds RLSStruct (# ( MultilinearOperators (X,Y)), ( Zero_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Add_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Mult_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))) #) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster RLSStruct (# ( MultilinearOperators (X,Y)), ( Zero_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Add_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Mult_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by RSSPACE: 11;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def8

      func R_VectorSpace_of_MultilinearOperators (X,Y) -> strict RealLinearSpace equals RLSStruct (# ( MultilinearOperators (X,Y)), ( Zero_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Add_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))), ( Mult_ (( MultilinearOperators (X,Y)),( RealVectSpace (the carrier of ( product X),Y)))) #);

      coherence ;

    end

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster ( R_VectorSpace_of_MultilinearOperators (X,Y)) -> constituted-Functions;

      coherence by MONOID_0: 80;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Element of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      let v be VECTOR of ( product X);

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as MultilinearOperator of X, Y by Def6;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN10:19

    

     Th16: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,g,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of ( product X) holds (h . x) = ((f . x) + (g . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,g,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      reconsider f9 = f, g9 = g, h9 = h as MultilinearOperator of X, Y by Def6;

      

       A1: ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h, g1 = g as VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) by RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (f + g);

        let x be Element of ( product X);

        h1 = (f1 + g1) by A1, A3, RLSUB_1: 13;

        hence (h9 . x) = ((f9 . x) + (g9 . x)) by LOPBAN_1: 1;

      end;

      now

        assume for x be Element of ( product X) holds (h9 . x) = ((f9 . x) + (g9 . x));

        then h1 = (f1 + g1) by LOPBAN_1: 1;

        hence h = (f + g) by A1, RLSUB_1: 13;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN10:20

    

     Th17: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of ( product X) holds (h . x) = (a * (f . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,h be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y));

      reconsider f9 = f, h9 = h as MultilinearOperator of X, Y by Def6;

      let a be Real;

      

       A1: ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h as VECTOR of ( RealVectSpace (the carrier of ( product X),Y)) by RLSUB_1: 10;

       A2:

      now

        assume

         A3: h = (a * f);

        let x be Element of ( product X);

        h1 = (a * f1) by A1, A3, RLSUB_1: 14;

        hence (h9 . x) = (a * (f9 . x)) by LOPBAN_1: 2;

      end;

      now

        assume for x be Element of ( product X) holds (h9 . x) = (a * (f9 . x));

        then h1 = (a * f1) by LOPBAN_1: 2;

        hence h = (a * f) by A1, RLSUB_1: 14;

      end;

      hence thesis by A2;

    end;

    theorem :: LOPBAN10:21

    

     Th18: for X be RealNormSpace-Sequence, Y be RealNormSpace holds ( 0. ( R_VectorSpace_of_MultilinearOperators (X,Y))) = (the carrier of ( product X) --> ( 0. Y))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      

       A1: ( 0. ( RealVectSpace (the carrier of ( product X),Y))) = (the carrier of ( product X) --> ( 0. Y));

      ( R_VectorSpace_of_MultilinearOperators (X,Y)) is Subspace of ( RealVectSpace (the carrier of ( product X),Y)) by RSSPACE: 11;

      hence thesis by A1, RLSUB_1: 11;

    end;

    theorem :: LOPBAN10:22

    

     Th19: for X be RealNormSpace-Sequence, Y be RealNormSpace holds (the carrier of ( product X) --> ( 0. Y)) is MultilinearOperator of X, Y

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      set f0 = (the carrier of ( product X) --> ( 0. Y));

      now

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

        set F = (f0 * ( reproj (i,u)));

        

         A1: ( dom F) = the carrier of (X . i) by FUNCT_2:def 1;

        

         A4: for z be object st z in ( dom F) holds (F . z) = ( 0. Y)

        proof

          let z be object;

          assume z in ( dom F);

          then

           A2: z in the carrier of (X . i) by FUNCT_2:def 1;

          

          thus (F . z) = (f0 . (( reproj (i,u)) . z)) by A2, FUNCT_2: 15

          .= ( 0. Y) by A2, FUNCT_2: 5, FUNCOP_1: 7;

        end;

        reconsider f = (f0 * ( reproj (i,u))) as Function of (X . i), Y;

        

         A5: f is homogeneous

        proof

          let x be VECTOR of (X . i), r be Real;

          

          thus (f . (r * x)) = (r * ( 0. Y)) by A1, A4

          .= (r * (f . x)) by A1, A4;

        end;

        now

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

          

          thus (f . (x + y)) = ( 0. Y) by A1, A4

          .= ((f . x) + ( 0. Y)) by A1, A4

          .= ((f . x) + (f . y)) by A1, A4;

        end;

        hence (f0 * ( reproj (i,u))) is LinearOperator of (X . i), Y by A5, VECTSP_1:def 20;

      end;

      hence thesis by Def3;

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let IT be MultilinearOperator of X, Y;

      let x be VECTOR of ( product X);

      :: original: .

      redefine

      func IT . x -> Point of Y ;

      correctness

      proof

        (IT . x) in the carrier of Y;

        hence thesis;

      end;

    end

    registration

      let X be RealNormSpace-Sequence;

      cluster ( product X) -> constituted-Functions;

      coherence ;

    end

    definition

      let X be RealNormSpace-Sequence;

      let x be Point of ( product X);

      let i be Element of ( dom X);

      :: original: .

      redefine

      func x . i -> Point of (X . i) ;

      correctness

      proof

        

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

        reconsider s = x as Element of ( product ( carr X)) by A1;

        (s . i) is Point of (X . i);

        hence thesis;

      end;

    end

    

     EXTh10: for G be RealNormSpace-Sequence holds the carrier of ( product G) = ( product ( carr G))

    proof

      let G be RealNormSpace-Sequence;

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

      hence thesis;

    end;

    theorem :: LOPBAN10:23

    

     EXTh12: for G be RealNormSpace-Sequence, p,q,r be Point of ( product G) holds (p + q) = r iff for i be Element of ( dom G) holds (r . i) = ((p . i) + (q . i))

    proof

      let G be RealNormSpace-Sequence, p,q,r be Point of ( product G);

      reconsider p0 = p, q0 = q, r0 = r as Element of ( product ( carr G)) by EXTh10;

      

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

      hereby

        assume

         A3: (p + q) = r;

        hereby

          let i be Element of ( dom G);

          reconsider i0 = i as Element of ( dom ( carr G)) by LemmaX;

          (( addop G) . i0) = the addF of (G . i0) by PRVECT_1:def 12;

          hence (r . i) = ((p . i) + (q . i)) by A2, A3, PRVECT_1:def 8;

        end;

      end;

      assume

       A4: for i be Element of ( dom G) holds (r . i) = ((p . i) + (q . i));

      reconsider pq = (p + q) as Element of ( product ( carr G)) by EXTh10;

      

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

      

       A6: ex g be Function st r0 = g & ( dom g) = ( dom ( carr G)) & for i be object st i in ( dom ( carr G)) holds (g . i) in (( carr G) . i) by CARD_3:def 5;

      now

        let i0 be object;

        assume

         A7: i0 in ( dom pq);

        then

        reconsider i1 = i0 as Element of ( dom G) by LemmaX, A5;

        reconsider i = i0 as Element of ( dom ( carr G)) by A5, A7;

        (( addop G) . i) = the addF of (G . i) by PRVECT_1:def 12;

        then (pq . i0) = ((p0 . i1) + (q0 . i1)) by A2, PRVECT_1:def 8;

        hence (pq . i0) = (r0 . i0) by A4;

      end;

      hence (p + q) = r by A5, A6;

    end;

    theorem :: LOPBAN10:24

    

     EXTh13: for G be RealNormSpace-Sequence, p,r be Point of ( product G), a be Real holds (a * p) = r iff for i be Element of ( dom G) holds (r . i) = (a * (p . i))

    proof

      let G be RealNormSpace-Sequence, p,r be Point of ( product G), a be Real;

      reconsider p0 = p, r0 = r as Element of ( product ( carr G)) by EXTh10;

      hereby

        assume

         A1: (a * p) = r;

        hereby

          let i be Element of ( dom G);

          reconsider i0 = i as Element of ( dom ( carr G)) by LemmaX;

          

           A2: (( multop G) . i0) = the Mult of (G . i0) by PRVECT_2:def 8;

          reconsider rr = a as Element of REAL by XREAL_0:def 1;

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

          

          hence (r . i) = (rr * (p0 . i)) by A1, A2, PRVECT_2:def 2

          .= (a * (p . i));

        end;

      end;

      assume

       A3: for i be Element of ( dom G) holds (r . i) = (a * (p . i));

      reconsider rp = (a * p) as Element of ( product ( carr G)) by EXTh10;

      

       A4: ex g be Function st rp = g & ( dom g) = ( dom ( carr G)) & for i be object st i in ( dom ( carr G)) holds (g . i) in (( carr G) . i) by CARD_3:def 5;

      

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

      now

        let i0 be object;

        assume

         A6: i0 in ( dom rp);

        then

        reconsider i1 = i0 as Element of ( dom G) by A4, LemmaX;

        reconsider i = i0 as Element of ( dom ( carr G)) by A4, A6;

        

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

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

        (( multop G) . i) = the Mult of (G . i) by PRVECT_2:def 8;

        then (rp . i0) = (a * (p0 . i1)) by A7, PRVECT_2:def 2;

        hence (rp . i0) = (r0 . i0) by A3;

      end;

      hence (a * p) = r by A4, A5;

    end;

    theorem :: LOPBAN10:25

    for G be RealNormSpace-Sequence, p be Point of ( product G) holds ( 0. ( product G)) = p iff for i be Element of ( dom G) holds (p . i) = ( 0. (G . i))

    proof

      let G be RealNormSpace-Sequence, p be Point of ( product G);

      reconsider p0 = p as Element of ( product ( carr G)) by EXTh10;

      

       A1: ( dom ( carr G)) = ( dom G) by LemmaX;

      

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

      hence ( 0. ( product G)) = p implies for i be Element of ( dom G) holds (p . i) = ( 0. (G . i)) by A1, PRVECT_1:def 14;

      assume

       A3: for i be Element of ( dom G) holds (p . i) = ( 0. (G . i));

      now

        let i0 be Element of ( dom ( carr G));

        reconsider i = i0 as Element of ( dom G) by LemmaX;

        (p0 . i0) = ( 0. (G . i)) by A3;

        hence (p0 . i0) = ( 0. (G . i0));

      end;

      hence ( 0. ( product G)) = p by A2, PRVECT_1:def 14;

    end;

    theorem :: LOPBAN10:26

    for G be RealNormSpace-Sequence, p,q,r be Point of ( product G) holds (p - q) = r iff for i be Element of ( dom G) holds (r . i) = ((p . i) - (q . i))

    proof

      let G be RealNormSpace-Sequence, p,q,r be Point of ( product G);

      reconsider p0 = p, q0 = q, r0 = r as Element of ( product ( carr G)) by EXTh10;

      reconsider qq0 = (( - 1) * q) as Element of ( product ( carr G)) by EXTh10;

      

       A2: (p - q) = (p + (( - 1) * q)) by RLVECT_1: 16;

      hereby

        assume

         A3: (p - q) = r;

        thus for i be Element of ( dom G) holds (r . i) = ((p . i) - (q . i))

        proof

          let i be Element of ( dom G);

          

           A4: (r0 . i) = ((p0 . i) + (qq0 . i)) by EXTh12, A3, A2;

          (qq0 . i) = (( - 1) * (q0 . i)) by EXTh13;

          hence thesis by A4, RLVECT_1: 16;

        end;

      end;

      assume

       A5: for i be Element of ( dom G) holds (r . i) = ((p . i) - (q . i));

      now

        let i be Element of ( dom G);

        

         A6: (qq0 . i) = (( - 1) * (q0 . i)) by EXTh13;

        (r0 . i) = ((p0 . i) - (q0 . i)) by A5;

        hence (r0 . i) = ((p0 . i) + (qq0 . i)) by A6, RLVECT_1: 16;

      end;

      hence (p - q) = r by A2, EXTh12;

    end;

    definition

      let X be RealNormSpace-Sequence, x be Point of ( product X);

      :: LOPBAN10:def9

      func NrProduct x -> non negative Real means

      : DefNrPro: ex Nx be FinSequence of REAL st ( dom Nx) = ( dom X) & (for i be Element of ( dom X) holds (Nx . i) = ||.(x . i).||) & it = ( Product Nx);

      existence

      proof

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

        then

        reconsider s = x as Element of ( product ( carr X));

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

        

         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 d = ||.(x . i).|| as Element of REAL ;

          take d;

          thus P1[n, d];

        end;

        consider F be FinSequence of REAL such that

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

        

         A9: ( dom F) = ( dom X) by A8, FINSEQ_3: 29;

        

         A10: for i be Element of ( dom X) holds (F . i) = ||.(x . i).||

        proof

          let i be Element of ( dom X);

          i in ( dom X);

          then

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

          reconsider n = i as Nat;

          consider j be Element of ( dom X) such that

           A12: n = j & (F /. n) = ||.(x . j).|| by A8, A11;

          thus (F . i) = ||.(x . i).|| by A9, A12, PARTFUN1:def 6;

        end;

        set R = ( Product F);

         0 <= ( Product F)

        proof

          per cases ;

            suppose ex i be Nat st i in ( dom F) & (F . i) = 0 ;

            hence 0 <= ( Product F) by RVSUM_1: 103;

          end;

            suppose

             A15: not ex i be Nat st i in ( dom F) & (F . i) = 0 ;

            for k be Element of NAT st k in ( dom F) holds (F . k) > 0

            proof

              let k be Element of NAT ;

              assume

               A17: k in ( dom F);

              then

               A18: (F . k) <> 0 by A15;

              reconsider i = k as Element of ( dom X) by A8, FINSEQ_3: 29, A17;

              (F . i) = ||.(x . i).|| by A10;

              hence (F . k) > 0 by A18;

            end;

            hence 0 <= ( Product F) by NAT_4: 42;

          end;

        end;

        then

        reconsider R as non negative Real;

        take R;

        thus thesis by A9, A10;

      end;

      uniqueness

      proof

        let N1,N2 be non negative Real;

        given Nx1 be FinSequence of REAL such that

         A21: ( dom Nx1) = ( dom X) & (for i be Element of ( dom X) holds (Nx1 . i) = ||.(x . i).||) & N1 = ( Product Nx1);

        given Nx2 be FinSequence of REAL such that

         A22: ( dom Nx2) = ( dom X) & (for i be Element of ( dom X) holds (Nx2 . i) = ||.(x . i).||) & N2 = ( Product Nx2);

        for i be Nat st i in ( dom Nx1) holds (Nx1 . i) = (Nx2 . i)

        proof

          let k be Nat;

          assume k in ( dom Nx1);

          then

          reconsider i = k as Element of ( dom X) by A21;

          (Nx1 . i) = ||.(x . i).|| by A21;

          hence thesis by A22;

        end;

        then Nx1 = Nx2 by A21, A22;

        hence thesis by A21, A22;

      end;

    end

    theorem :: LOPBAN10:27

    for X be RealNormSpace-Sequence, x be Point of ( product X) holds ((ex i be Element of ( dom X) st (x . i) = ( 0. (X . i))) iff ( NrProduct x) = 0 ) & ( not (ex i be Element of ( dom X) st (x . i) = ( 0. (X . i))) implies 0 < ( NrProduct x))

    proof

      let X be RealNormSpace-Sequence, x be Point of ( product X);

      consider Nx be FinSequence of REAL such that

       A1: ( dom Nx) = ( dom X) & (for i be Element of ( dom X) holds (Nx . i) = ||.(x . i).||) and

       A2: ( NrProduct x) = ( Product Nx) by DefNrPro;

      thus (ex i be Element of ( dom X) st (x . i) = ( 0. (X . i))) iff ( NrProduct x) = 0

      proof

        hereby

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

          then

          consider i be Element of ( dom X) such that

           A3: (x . i) = ( 0. (X . i));

          (Nx . i) = ||.( 0. (X . i)).|| by A1, A3

          .= 0 ;

          hence ( NrProduct x) = 0 by A1, A2, RVSUM_1: 103;

        end;

        assume ( NrProduct x) = 0 ;

        then

        consider k be Nat such that

         A5: k in ( dom Nx) & (Nx . k) = 0 by A2, RVSUM_1: 103;

        reconsider i = k as Element of ( dom X) by A1, A5;

         ||.(x . i).|| = 0 by A1, A5;

        then (x . i) = ( 0. (X . i)) by NORMSP_0:def 5;

        hence thesis;

      end;

      thus not (ex i be Element of ( dom X) st (x . i) = ( 0. (X . i))) implies 0 < ( NrProduct x)

      proof

        assume

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

        for k be Element of NAT st k in ( dom Nx) holds (Nx . k) > 0

        proof

          let k be Element of NAT ;

          assume k in ( dom Nx);

          then

          reconsider i = k as Element of ( dom X) by A1;

          

           A9: (Nx . i) = ||.(x . i).|| by A1;

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

          then (Nx . k) <> 0 by A9, NORMSP_0:def 5;

          hence (Nx . k) > 0 by A9;

        end;

        hence 0 < ( NrProduct x) by A2, NAT_4: 42;

      end;

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let IT be MultilinearOperator of X, Y;

      :: LOPBAN10:def10

      attr IT is Lipschitzian means

      : Def8: ex K be Real st 0 <= K & for x be Point of ( product X) holds ||.(IT . x).|| <= (K * ( NrProduct x));

    end

    theorem :: LOPBAN10:28

    

     Th21: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be MultilinearOperator of X, Y st (for x be VECTOR of ( product X) holds (f . x) = ( 0. Y)) holds f is Lipschitzian

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be MultilinearOperator of X, Y such that

       A1: for x be VECTOR of ( product X) holds (f . x) = ( 0. Y);

       A2:

      now

        let x be VECTOR of ( product X);

        

        thus ||.(f . x).|| = ||.( 0. Y).|| by A1

        .= ( 0 * ( NrProduct x));

      end;

      take 0 ;

      thus thesis by A2;

    end;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster Lipschitzian for MultilinearOperator of X, Y;

      existence

      proof

        set f = (the carrier of ( product X) --> ( 0. Y));

        reconsider f as MultilinearOperator of X, Y by Th19;

        take f;

        for x be VECTOR of ( product X) holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        hence thesis by Th21;

      end;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def11

      func BoundedMultilinearOperators (X,Y) -> Subset of ( R_VectorSpace_of_MultilinearOperators (X,Y)) means

      : Def9: for x be set holds x in it iff x is Lipschitzian MultilinearOperator of X, Y;

      existence

      proof

        defpred P[ object] means $1 is Lipschitzian MultilinearOperator of X, Y;

        consider IT be set such that

         A1: for x be object holds x in IT iff x in ( MultilinearOperators (X,Y)) & P[x] from XBOOLE_0:sch 1;

        take IT;

        for x be object st x in IT holds x in ( MultilinearOperators (X,Y)) by A1;

        hence IT is Subset of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by TARSKI:def 3;

        let x be set;

        thus x in IT implies x is Lipschitzian MultilinearOperator of X, Y by A1;

        assume

         A2: x is Lipschitzian MultilinearOperator of X, Y;

        then x in ( MultilinearOperators (X,Y)) by Def6;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let X1,X2 be Subset of ( R_VectorSpace_of_MultilinearOperators (X,Y));

        assume that

         A3: for x be set holds x in X1 iff x is Lipschitzian MultilinearOperator of X, Y and

         A4: for x be set holds x in X2 iff x is Lipschitzian MultilinearOperator of X, Y;

        

         A5: X2 c= X1

        proof

          let x be object;

          assume x in X2;

          then x is Lipschitzian MultilinearOperator of X, Y by A4;

          hence thesis by A3;

        end;

        X1 c= X2

        proof

          let x be object;

          assume x in X1;

          then x is Lipschitzian MultilinearOperator of X, Y by A3;

          hence thesis by A4;

        end;

        hence thesis by A5, XBOOLE_0:def 10;

      end;

    end

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster ( BoundedMultilinearOperators (X,Y)) -> non empty;

      coherence

      proof

        set f = (the carrier of ( product X) --> ( 0. Y));

        reconsider f as MultilinearOperator of X, Y by Th19;

        for x be VECTOR of ( product X) holds (f . x) = ( 0. Y) by FUNCOP_1: 7;

        then f is Lipschitzian by Th21;

        hence thesis by Def9;

      end;

      cluster ( BoundedMultilinearOperators (X,Y)) -> linearly-closed;

      coherence

      proof

        set W = ( BoundedMultilinearOperators (X,Y));

        

         A1: for v,u be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) st v in W & u in W holds (v + u) in W

        proof

          let v,u be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) such that

           A2: v in W and

           A3: u in W;

          reconsider f = (v + u) as MultilinearOperator of X, Y by Def6;

          f is Lipschitzian

          proof

            reconsider v1 = v as Lipschitzian MultilinearOperator of X, Y by A2, Def9;

            consider K2 be Real such that

             A4: 0 <= K2 and

             A5: for x be Point of ( product X) holds ||.(v1 . x).|| <= (K2 * ( NrProduct x)) by Def8;

            reconsider u1 = u as Lipschitzian MultilinearOperator of X, Y by A3, Def9;

            consider K1 be Real such that

             A6: 0 <= K1 and

             A7: for x be Point of ( product X) holds ||.(u1 . x).|| <= (K1 * ( NrProduct x)) by Def8;

            take K3 = (K1 + K2);

            now

              let x be VECTOR of ( product X);

              

               A8: ||.((u1 . x) + (v1 . x)).|| <= ( ||.(u1 . x).|| + ||.(v1 . x).||) by NORMSP_1:def 1;

              

               A9: ||.(v1 . x).|| <= (K2 * ( NrProduct x)) by A5;

               ||.(u1 . x).|| <= (K1 * ( NrProduct x)) by A7;

              then

               A10: ( ||.(u1 . x).|| + ||.(v1 . x).||) <= ((K1 * ( NrProduct x)) + (K2 * ( NrProduct x))) by A9, XREAL_1: 7;

               ||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th16;

              hence ||.(f . x).|| <= (K3 * ( NrProduct x)) by A8, A10, XXREAL_0: 2;

            end;

            hence thesis by A4, A6;

          end;

          hence thesis by Def9;

        end;

        for a be Real holds for v be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) st v in W holds (a * v) in W

        proof

          let a be Real;

          let v be VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) such that

           A11: v in W;

          reconsider f = (a * v) as MultilinearOperator of X, Y by Def6;

          f is Lipschitzian

          proof

            reconsider v1 = v as Lipschitzian MultilinearOperator of X, Y by A11, Def9;

            consider K be Real such that

             A12: 0 <= K and

             A13: for x be Point of ( product X) holds ||.(v1 . x).|| <= (K * ( NrProduct x)) by Def8;

            take ( |.a.| * K);

             A14:

            now

              let x be VECTOR of ( product X);

               0 <= |.a.| by COMPLEX1: 46;

              then

               A16: ( |.a.| * ||.(v1 . x).||) <= ( |.a.| * (K * ( NrProduct x))) by A13, XREAL_1: 64;

               ||.(a * (v1 . x)).|| = ( |.a.| * ||.(v1 . x).||) by NORMSP_1:def 1;

              hence ||.(f . x).|| <= (( |.a.| * K) * ( NrProduct x)) by A16, Th17;

            end;

             0 <= |.a.| by COMPLEX1: 46;

            hence thesis by A12, A14;

          end;

          hence thesis by Def9;

        end;

        hence thesis by A1, RLSUB_1:def 1;

      end;

    end

    theorem :: LOPBAN10:29

    for X be RealNormSpace-Sequence, Y be RealNormSpace holds RLSStruct (# ( BoundedMultilinearOperators (X,Y)), ( Zero_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Add_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Mult_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is Subspace of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RSSPACE: 11;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster RLSStruct (# ( BoundedMultilinearOperators (X,Y)), ( Zero_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Add_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Mult_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))) #) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence by RSSPACE: 11;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def12

      func R_VectorSpace_of_BoundedMultilinearOperators (X,Y) -> strict RealLinearSpace equals RLSStruct (# ( BoundedMultilinearOperators (X,Y)), ( Zero_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Add_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Mult_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))) #);

      coherence ;

    end

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster -> Function-like Relation-like for Element of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      coherence ;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Element of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      let v be VECTOR of ( product X);

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as MultilinearOperator of X, Y by Def9;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN10:30

    

     Th24: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,g,h be VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of ( product X) holds (h . x) = ((f . x) + (g . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,g,h be VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      

       A1: ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h, g1 = g as VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RLSUB_1: 10;

      hereby

        assume

         A2: h = (f + g);

        let x be Element of ( product X);

        h1 = (f1 + g1) by A1, A2, RLSUB_1: 13;

        hence (h . x) = ((f . x) + (g . x)) by Th16;

      end;

      assume for x be Element of ( product X) holds (h . x) = ((f . x) + (g . x));

      then h1 = (f1 + g1) by Th16;

      hence thesis by A1, RLSUB_1: 13;

    end;

    theorem :: LOPBAN10:31

    

     Th25: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,h be VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of ( product X) holds (h . x) = (a * (f . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,h be VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      let a be Real;

      

       A1: ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RSSPACE: 11;

      then

      reconsider f1 = f, h1 = h as VECTOR of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RLSUB_1: 10;

      hereby

        assume

         A2: h = (a * f);

        let x be Element of ( product X);

        h1 = (a * f1) by A1, A2, RLSUB_1: 14;

        hence (h . x) = (a * (f . x)) by Th17;

      end;

      assume for x be Element of ( product X) holds (h . x) = (a * (f . x));

      then h1 = (a * f1) by Th17;

      hence thesis by A1, RLSUB_1: 14;

    end;

    theorem :: LOPBAN10:32

    

     Th26: for X be RealNormSpace-Sequence, Y be RealNormSpace holds ( 0. ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y))) = (the carrier of ( product X) --> ( 0. Y))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      

       A1: ( 0. ( R_VectorSpace_of_MultilinearOperators (X,Y))) = (the carrier of ( product X) --> ( 0. Y)) by Th18;

      ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y)) is Subspace of ( R_VectorSpace_of_MultilinearOperators (X,Y)) by RSSPACE: 11;

      hence thesis by A1, RLSUB_1: 11;

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be object;

      :: LOPBAN10:def13

      func modetrans (f,X,Y) -> Lipschitzian MultilinearOperator of X, Y equals

      : Def11: f;

      coherence by A1, Def9;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let u be MultilinearOperator of X, Y;

      :: LOPBAN10:def14

      func PreNorms (u) -> non empty Subset of REAL equals { ||.(u . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 };

      coherence

      proof

         A1:

        now

          let x be object;

          now

            assume x in { ||.(u . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 };

            then ex t be VECTOR of ( product X) st x = ||.(u . t).|| & for i be Element of ( dom X) holds ||.(t . i).|| <= 1;

            hence x in REAL ;

          end;

          hence x in { ||.(u . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 } implies x in REAL ;

        end;

        

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

        

         A3: ( dom X) = ( dom ( carr X)) by LemmaX;

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

        reconsider s = x as Element of ( product ( carr X)) by A2;

        for i be Element of ( dom X) holds ||.(x . i).|| <= 1

        proof

          let i be Element of ( dom X);

          (s . i) = ( 0. (X . i)) by A2, A3, PRVECT_1:def 14;

          hence thesis;

        end;

        then ||.(u . x).|| in { ||.(u . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 };

        hence thesis by A1, TARSKI:def 3;

      end;

    end

    theorem :: LOPBAN10:33

    for X be RealNormSpace-Sequence, s be Element of ( product X) holds ex F be FinSequence of REAL st ( dom F) = ( dom X) & for i be Element of ( dom X) holds (F . i) = ||.(s . i).||

    proof

      let X be RealNormSpace-Sequence, s be Element of ( product X);

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

      

       A5: 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 d = ||.(s . i).|| as Element of REAL ;

        take d;

        thus P1[n, d];

      end;

      consider F be FinSequence of REAL such that

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

      take F;

      thus

       A7: ( dom F) = ( dom X) by A6, FINSEQ_3: 29;

      thus for i be Element of ( dom X) holds (F . i) = ||.(s . i).||

      proof

        let i be Element of ( dom X);

        i in ( dom X);

        then

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

        reconsider n = i as Nat;

        consider j be Element of ( dom X) such that

         A9: n = j & (F /. n) = ||.(s . j).|| by A6, A8;

        thus (F . i) = ||.(s . i).|| by A7, A9, PARTFUN1:def 6;

      end;

    end;

    theorem :: LOPBAN10:34

    

     LM281: for F be FinSequence of REAL st for i be Element of ( dom F) holds 0 <= (F . i) & (F . i) <= 1 holds 0 <= ( Product F) & ( Product F) <= 1

    proof

      let F be FinSequence of REAL ;

      assume

       A1: for i be Element of ( dom F) holds 0 <= (F . i) & (F . i) <= 1;

      per cases ;

        suppose ex i be Nat st i in ( dom F) & (F . i) = 0 ;

        hence 0 <= ( Product F) & ( Product F) <= 1 by RVSUM_1: 103;

      end;

        suppose

         A2: not ex i be Nat st i in ( dom F) & (F . i) = 0 ;

        

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

        proof

          let k be Element of NAT ;

          assume

           A4: k in ( dom F);

          (F . k) <> 0 by A2, A4;

          hence (F . k) > 0 by A1, A4;

        end;

        hence 0 <= ( Product F) by NAT_4: 42;

        1 is Element of REAL by XREAL_0:def 1;

        then

        reconsider G = (( len F) |-> 1) as FinSequence of REAL by FINSEQ_2: 63;

        

         A6: ( len G) = ( len F) by CARD_1:def 7;

        for k be Element of NAT st k in ( dom F) holds (F . k) <= (G . k) & (F . k) > 0

        proof

          let k be Element of NAT ;

          assume

           A7: k in ( dom F);

          

           A9: k in ( Seg ( len F)) by A7, FINSEQ_1:def 3;

          (F . k) <= 1 by A1, A7;

          hence (F . k) <= (G . k) by A9, FINSEQ_2: 57;

          thus thesis by A3, A7;

        end;

        then ( Product F) <= ( Product G) by A6, NAT_4: 54;

        hence ( Product F) <= 1 by RVSUM_1: 102;

      end;

    end;

    theorem :: LOPBAN10:35

    

     LM28: for X be RealNormSpace-Sequence, x be Point of ( product X) st (for i be Element of ( dom X) holds ||.(x . i).|| <= 1) holds 0 <= ( NrProduct x) & ( NrProduct x) <= 1

    proof

      let X be RealNormSpace-Sequence, x be Point of ( product X);

      assume

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

      consider F be FinSequence of REAL such that

       A2: ( dom F) = ( dom X) & (for i be Element of ( dom X) holds (F . i) = ||.(x . i).||) & ( NrProduct x) = ( Product F) by DefNrPro;

      for i be Element of ( dom F) holds 0 <= (F . i) & (F . i) <= 1

      proof

        let i be Element of ( dom F);

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

        

         A3: (F . j) = ||.(x . j).|| by A2;

        thus 0 <= (F . i) by A3;

        thus (F . i) <= 1 by A1, A3;

      end;

      hence 0 <= ( NrProduct x) & ( NrProduct x) <= 1 by A2, LM281;

    end;

    

     LM31: 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 :: LOPBAN10:36

    

     LM32: for X be RealNormSpace-Sequence, Y be RealNormSpace, g be MultilinearOperator of X, Y, t be Point of ( product X) st ex i be Element of ( dom X) st (t . i) = ( 0. (X . i)) holds (g . t) = ( 0. Y)

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace, g be MultilinearOperator of X, Y, t be Point of ( product X);

      given i be Element of ( dom X) such that

       A2: (t . i) = ( 0. (X . i));

      

       A6: ((g * ( reproj (i,t))) . ( 0. (X . i))) = (g . (( reproj (i,t)) . ( 0. (X . i)))) by FUNCT_2: 15

      .= (g . t) by A2, Th4X;

      (g * ( reproj (i,t))) is LinearOperator of (X . i), Y by Def3;

      hence (g . t) = ( 0. Y) by A6, LOPBAN_7: 3;

    end;

    theorem :: LOPBAN10:37

    

     LM34: for X be RealNormSpace-Sequence, x be Point of ( product X) holds ex d be FinSequence of REAL st ( dom d) = ( dom X) & for i be Element of ( dom X) holds (d . i) = ( ||.(x . i).|| " )

    proof

      let X be RealNormSpace-Sequence, x be Point of ( product X);

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

      

       A4: 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 d = ( ||.(x . i).|| " ) as Element of REAL by XREAL_0:def 1;

        take d;

        thus P1[n, d];

      end;

      consider F be FinSequence of REAL such that

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

      take F;

      thus

       A6: ( dom F) = ( dom X) by A5, FINSEQ_3: 29;

      thus for i be Element of ( dom X) holds (F . i) = ( ||.(x . i).|| " )

      proof

        let i be Element of ( dom X);

        i in ( dom X);

        then

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

        reconsider n = i as Nat;

        consider j be Element of ( dom X) such that

         A8: n = j & (F /. n) = ( ||.(x . j).|| " ) by A5, A7;

        thus (F . i) = ( ||.(x . i).|| " ) by A6, A8, PARTFUN1:def 6;

      end;

    end;

    theorem :: LOPBAN10:38

    

     LM33: for X be RealNormSpace-Sequence, s be Point of ( product X), a be FinSequence of REAL holds ex s1 be Point of ( product X) st for i be Element of ( dom X) holds (s1 . i) = ((a /. i) * (s . i))

    proof

      let X be RealNormSpace-Sequence, x be Point of ( product X), a be FinSequence of REAL ;

      

       A4: ( dom ( carr X)) = ( dom X) by LemmaX;

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

      

       A5: 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;

        reconsider d = ((a /. i) * (x . i)) as Element of (X . i);

        take d;

        thus P1[n, d];

      end;

      consider F be FinSequence such that

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

      

       A7: ( dom F) = ( dom ( carr X)) by A4, A6, FINSEQ_1:def 3;

      for y be object st y in ( dom ( carr X)) holds (F . y) in (( carr X) . y)

      proof

        let y be object;

        assume

         A8: y in ( dom ( carr X));

        then

        reconsider n = y as Nat;

        consider i be Element of ( dom X) such that

         A9: n = i & (F . n) = ((a /. i) * (x . i)) by A6, A7, A8;

        (F . n) in the carrier of (X . i) by A9;

        hence (F . y) in (( carr X) . y) by A9, PRVECT_1:def 11;

      end;

      then

      reconsider F as Element of ( product ( carr X)) by A7, CARD_3:def 5;

      reconsider F as Element of ( product X) by EXTh10;

      take F;

      thus for i be Element of ( dom X) holds (F . i) = ((a /. i) * (x . i))

      proof

        let i be Element of ( dom X);

        i in ( dom X);

        then

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

        set n = i;

        consider j be Element of ( dom X) such that

         A11: n = j & (F . n) = ((a /. j) * (x . j)) by A6, A10;

        thus (F . i) = ((a /. i) * (x . i)) by A11;

      end;

    end;

    theorem :: LOPBAN10:39

    

     LM35: for X be RealNormSpace-Sequence, Y be RealNormSpace, g be MultilinearOperator of X, Y, a be FinSequence of REAL st ( dom a) = ( dom X) holds for t,t1 be Point of ( product X) st for i be Element of ( dom X) holds (t1 . i) = ((a /. i) * (t . i)) holds (g . t1) = (( Product a) * (g . t))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace, g be MultilinearOperator of X, Y, a be FinSequence of REAL ;

      assume

       A1: ( dom a) = ( dom X);

      

       A4: ( dom ( carr X)) = ( dom X) by LemmaX;

      

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

      defpred P[ Nat] means for t,t1 be Point of ( product X), b be FinSequence of REAL st b = (a | $1) & $1 <= ( len a) & (for i be Element of ( dom X) holds ((i in ( Seg $1) implies (t1 . i) = ((a /. i) * (t . i))) & ( not i in ( Seg $1) implies (t1 . i) = (t . i)))) holds (g . t1) = (( Product b) * (g . t));

      

       A6: P[ 0 ]

      proof

        let t,t1 be Point of ( product X), b be FinSequence of REAL ;

        assume

         A7: b = (a | 0 ) & 0 <= ( len a) & for i be Element of ( dom X) holds ((i in ( Seg 0 ) implies (t1 . i) = ((a /. i) * (t . i))) & ( not i in ( Seg 0 ) implies (t1 . i) = (t . i)));

        

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

        

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

        t1 = t by A4, A7, A10, A11;

        hence (g . t1) = (( Product b) * (g . t)) by A7, RLVECT_1:def 8, RVSUM_1: 94;

      end;

      

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

      proof

        let k be Nat;

        assume

         A16: P[k];

        let t,t1 be Point of ( product X), b be FinSequence of REAL ;

        assume

         A17: b = (a | (k + 1)) & (k + 1) <= ( len a) & for i be Element of ( dom X) holds ((i in ( Seg (k + 1)) implies (t1 . i) = ((a /. i) * (t . i))) & ( not i in ( Seg (k + 1)) implies (t1 . i) = (t . i)));

        reconsider b2 = (a | k) as FinSequence of REAL ;

        

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

        1 <= (k + 1) <= ( len a) by A17, NAT_1: 11;

        then

         B19: (k + 1) in ( Seg ( len a));

        then

         A20: (k + 1) in ( dom a) by FINSEQ_1:def 3;

        

         A22: b2 = (b | k) by A17, FINSEQ_1: 82, NAT_1: 11;

        

         A23: b = (b2 ^ <*(b . (k + 1))*>) by A17, A22, FINSEQ_1: 59, FINSEQ_3: 55

        .= (b2 ^ <*(a . (k + 1))*>) by A17, FINSEQ_1: 4, FUNCT_1: 49

        .= (b2 ^ <*(a /. (k + 1))*>) by A20, PARTFUN1:def 6;

        defpred LP1[ object] means $1 in ( Seg k);

        deffunc F1( Element of ( dom X)) = ((a /. $1) * (t . $1));

        deffunc F2( Element of ( dom X)) = (t . $1);

        consider s2 be Function such that

         A25: ( dom s2) = ( dom X) & for i be Element of ( dom X) holds ( LP1[i] implies (s2 . i) = F1(i)) & ( not LP1[i] implies (s2 . i) = F2(i)) from PARTFUN1:sch 4;

        for y be object st y in ( dom ( carr X)) holds (s2 . y) in (( carr X) . y)

        proof

          let y be object;

          assume y in ( dom ( carr X));

          then

          reconsider i = y as Element of ( dom X) by LemmaX;

          per cases ;

            suppose LP1[i];

            then (s2 . y) = ((a /. i) * (t . i)) by A25;

            then (s2 . y) in the carrier of (X . i);

            hence (s2 . y) in (( carr X) . y) by PRVECT_1:def 11;

          end;

            suppose not LP1[i];

            then (s2 . y) = (t . i) by A25;

            then (s2 . y) in the carrier of (X . i);

            hence (s2 . y) in (( carr X) . y) by PRVECT_1:def 11;

          end;

        end;

        then

        reconsider s2 as Element of ( product ( carr X)) by A4, A25, CARD_3:def 5;

        reconsider t2 = s2 as Point of ( product X) by A5;

        reconsider k1 = (k + 1) as Element of ( dom X) by A1, B19, FINSEQ_1:def 3;

        (k + 0 ) < (k + 1) by XREAL_1: 8;

        then not k1 in ( Seg k) by FINSEQ_1: 1;

        then

         A29: (s2 . k1) = (t . k1) by A25;

        

         A30: (g * ( reproj (k1,t2))) is LinearOperator of (X . k1), Y by Def3;

        set RK = (( reproj (k1,t2)) . ((a /. k1) * (t . k1)));

        

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

        

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

        reconsider RK as Function;

        for x be object st x in ( dom t1) holds (t1 . x) = (RK . x)

        proof

          let x be object;

          assume x in ( dom t1);

          then

          reconsider i = x as Element of ( dom X) by LemmaX, A31;

          

           A37: (i in ( Seg k) implies (s2 . i) = ((a /. i) * (t . i))) & ( not i in ( Seg k) implies (s2 . i) = (t . i)) by A25;

          per cases ;

            suppose

             A40: i in ( Seg (k + 1));

            per cases ;

              suppose

               A42: i = (k + 1);

              

              then (RK . i) = ((a /. k1) * (t . k1)) by Th3

              .= (t1 . i) by A17, A40, A42;

              hence (t1 . x) = (RK . x);

            end;

              suppose

               A43: i <> (k + 1);

              then

               A44: (RK . i) = (s2 . i) by Th4;

              1 <= i <= (k + 1) by A40, FINSEQ_1: 1;

              then 1 <= i & i < (k + 1) by A43, XXREAL_0: 1;

              then 1 <= i <= k by NAT_1: 13;

              hence (t1 . x) = (RK . x) by A17, A37, A40, A44;

            end;

          end;

            suppose

             A45: not i in ( Seg (k + 1));

            

             A46: 1 <= i <= ( len X) by FINSEQ_3: 25;

            

             A48: (k + 1) < i by A45, A46;

            then

             A49: (RK . i) = (s2 . i) by Th4;

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

            then k < i by A48, XXREAL_0: 2;

            hence (t1 . x) = (RK . x) by A17, A37, A45, A49, FINSEQ_1: 1;

          end;

        end;

        then

         A50: t1 = (( reproj (k1,t2)) . ((a /. k1) * (t . k1))) by A31, A32;

        

         A53: (g . t1) = ((g * ( reproj (k1,t2))) . ((a /. k1) * (t . k1))) by A50, FUNCT_2: 15

        .= ((a /. k1) * ((g * ( reproj (k1,t2))) . (t . k1))) by A30, LOPBAN_1:def 5

        .= ((a /. (k + 1)) * (g . (( reproj (k1,t2)) . (t . k1)))) by FUNCT_2: 15

        .= ((a /. (k + 1)) * (g . t2)) by A29, Th4X;

        

        thus (g . t1) = ((a /. (k + 1)) * (( Product b2) * (g . t))) by A16, A17, A18, A25, A53, XXREAL_0: 2

        .= (((a /. (k + 1)) * ( Product b2)) * (g . t)) by RLVECT_1:def 7

        .= (( Product b) * (g . t)) by A23, RVSUM_1: 96;

      end;

      

       A54: for k be Nat holds P[k] from NAT_1:sch 2( A6, A15);

      let t,t1 be Point of ( product X);

      assume

       A55: for i be Element of ( dom X) holds (t1 . i) = ((a /. i) * (t . i));

      set b = (a | ( len a));

      

       A56: b = a & ( len a) <= ( len a) by FINSEQ_2: 20;

      for i be Element of ( dom X) holds (i in ( Seg ( len a)) implies (t1 . i) = ((a /. i) * (t . i))) & ( not i in ( Seg ( len a)) implies (t1 . i) = (t . i))

      proof

        let i be Element of ( dom X);

        thus i in ( Seg ( len a)) implies (t1 . i) = ((a /. i) * (t . i)) by A55;

        thus not i in ( Seg ( len a)) implies (t1 . i) = (t . i)

        proof

          assume not i in ( Seg ( len a));

          then not i in ( dom X) by A1, FINSEQ_1:def 3;

          hence (t1 . i) = (t . i);

        end;

      end;

      hence (g . t1) = (( Product a) * (g . t)) by A54, A56;

    end;

    

     LM36A: for F,G be FinSequence of REAL st ( len F) = ( len G) & (for i be Element of NAT st i in ( dom F) holds (G . i) = ((F . i) " )) holds ( Product G) = (( Product F) " )

    proof

      let f1,f2 be FinSequence of REAL ;

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

      assume

       A1: ( len f1) = ( len f2);

      

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

      proof

        let n be Nat;

        assume

         A3: P[n];

        for f1,f2 be FinSequence of REAL st ( len f1) = ( len f2) & (n + 1) = ( len f1) & (for k be Element of NAT st k in ( dom f1) holds (f2 . k) = ((f1 . k) " )) holds ( Product f2) = (( Product f1) " )

        proof

          let f1,f2 be FinSequence of REAL ;

          assume that

           A4: ( len f1) = ( len f2) and

           A5: (n + 1) = ( len f1);

          consider g2 be FinSequence of REAL , r2 be Element of REAL such that

           A6: f2 = (g2 ^ <*r2*>) by A4, A5, FINSEQ_2: 19;

          ( len f2) = (( len g2) + ( len <*r2*>)) by A6, FINSEQ_1: 22;

          then

           A7: (n + 1) = (( len g2) + 1) by A4, A5, FINSEQ_1: 39;

          

           A8: ( Product f2) = (( Product g2) * r2) by A6, RVSUM_1: 96;

          consider g1 be FinSequence of REAL , r1 be Element of REAL such that

           A9: f1 = (g1 ^ <*r1*>) by A5, FINSEQ_2: 19;

          set k1 = (( len g1) + 1);

          

           A10: ( Product f1) = (( Product g1) * r1) by A9, RVSUM_1: 96;

          ( len f1) = (( len g1) + ( len <*r1*>)) by A9, FINSEQ_1: 22;

          then

           A11: (n + 1) = (( len g1) + 1) by A5, FINSEQ_1: 39;

          assume

           A12: for k be Element of NAT st k in ( dom f1) holds (f2 . k) = ((f1 . k) " );

           A13:

          now

            let k be Element of NAT ;

            

             A14: ( dom g1) c= ( dom f1) by A9, FINSEQ_1: 26;

            assume

             A15: k in ( dom g1);

            then k in ( Seg ( len g2)) by A7, A11, FINSEQ_1:def 3;

            then k in ( dom g2) by FINSEQ_1:def 3;

            then

             A16: (f2 . k) = (g2 . k) by A6, FINSEQ_1:def 7;

            (f1 . k) = (g1 . k) by A9, A15, FINSEQ_1:def 7;

            hence (g2 . k) = ((g1 . k) " ) by A12, A14, A15, A16;

          end;

          

           A17: ( Product g2) = (( Product g1) " ) by A3, A7, A11, A13;

          (n + 1) >= ( 0 + 1) by XREAL_1: 6;

          then k1 in ( Seg (n + 1)) by A11;

          then k1 in ( dom f1) by A5, FINSEQ_1:def 3;

          then

           A19: (f2 . k1) = ((f1 . k1) " ) by A12;

          r1 = (f1 . k1) & r2 = (f2 . k1) by A6, A7, A9, A11, FINSEQ_1: 42;

          hence ( Product f2) = (( Product f1) " ) by A8, A10, A17, A19, XCMPLX_1: 204;

        end;

        hence thesis;

      end;

      

       A21: P[ 0 ]

      proof

        let f1,f2 be FinSequence of REAL ;

        assume ( len f1) = ( len f2) & 0 = ( len f1) & (for k be Element of NAT st k in ( dom f1) holds (f2 . k) = ((f1 . k) " ));

        then f1 = {} & f2 = {} ;

        hence ( Product f2) = (( Product f1) " ) by RVSUM_1: 94;

      end;

      

       A25: for n be Nat holds P[n] from NAT_1:sch 2( A21, A2);

      assume for k be Element of NAT st k in ( dom f1) holds (f2 . k) = ((f1 . k) " );

      hence thesis by A1, A25;

    end;

    theorem :: LOPBAN10:40

    

     LM36: for F,G be FinSequence of REAL st ( dom F) = ( dom G) & (for i be Element of ( dom F) holds (G . i) = ((F . i) " )) holds ( Product G) = (( Product F) " )

    proof

      let F,G be FinSequence of REAL ;

      assume that

       A1: ( dom F) = ( dom G) and

       A2: for i be Element of ( dom F) holds (G . i) = ((F . i) " );

      

       A3: ( len F) = ( len G) by A1, FINSEQ_3: 29;

      for i be Element of NAT st i in ( dom F) holds (G . i) = ((F . i) " ) by A2;

      hence thesis by A3, LM36A;

    end;

    theorem :: LOPBAN10:41

    

     Th27: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for g be Lipschitzian MultilinearOperator of X, Y holds ( PreNorms g) is bounded_above

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let g be Lipschitzian MultilinearOperator of X, Y;

      consider K be Real such that

       A1: 0 <= K and

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

      take K;

      let r be ExtReal;

      assume r in ( PreNorms g);

      then

      consider t be VECTOR of ( product X) such that

       A3: r = ||.(g . t).|| and

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

      

       A5: ||.(g . t).|| <= (K * ( NrProduct t)) by A2;

       0 <= ( NrProduct t) & ( NrProduct t) <= 1 by A4, LM28;

      then (K * ( NrProduct t)) <= (K * 1) by A1, XREAL_1: 64;

      hence r <= K by A3, A5, XXREAL_0: 2;

    end;

    theorem :: LOPBAN10:42

    for X be RealNormSpace-Sequence, Y be RealNormSpace holds for g be MultilinearOperator of X, Y holds g is Lipschitzian iff ( PreNorms g) is bounded_above

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let g be MultilinearOperator of X, Y;

      now

        reconsider K = ( upper_bound ( PreNorms g)) as Real;

        assume

         A1: ( PreNorms g) is bounded_above;

         A2:

        now

          let t be VECTOR of ( product X);

          consider F be FinSequence of REAL such that

           A3: ( dom F) = ( dom X) & (for i be Element of ( dom X) holds (F . i) = ||.(t . i).||) & ( NrProduct t) = ( Product F) by DefNrPro;

          now

            per cases ;

              suppose ex i be Element of ( dom X) st (t . i) = ( 0. (X . i));

              then

              consider i be Element of ( dom X) such that

               A6: (t . i) = ( 0. (X . i));

              

               A7: (F . i) = ||.(t . i).|| by A3;

              (F . i) = 0 by A6, A7;

              then

               A10: ( Product F) = 0 by A3, RVSUM_1: 103;

              (g . t) = ( 0. Y) by A6, LM32;

              hence ||.(g . t).|| <= (K * ( NrProduct t)) by A3, A10;

            end;

              suppose

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

              

               A12: for i be Element of ( dom F) holds (F . i) > 0

              proof

                let i be Element of ( dom F);

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

                

                 A13: (F . j) = ||.(t . j).|| by A3;

                (t . j) <> ( 0. (X . j)) by A11;

                then (F . j) <> 0 by A13, NORMSP_0:def 5;

                hence thesis by A13;

              end;

              

               A15: 0 < ( Product F) by A12, LM31;

              consider d be FinSequence of REAL such that

               A16: ( dom d) = ( dom X) & for i be Element of ( dom X) holds (d . i) = ( ||.(t . i).|| " ) by LM34;

              consider t1 be Element of ( product X) such that

               A17: for i be Element of ( dom X) holds (t1 . i) = ((d /. i) * (t . i)) by LM33;

              

               A18: (( Product d) * (g . t)) = (g . t1) by A16, A17, LM35;

              

               A22: 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 A3;

                (d . j) = ( ||.(t . j).|| " ) by A16;

                hence thesis by A3;

              end;

              

               A23: ( |.( Product d).| * ||.(g . t).||) = ||.(g . t1).|| by A18, NORMSP_1:def 1;

               |.(( Product F) " ).| = |.(1 * (( Product F) " )).|

              .= |.(1 / ( Product F)).| by XCMPLX_0:def 9

              .= (1 / ( Product F)) by A15, ABSVALUE:def 1;

              

              then

               A25: ( |.( Product d).| * ||.(g . t).||) = ((1 / ( Product F)) * ||.(g . t).||) by A3, A16, A22, LM36

              .= ( ||.(g . t).|| / ( Product F)) by XCMPLX_1: 99;

              

               A26: for i be Element of ( dom X) holds ||.(t1 . i).|| <= 1

              proof

                let i be Element of ( dom X);

                

                 A27: (d . i) = ( ||.(t . i).|| " ) by A16;

                

                 A28: (t1 . i) = ((d /. i) * (t . i)) by A17;

                (t . i) <> ( 0. (X . i)) by A11;

                then

                 A29: ||.(t . i).|| <> 0 by NORMSP_0:def 5;

                 ||.(t1 . i).|| = ( |.(d /. i).| * ||.(t . i).||) by A28, NORMSP_1:def 1

                .= ( |.( ||.(t . i).|| " ).| * ||.(t . i).||) by A16, A27, PARTFUN1:def 6

                .= (( ||.(t . i).|| " ) * ||.(t . i).||) by ABSVALUE:def 1

                .= 1 by A29, XCMPLX_0:def 7;

                hence thesis;

              end;

               ||.(g . t1).|| in { ||.(g . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 } by A26;

              then ( ||.(g . t).|| / ( Product F)) <= K by A1, A23, A25, SEQ_4:def 1;

              then (( ||.(g . t).|| / ( Product F)) * ( Product F)) <= (K * ( Product F)) by A15, XREAL_1: 64;

              hence ||.(g . t).|| <= (K * ( NrProduct t)) by A3, A15, XCMPLX_1: 87;

            end;

          end;

          hence ||.(g . t).|| <= (K * ( NrProduct t));

        end;

        take K;

         0 <= K

        proof

          consider r0 be object such that

           A30: r0 in ( PreNorms g) by XBOOLE_0:def 1;

          reconsider r0 as Real by A30;

          now

            let r be Real;

            assume r in ( PreNorms g);

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

            hence 0 <= r;

          end;

          then 0 <= r0 by A30;

          hence thesis by A1, A30, SEQ_4:def 1;

        end;

        hence g is Lipschitzian by A2;

      end;

      hence thesis by Th27;

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def15

      func BoundedMultilinearOperatorsNorm (X,Y) -> Function of ( BoundedMultilinearOperators (X,Y)), REAL means

      : Def13: for x be object st x in ( BoundedMultilinearOperators (X,Y)) holds (it . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y))));

      existence

      proof

        deffunc F( object) = ( upper_bound ( PreNorms ( modetrans ($1,X,Y))));

        

         A1: for z be object st z in ( BoundedMultilinearOperators (X,Y)) holds F(z) in REAL by XREAL_0:def 1;

        thus ex f be Function of ( BoundedMultilinearOperators (X,Y)), REAL st for x be object st x in ( BoundedMultilinearOperators (X,Y)) holds (f . x) = F(x) from FUNCT_2:sch 2( A1);

      end;

      uniqueness

      proof

        let NORM1,NORM2 be Function of ( BoundedMultilinearOperators (X,Y)), REAL such that

         A2: for x be object st x in ( BoundedMultilinearOperators (X,Y)) holds (NORM1 . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y)))) and

         A3: for x be object st x in ( BoundedMultilinearOperators (X,Y)) holds (NORM2 . x) = ( upper_bound ( PreNorms ( modetrans (x,X,Y))));

        

         A4: for z be object st z in ( BoundedMultilinearOperators (X,Y)) holds (NORM1 . z) = (NORM2 . z)

        proof

          let z be object;

          assume

           A5: z in ( BoundedMultilinearOperators (X,Y));

          then (NORM1 . z) = ( upper_bound ( PreNorms ( modetrans (z,X,Y)))) by A2;

          hence thesis by A3, A5;

        end;

        ( dom NORM1) = ( BoundedMultilinearOperators (X,Y)) by FUNCT_2:def 1;

        hence thesis by A4, FUNCT_2:def 1;

      end;

    end

    

     Th29: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be Lipschitzian MultilinearOperator of X, Y holds ( modetrans (f,X,Y)) = f

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Lipschitzian MultilinearOperator of X, Y;

      f in ( BoundedMultilinearOperators (X,Y)) by Def9;

      hence thesis by Def11;

    end;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Lipschitzian MultilinearOperator of X, Y;

      reduce ( modetrans (f,X,Y)) to f;

      reducibility by Th29;

    end

    theorem :: LOPBAN10:43

    

     Th30: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be Lipschitzian MultilinearOperator of X, Y holds (( BoundedMultilinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms f))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Lipschitzian MultilinearOperator of X, Y;

      reconsider f9 = f as set;

      f in ( BoundedMultilinearOperators (X,Y)) by Def9;

      

      hence (( BoundedMultilinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms ( modetrans (f9,X,Y)))) by Def13

      .= ( upper_bound ( PreNorms f));

    end;

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      :: LOPBAN10:def16

      func R_NormSpace_of_BoundedMultilinearOperators (X,Y) -> non empty strict NORMSTR equals NORMSTR (# ( BoundedMultilinearOperators (X,Y)), ( Zero_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Add_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Mult_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( BoundedMultilinearOperatorsNorm (X,Y)) #);

      coherence ;

    end

    theorem :: LOPBAN10:44

    

     Th31: for X be RealNormSpace-Sequence, Y be RealNormSpace holds (the carrier of ( product X) --> ( 0. Y)) = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      (the carrier of ( product X) --> ( 0. Y)) = ( 0. ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y))) by Th26

      .= ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)));

      hence thesis;

    end;

    theorem :: LOPBAN10:45

    

     Th32: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds for g be Lipschitzian MultilinearOperator of X, Y st g = f holds for t be VECTOR of ( product X) holds ||.(g . t).|| <= ( ||.f.|| * ( NrProduct t))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      let g be Lipschitzian MultilinearOperator of X, Y such that

       A1: g = f;

      

       A2: ( PreNorms g) is non empty bounded_above by Th27;

      now

        let t be VECTOR of ( product X);

        consider F be FinSequence of REAL such that

         A3: ( dom F) = ( dom X) & (for i be Element of ( dom X) holds (F . i) = ||.(t . i).||) & ( NrProduct t) = ( Product F) by DefNrPro;

        now

          per cases ;

            suppose ex i be Element of ( dom X) st (t . i) = ( 0. (X . i));

            then

            consider i be Element of ( dom X) such that

             A7: (t . i) = ( 0. (X . i));

            (F . i) = ||.( 0. (X . i)).|| by A3, A7

            .= 0 ;

            then

             A9: ( Product F) = 0 by A3, RVSUM_1: 103;

            (g . t) = ( 0. Y) by A7, LM32;

            hence ||.(g . t).|| <= ( ||.f.|| * ( NrProduct t)) by A3, A9;

          end;

            suppose

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

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

            proof

              let i be Element of ( dom F);

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

              

               A12: (F . j) = ||.(t . j).|| by A3;

              (t . j) <> ( 0. (X . j)) by A10;

              then (F . j) <> 0 by A12, NORMSP_0:def 5;

              hence thesis by A12;

            end;

            then

             A13: 0 < ( Product F) by LM31;

            consider d be FinSequence of REAL such that

             A14: ( dom d) = ( dom X) & for i be Element of ( dom X) holds (d . i) = ( ||.(t . i).|| " ) by LM34;

            consider t1 be Element of ( product X) such that

             A15: for i be Element of ( dom X) holds (t1 . i) = ((d /. i) * (t . i)) by LM33;

            

             A16: for i be Element of ( dom X) holds ||.(t1 . i).|| <= 1

            proof

              let i be Element of ( dom X);

              

               A17: (d . i) = ( ||.(t . i).|| " ) by A14;

              

               A18: (t1 . i) = ((d /. i) * (t . i)) by A15;

              (t . i) <> ( 0. (X . i)) by A10;

              then

               A19: ||.(t . i).|| <> 0 by NORMSP_0:def 5;

               ||.(t1 . i).|| = ( |.(d /. i).| * ||.(t . i).||) by A18, NORMSP_1:def 1

              .= ( |.( ||.(t . i).|| " ).| * ||.(t . i).||) by A14, A17, PARTFUN1:def 6

              .= (( ||.(t . i).|| " ) * ||.(t . i).||) by ABSVALUE:def 1

              .= 1 by A19, XCMPLX_0:def 7;

              hence thesis;

            end;

            

             A20: (( Product d) * (g . t)) = (g . t1) by A14, A15, LM35;

            

             A23: 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 A3;

              (d . i) = ( ||.(t . j).|| " ) by A14;

              hence thesis by A3;

            end;

            

             A24: ( |.( Product d).| * ||.(g . t).||) = ||.(g . t1).|| by A20, NORMSP_1:def 1;

            

             A25: |.(( Product F) " ).| = |.(1 * (( Product F) " )).|

            .= |.(1 / ( Product F)).| by XCMPLX_0:def 9

            .= (1 / ( Product F)) by A13, ABSVALUE:def 1;

            

             A26: ( |.( Product d).| * ||.(g . t).||) = ((1 / ( Product F)) * ||.(g . t).||) by A3, A14, A23, A25, LM36

            .= ( ||.(g . t).|| / ( Product F)) by XCMPLX_1: 99;

             ||.(g . t1).|| in { ||.(g . t).|| where t be VECTOR of ( product X) : for i be Element of ( dom X) holds ||.(t . i).|| <= 1 } by A16;

            then ( ||.(g . t).|| / ( Product F)) <= ( upper_bound ( PreNorms g)) by A2, A24, A26, SEQ_4:def 1;

            then

             A28: ( ||.(g . t).|| / ( Product F)) <= ||.f.|| by A1, Th30;

            (( ||.(g . t).|| / ( Product F)) * ( Product F)) = ||.(g . t).|| by A13, XCMPLX_1: 87;

            hence ||.(g . t).|| <= ( ||.f.|| * ( NrProduct t)) by A3, A28, XREAL_1: 64;

          end;

        end;

        hence ||.(g . t).|| <= ( ||.f.|| * ( NrProduct t));

      end;

      hence thesis;

    end;

    theorem :: LOPBAN10:46

    

     Th33: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds 0 <= ||.f.||

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      reconsider g = f as Lipschitzian MultilinearOperator of X, Y by Def9;

      consider r0 be object such that

       A1: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A1;

      

       A2: ( PreNorms g) is non empty bounded_above by Th27;

      

       A3: (( BoundedMultilinearOperatorsNorm (X,Y)) . f) = ( upper_bound ( PreNorms g)) by Th30;

      now

        let r be Real;

        assume r in ( PreNorms g);

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

        hence 0 <= r;

      end;

      then 0 <= r0 by A1;

      hence thesis by A1, A2, A3, SEQ_4:def 1;

    end;

    theorem :: LOPBAN10:47

    

     Th34: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) st f = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y))) holds 0 = ||.f.||

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) such that

       A1: f = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)));

      reconsider g = f as Lipschitzian MultilinearOperator of X, Y by Def9;

      set z = (the carrier of ( product X) --> ( 0. Y));

      reconsider z as Function of the carrier of ( product X), the carrier of Y;

      consider r0 be object such that

       A2: r0 in ( PreNorms g) by XBOOLE_0:def 1;

      reconsider r0 as Real by A2;

      

       A3: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

      

       A4: ( PreNorms g) is non empty bounded_above by Th27;

      

       A5: z = g by A1, Th31;

       A6:

      now

        let r be Real;

        assume r in ( PreNorms g);

        then

        consider t be VECTOR of ( product X) such that

         A7: r = ||.(g . t).|| and for i be Element of ( dom X) holds ||.(t . i).|| <= 1;

         ||.(g . t).|| = ||.( 0. Y).|| by A5, FUNCOP_1: 7

        .= 0 ;

        hence 0 <= r & r <= 0 by A7;

      end;

      then 0 <= r0 by A2;

      then ( upper_bound ( PreNorms g)) = 0 by A6, A4, A2, A3, SEQ_4:def 1;

      hence thesis by Th30;

    end;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster -> Function-like Relation-like for Element of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      coherence ;

    end

    definition

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f be Element of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      let v be VECTOR of ( product X);

      :: original: .

      redefine

      func f . v -> VECTOR of Y ;

      coherence

      proof

        reconsider f as MultilinearOperator of X, Y by Def9;

        (f . v) is VECTOR of Y;

        hence thesis;

      end;

    end

    theorem :: LOPBAN10:48

    

     Th35: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,g,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds h = (f + g) iff for x be VECTOR of ( product X) holds (h . x) = ((f . x) + (g . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,g,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      reconsider f1 = f, g1 = g, h1 = h as VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      h = (f + g) iff h1 = (f1 + g1);

      hence thesis by Th24;

    end;

    theorem :: LOPBAN10:49

    

     Th36: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds for a be Real holds h = (a * f) iff for x be VECTOR of ( product X) holds (h . x) = (a * (f . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      let a be Real;

      reconsider f1 = f, h1 = h as VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

      h = (a * f) iff h1 = (a * f1);

      hence thesis by Th25;

    end;

    theorem :: LOPBAN10:50

    

     Th37: for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,g be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds for a be Real holds ( ||.f.|| = 0 iff f = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)))) & ||.(a * f).|| = ( |.a.| * ||.f.||) & ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,g be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      let a be Real;

       A2:

      now

        assume

         A3: f = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)));

        thus ||.f.|| = 0

        proof

          reconsider g = f as Lipschitzian MultilinearOperator of X, Y by Def9;

          set z = (the carrier of ( product X) --> ( 0. Y));

          reconsider z as Function of the carrier of ( product X), the carrier of Y;

          consider r0 be object such that

           A4: r0 in ( PreNorms g) by XBOOLE_0:def 1;

          reconsider r0 as Real by A4;

          

           A5: (for s be Real st s in ( PreNorms g) holds s <= 0 ) implies ( upper_bound ( PreNorms g)) <= 0 by SEQ_4: 45;

          

           A6: ( PreNorms g) is non empty bounded_above by Th27;

          

           A7: z = g by A3, Th31;

           A8:

          now

            let r be Real;

            assume r in ( PreNorms g);

            then

            consider t be VECTOR of ( product X) such that

             A9: r = ||.(g . t).|| and for i be Element of ( dom X) holds ||.(t . i).|| <= 1;

             ||.(g . t).|| = ||.( 0. Y).|| by A7, FUNCOP_1: 7

            .= 0 ;

            hence 0 <= r & r <= 0 by A9;

          end;

          then 0 <= r0 by A4;

          then ( upper_bound ( PreNorms g)) = 0 by A4, A5, A6, A8, SEQ_4:def 1;

          hence thesis by Th30;

        end;

      end;

      

       A11: ||.(f + g).|| <= ( ||.f.|| + ||.g.||)

      proof

        reconsider f1 = f, g1 = g, h1 = (f + g) as Lipschitzian MultilinearOperator of X, Y by Def9;

        

         A12: (for s be Real st s in ( PreNorms h1) holds s <= ( ||.f.|| + ||.g.||)) implies ( upper_bound ( PreNorms h1)) <= ( ||.f.|| + ||.g.||) by SEQ_4: 45;

         A13:

        now

          let t be VECTOR of ( product X);

          assume

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

          

           A15: 0 <= ( NrProduct t) & ( NrProduct t) <= 1 by A14, LM28;

           0 <= ||.g.|| by Th33;

          then

           A16: ( ||.g.|| * ( NrProduct t)) <= ( ||.g.|| * 1) by A15, XREAL_1: 64;

           0 <= ||.f.|| by Th33;

          then ( ||.f.|| * ( NrProduct t)) <= ( ||.f.|| * 1) by A15, XREAL_1: 64;

          then

           A17: (( ||.f.|| * ( NrProduct t)) + ( ||.g.|| * ( NrProduct t))) <= (( ||.f.|| * 1) + ( ||.g.|| * 1)) by A16, XREAL_1: 7;

          

           A18: ||.((f1 . t) + (g1 . t)).|| <= ( ||.(f1 . t).|| + ||.(g1 . t).||) by NORMSP_1:def 1;

          

           A19: ||.(g1 . t).|| <= ( ||.g.|| * ( NrProduct t)) by Th32;

           ||.(f1 . t).|| <= ( ||.f.|| * ( NrProduct t)) by Th32;

          then ( ||.(f1 . t).|| + ||.(g1 . t).||) <= (( ||.f.|| * ( NrProduct t)) + ( ||.g.|| * ( NrProduct t))) by A19, XREAL_1: 7;

          then

           A20: ( ||.(f1 . t).|| + ||.(g1 . t).||) <= ( ||.f.|| + ||.g.||) by A17, XXREAL_0: 2;

           ||.(h1 . t).|| = ||.((f1 . t) + (g1 . t)).|| by Th35;

          hence ||.(h1 . t).|| <= ( ||.f.|| + ||.g.||) by A18, A20, XXREAL_0: 2;

        end;

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then

          consider t be VECTOR of ( product X) such that

           A22: r = ||.(h1 . t).|| and

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

          thus r <= ( ||.f.|| + ||.g.||) by A13, A22, A23;

        end;

        hence thesis by A12, Th30;

      end;

      reconsider f1 = f, h1 = (a * f) as Lipschitzian MultilinearOperator of X, Y by Def9;

      

       A25: (for s be Real st s in ( PreNorms h1) holds s <= ( |.a.| * ||.f.||)) implies ( upper_bound ( PreNorms h1)) <= ( |.a.| * ||.f.||) by SEQ_4: 45;

      

       A24: ||.(a * f).|| = ( |.a.| * ||.f.||)

      proof

         A26:

        now

          

           A27: 0 <= ||.f.|| by Th33;

          let t be VECTOR of ( product X);

          assume

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

          ( NrProduct t) <= 1 by A28, LM28;

          then

           A29: ( ||.f.|| * ( NrProduct t)) <= ( ||.f.|| * 1) by A27, XREAL_1: 64;

           ||.(f1 . t).|| <= ( ||.f.|| * ( NrProduct t)) by Th32;

          then

           A30: ||.(f1 . t).|| <= ||.f.|| by A29, XXREAL_0: 2;

          

           A31: ||.(a * (f1 . t)).|| = ( |.a.| * ||.(f1 . t).||) by NORMSP_1:def 1;

          

           A32: 0 <= |.a.| by COMPLEX1: 46;

           ||.(h1 . t).|| = ||.(a * (f1 . t)).|| by Th36;

          hence ||.(h1 . t).|| <= ( |.a.| * ||.f.||) by A30, A31, A32, XREAL_1: 64;

        end;

         A33:

        now

          let r be Real;

          assume r in ( PreNorms h1);

          then

          consider t be VECTOR of ( product X) such that

           A34: r = ||.(h1 . t).|| and

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

          thus r <= ( |.a.| * ||.f.||) by A26, A34, A35;

        end;

         A36:

        now

          per cases ;

            case

             A37: a <> 0 ;

             A38:

            now

              

               A39: 0 <= ||.(a * f).|| by Th33;

              let t be VECTOR of ( product X);

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

              then ( NrProduct t) <= 1 by LM28;

              then

               A41: ( ||.(a * f).|| * ( NrProduct t)) <= ( ||.(a * f).|| * 1) by A39, XREAL_1: 64;

               ||.(h1 . t).|| <= ( ||.(a * f).|| * ( NrProduct t)) by Th32;

              then

               A42: ||.(h1 . t).|| <= ||.(a * f).|| by A41, XXREAL_0: 2;

              (h1 . t) = (a * (f1 . t)) by Th36;

              

              then

               A43: ((a " ) * (h1 . t)) = (((a " ) * a) * (f1 . t)) by RLVECT_1:def 7

              .= (1 * (f1 . t)) by A37, XCMPLX_0:def 7

              .= (f1 . t) by RLVECT_1:def 8;

              

               A44: |.(a " ).| = |.(1 * (a " )).|

              .= |.(1 / a).| by XCMPLX_0:def 9

              .= (1 / |.a.|) by ABSVALUE: 7

              .= (1 * ( |.a.| " )) by XCMPLX_0:def 9

              .= ( |.a.| " );

              

               A45: 0 <= |.(a " ).| by COMPLEX1: 46;

               ||.((a " ) * (h1 . t)).|| = ( |.(a " ).| * ||.(h1 . t).||) by NORMSP_1:def 1;

              hence ||.(f1 . t).|| <= (( |.a.| " ) * ||.(a * f).||) by A42, A43, A44, A45, XREAL_1: 64;

            end;

             A46:

            now

              let r be Real;

              assume r in ( PreNorms f1);

              then

              consider t be VECTOR of ( product X) such that

               A47: r = ||.(f1 . t).|| and

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

              thus r <= (( |.a.| " ) * ||.(a * f).||) by A38, A47, A48;

            end;

            

             A49: (for s be Real st s in ( PreNorms f1) holds s <= (( |.a.| " ) * ||.(a * f).||)) implies ( upper_bound ( PreNorms f1)) <= (( |.a.| " ) * ||.(a * f).||) by SEQ_4: 45;

            

             A50: 0 <= |.a.| by COMPLEX1: 46;

             ||.f.|| <= (( |.a.| " ) * ||.(a * f).||) by A46, A49, Th30;

            then ( |.a.| * ||.f.||) <= ( |.a.| * (( |.a.| " ) * ||.(a * f).||)) by A50, XREAL_1: 64;

            then

             A51: ( |.a.| * ||.f.||) <= (( |.a.| * ( |.a.| " )) * ||.(a * f).||);

             |.a.| <> 0 by A37, COMPLEX1: 47;

            then ( |.a.| * ||.f.||) <= (1 * ||.(a * f).||) by A51, XCMPLX_0:def 7;

            hence ( |.a.| * ||.f.||) <= ||.(a * f).||;

          end;

            case

             A52: a = 0 ;

            reconsider fz = f as VECTOR of ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y));

            

             A53: (a * f) = (a * fz)

            .= ( 0. ( R_VectorSpace_of_BoundedMultilinearOperators (X,Y))) by A52, RLVECT_1: 10

            .= ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)));

            

            thus ( |.a.| * ||.f.||) = ( 0 * ||.f.||) by A52, ABSVALUE: 2

            .= ||.(a * f).|| by A53, Th34;

          end;

        end;

         ||.(a * f).|| <= ( |.a.| * ||.f.||) by A25, A33, Th30;

        hence thesis by A36, XXREAL_0: 1;

      end;

      now

        reconsider g = f as Lipschitzian MultilinearOperator of X, Y by Def9;

        set z = (the carrier of ( product X) --> ( 0. Y));

        reconsider z as Function of the carrier of ( product X), the carrier of Y;

        assume

         A54: ||.f.|| = 0 ;

        now

          let t be VECTOR of ( product X);

           ||.(g . t).|| <= ( ||.f.|| * ( NrProduct t)) by Th32;

          then ||.(g . t).|| = 0 by A54;

          

          hence (g . t) = ( 0. Y) by NORMSP_0:def 5

          .= (z . t) by FUNCOP_1: 7;

        end;

        then g = z by FUNCT_2: 63;

        hence f = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y))) by Th31;

      end;

      hence thesis by A2, A11, A24;

    end;

    

     Th38: for X be RealNormSpace-Sequence, Y be RealNormSpace holds ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) is reflexive discerning RealNormSpace-like

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      thus ||.( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y))).|| = 0 by Th37;

      for x,y be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds for a be Real holds ( ||.x.|| = 0 iff x = ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)))) & ||.(a * x).|| = ( |.a.| * ||.x.||) & ||.(x + y).|| <= ( ||.x.|| + ||.y.||) by Th37;

      hence thesis by NORMSP_1:def 1, NORMSP_0:def 5;

    end;

    theorem :: LOPBAN10:51

    

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

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

       RLSStruct (# ( BoundedMultilinearOperators (X,Y)), ( Zero_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Add_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))), ( Mult_ (( BoundedMultilinearOperators (X,Y)),( R_VectorSpace_of_MultilinearOperators (X,Y)))) #) is RealLinearSpace;

      hence thesis by Th38, RSSPACE3: 2;

    end;

    registration

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      cluster ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) -> reflexive discerning RealNormSpace-like vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      coherence by Th39;

    end

    theorem :: LOPBAN10:52

    for X be RealNormSpace-Sequence, Y be RealNormSpace holds for f,g,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)) holds h = (f - g) iff for x be VECTOR of ( product X) holds (h . x) = ((f . x) - (g . x))

    proof

      let X be RealNormSpace-Sequence, Y be RealNormSpace;

      let f,g,h be Point of ( R_NormSpace_of_BoundedMultilinearOperators (X,Y));

      reconsider f9 = f, g9 = g, h9 = h as Lipschitzian MultilinearOperator of X, Y by Def9;

      hereby

        assume h = (f - g);

        then (h + g) = (f - (g - g)) by RLVECT_1: 29;

        then

         A1: (h + g) = (f - ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)))) by RLVECT_1: 15;

        now

          let x be VECTOR of ( product X);

          (f9 . x) = ((h9 . x) + (g9 . x)) by A1, Th35;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ((g9 . x) - (g9 . x))) by RLVECT_1:def 3;

          then ((f9 . x) - (g9 . x)) = ((h9 . x) + ( 0. Y)) by RLVECT_1: 15;

          hence ((f9 . x) - (g9 . x)) = (h9 . x);

        end;

        hence for x be VECTOR of ( product X) holds (h . x) = ((f . x) - (g . x));

      end;

      assume

       A2: for x be VECTOR of ( product X) holds (h . x) = ((f . x) - (g . x));

      now

        let x be VECTOR of ( product X);

        (h9 . x) = ((f9 . x) - (g9 . x)) by A2;

        then ((h9 . x) + (g9 . x)) = ((f9 . x) - ((g9 . x) - (g9 . x))) by RLVECT_1: 29;

        then ((h9 . x) + (g9 . x)) = ((f9 . x) - ( 0. Y)) by RLVECT_1: 15;

        hence ((h9 . x) + (g9 . x)) = (f9 . x);

      end;

      then f = (h + g) by Th35;

      then (f - g) = (h + (g - g)) by RLVECT_1:def 3;

      then (f - g) = (h + ( 0. ( R_NormSpace_of_BoundedMultilinearOperators (X,Y)))) by RLVECT_1: 15;

      hence thesis;

    end;