lopban12.miz



    begin

    reserve X,Y,Z,E,F,G,S,T for RealLinearSpace;

    registration

      let G be RealLinearSpace-Sequence;

      cluster ( product G) -> constituted-FinSeqs;

      coherence

      proof

        let a be Element of ( product G);

        ( product G) = RLSStruct (# ( product ( carr G)), ( zeros G), [:( addop G):], [:( multop G):] #) by PRVECT_2:def 9;

        hence thesis by NDIFF_5: 9;

      end;

    end

    theorem :: LOPBAN12:1

    

     LemmaA: for s be Element of ( product <*E, F*>), i be Element of ( dom <*E, F*>), x1 be object holds ( len (s +* (i,x1))) = 2

    proof

      let s be Element of ( product <*E, F*>), i be Element of ( dom <*E, F*>), x1 be object;

      consider x be Point of E, y be Point of F such that

       A3: s = <*x, y*> by PRVECT_3: 14;

      

       A1: ( len s) = 2 by A3, FINSEQ_1: 44;

      ( dom (s +* (i,x1))) = ( dom s) by FUNCT_7: 30

      .= ( Seg 2) by A1, FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: LOPBAN12:2

    

     NDIFF5def4: for G be RealLinearSpace-Sequence, i be Element of ( dom G), x be Element of ( product G) holds for r be Element of (G . i) holds (( reproj (i,x)) . r) = (x +* (i,r))

    proof

      let G be RealLinearSpace-Sequence, i be Element of ( dom G), x be Element of ( product G);

      ex x0 be Element of ( product ( carr G)) st x0 = x & ( reproj (i,x)) = ( reproj (i,x0)) by LOPBAN10:def 2;

      hence thesis by LOPBAN10:def 1;

    end;

    definition

      let X,Y be RealLinearSpace;

      :: LOPBAN12:def1

      func IsoCPRLSP (X,Y) -> LinearOperator of [:X, Y:], ( product <*X, Y*>) means

      : defISO: for x be Point of X, y be Point of Y holds (it . (x,y)) = <*x, y*>;

      existence

      proof

        consider I be Function of [:X, Y:], ( product <*X, Y*>) such that I is one-to-one onto and

         A1: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

         A2: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

         A3: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) by PRVECT_3: 12;

        reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A2, A3, LOPBAN_1:def 5, VECTSP_1:def 20;

        take I;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let I1,I2 be LinearOperator of [:X, Y:], ( product <*X, Y*>);

        assume that

         A4: for x be Point of X, y be Point of Y holds (I1 . (x,y)) = <*x, y*> and

         A5: for x be Point of X, y be Point of Y holds (I2 . (x,y)) = <*x, y*>;

        for x,y be set st x in the carrier of X & y in the carrier of Y holds (I1 . (x,y)) = (I2 . (x,y))

        proof

          let x,y be set;

          assume x in the carrier of X;

          then

          reconsider x1 = x as Point of X;

          assume y in the carrier of Y;

          then

          reconsider y1 = y as Point of Y;

          

          thus (I1 . (x,y)) = <*x1, y1*> by A4

          .= (I2 . (x,y)) by A5;

        end;

        hence I1 = I2 by BINOP_1:def 21;

      end;

    end

    theorem :: LOPBAN12:3

    

     ZeZe: for X,Y be RealLinearSpace holds ( 0. ( product <*X, Y*>)) = (( IsoCPRLSP (X,Y)) . ( 0. [:X, Y:]))

    proof

      let X,Y be RealLinearSpace;

      consider I be Function of [:X, Y:], ( product <*X, Y*>) such that I is one-to-one onto and

       A1: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

       A2: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

       A3: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and

       A4: ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) by PRVECT_3: 12;

      reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A2, A3, LOPBAN_1:def 5, VECTSP_1:def 20;

      for a be Element of X, b be Element of Y holds (I . (a,b)) = (( IsoCPRLSP (X,Y)) . (a,b)) by A1, defISO;

      hence thesis by A4, BINOP_1: 2;

    end;

    registration

      let X,Y be RealLinearSpace;

      cluster ( IsoCPRLSP (X,Y)) -> bijective;

      correctness

      proof

        consider I be Function of [:X, Y:], ( product <*X, Y*>) such that

         A1: I is one-to-one onto and

         A2: for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*> and

         A3: for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w)) and

         A4: for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v)) and ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) by PRVECT_3: 12;

        reconsider I as LinearOperator of [:X, Y:], ( product <*X, Y*>) by A3, A4, VECTSP_1:def 20, LOPBAN_1:def 5;

        for a be Element of X, b be Element of Y holds (I . (a,b)) = (( IsoCPRLSP (X,Y)) . (a,b)) by defISO, A2;

        hence thesis by A1, BINOP_1: 2;

      end;

    end

    registration

      let X,Y be RealLinearSpace;

      cluster bijective for LinearOperator of [:X, Y:], ( product <*X, Y*>);

      correctness

      proof

        take ( IsoCPRLSP (X,Y));

        thus thesis;

      end;

    end

    theorem :: LOPBAN12:4

    

     LM020: for I be LinearOperator of S, T st I is bijective holds ex J be LinearOperator of T, S st J = (I " ) & J is bijective

    proof

      let I be LinearOperator of S, T;

      assume

       A1: I is bijective;

      then

       a1: I is one-to-one onto;

      then

       A2: ( rng I) = the carrier of T & ( dom I) = the carrier of S by FUNCT_2:def 1;

      

       A3: ( rng I) = ( dom (I " )) & ( dom I) = ( rng (I " )) by A1, FUNCT_1: 33;

      then

      reconsider J = (I " ) as Function of T, S by A2, FUNCT_2: 1;

      

       A4: for v,w be Point of T holds (J . (v + w)) = ((J . v) + (J . w))

      proof

        let v,w be Point of T;

        consider t be Point of S such that

         A5: v = (I . t) by FUNCT_2: 113, a1;

        consider s be Point of S such that

         A6: w = (I . s) by FUNCT_2: 113, a1;

        

         A7: (J . (v + w)) = (J . (I . (t + s))) by A5, A6, VECTSP_1:def 20

        .= (t + s) by A1, A2, FUNCT_1: 34;

        (J . w) = s by A1, A2, A6, FUNCT_1: 34;

        hence thesis by A1, A2, A5, A7, FUNCT_1: 34;

      end;

      for v be Point of T, r be Real holds (J . (r * v)) = (r * (J . v))

      proof

        let v be Point of T, r be Real;

        consider t be Point of S such that

         A9: v = (I . t) by FUNCT_2: 113, a1;

        (J . (r * v)) = (J . (I . (r * t))) by A9, LOPBAN_1:def 5

        .= (r * t) by A1, A2, FUNCT_1: 34;

        hence thesis by A1, A2, A9, FUNCT_1: 34;

      end;

      then

      reconsider J as LinearOperator of T, S by A4, LOPBAN_1:def 5, VECTSP_1:def 20;

      take J;

      thus J = (I " );

      J is one-to-one onto by A1, A3, FUNCT_2:def 1;

      hence J is bijective;

    end;

    definition

      let X,Y be RealLinearSpace;

      let f be bijective LinearOperator of [:X, Y:], ( product <*X, Y*>);

      :: original: "

      redefine

      func f " -> LinearOperator of ( product <*X, Y*>), [:X, Y:] ;

      correctness

      proof

        ex J be LinearOperator of ( product <*X, Y*>), [:X, Y:] st J = (f " ) & J is bijective by LM020;

        hence thesis;

      end;

    end

    registration

      let X,Y be RealLinearSpace;

      let f be bijective LinearOperator of [:X, Y:], ( product <*X, Y*>);

      cluster (f " ) -> bijective;

      correctness

      proof

        ex J be LinearOperator of ( product <*X, Y*>), [:X, Y:] st J = (f " ) & J is bijective by LM020;

        hence thesis;

      end;

    end

    registration

      let X,Y be RealLinearSpace;

      cluster bijective for LinearOperator of ( product <*X, Y*>), [:X, Y:];

      correctness

      proof

        take (( IsoCPRLSP (X,Y)) " );

        thus thesis;

      end;

    end

    theorem :: LOPBAN12:5

    

     defISOA1: for X,Y be RealLinearSpace, x be Point of X, y be Point of Y holds ((( IsoCPRLSP (X,Y)) " ) . <*x, y*>) = [x, y]

    proof

      let X,Y be RealLinearSpace;

      set I = ( IsoCPRLSP (X,Y));

      set J = (I " );

      

       A1: ( dom I) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      let x be Point of X, y be Point of Y;

      

       A2: (I . (x,y)) = <*x, y*> by defISO;

      reconsider z = [x, y] as Point of [:X, Y:] by ZFMISC_1:def 2;

      (J . (I . z)) = z by A1, FUNCT_1: 34;

      hence thesis by A2;

    end;

    theorem :: LOPBAN12:6

    for X,Y be RealLinearSpace holds ((( IsoCPRLSP (X,Y)) " ) . ( 0. ( product <*X, Y*>))) = ( 0. [:X, Y:])

    proof

      let X,Y be RealLinearSpace;

      set I = ( IsoCPRLSP (X,Y));

      set J = (I " );

      

       A1: ( dom I) = the carrier of [:X, Y:] by FUNCT_2:def 1;

      (J . ( 0. ( product <*X, Y*>))) = (J . (I . ( 0. [:X, Y:]))) by ZeZe;

      hence thesis by A1, FUNCT_1: 34;

    end;

    theorem :: LOPBAN12:7

    

     IS01: for u be MultilinearOperator of <*E, F*>, G holds (u * ( IsoCPRLSP (E,F))) is BilinearOperator of E, F, G

    proof

      let u be MultilinearOperator of <*E, F*>, G;

      reconsider L = (u * ( IsoCPRLSP (E,F))) as Function of [:E, F:], G;

      ( dom <*E, F*>) = ( Seg ( len <*E, F*>)) by FINSEQ_1:def 3;

      then ( dom <*E, F*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

      then

      reconsider i1 = 1, i2 = 2 as Element of ( dom <*E, F*>) by TARSKI:def 2;

      

       A2: for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))

      proof

        let x1,x2 be Point of E, y be Point of F;

        set x = x1;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

        

         A3: ( <*E, F*> . i1) = E by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i1,xy))) as LinearOperator of E, G by LOPBAN10:def 3;

        

         A5: ( dom ( reproj (i1,xy))) = the carrier of ( <*E, F*> . i1) by FUNCT_2:def 1

        .= the carrier of E by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A7: i1 in ( dom xy) by TARSKI:def 2;

        then

         A14: ((xy +* (i1,x1)) . 1) = x1 by FUNCT_7: 31;

        

         A8: ( len (xy +* (i1,(x1 + x2)))) = 2 by LemmaA;

        

         A9: ((xy +* (i1,(x1 + x2))) . 1) = (x1 + x2) by A7, FUNCT_7: 31;

        

         A10: ((xy +* (i1,(x1 + x2))) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        reconsider x1x2 = (x1 + x2) as Element of ( <*E, F*> . i1) by FINSEQ_1: 44;

        

         A12: (( reproj (i1,xy)) . x1x2) = (xy +* (i1,(x1 + x2))) by NDIFF5def4

        .= <*(x1 + x2), y*> by A8, A9, A10, FINSEQ_1: 44;

        

         A13: ( len (xy +* (i1,x1))) = 2 by LemmaA;

        

         A15: ((xy +* (i1,x1)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A17: (( reproj (i1,xy)) . x1) = (xy +* (i1,x1)) by A3, NDIFF5def4

        .= <*x1, y*> by A13, A14, A15, FINSEQ_1: 44;

        

         A18: ( len (xy +* (i1,x2))) = 2 by LemmaA;

        

         A19: ((xy +* (i1,x2)) . 1) = x2 by A7, FUNCT_7: 31;

        

         A20: ((xy +* (i1,x2)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A22: (( reproj (i1,xy)) . x2) = (xy +* (i1,x2)) by A3, NDIFF5def4

        .= <*x2, y*> by A18, A19, A20, FINSEQ_1: 44;

         [(x1 + x2), y] is set & [x1, y] is set & [x2, y] is set by TARSKI: 1;

        then

         A4: [(x1 + x2), y] is Point of [:E, F:] & [x1, y] is Point of [:E, F:] & [x2, y] is Point of [:E, F:] by PRVECT_3: 9;

        

        then

         A23: (L . ((x1 + x2),y)) = (u . (( IsoCPRLSP (E,F)) . ((x1 + x2),y))) by FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . (x1 + x2))) by A12, defISO

        .= (L1 . (x1 + x2)) by A5, FUNCT_1: 13;

        

         A24: (L . (x1,y)) = (u . (( IsoCPRLSP (E,F)) . (x1,y))) by A4, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x1)) by A17, defISO

        .= (L1 . x1) by A5, FUNCT_1: 13;

        (L . (x2,y)) = (u . (( IsoCPRLSP (E,F)) . (x2,y))) by A4, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x2)) by A22, defISO

        .= (L1 . x2) by A5, FUNCT_1: 13;

        hence (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y))) by A23, A24, VECTSP_1:def 20;

      end;

      

       A26: for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))

      proof

        let x be Point of E, y be Point of F, a be Real;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

        

         A27: ( <*E, F*> . i1) = E by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i1,xy))) as LinearOperator of E, G by LOPBAN10:def 3;

        

         A29: ( dom ( reproj (i1,xy))) = the carrier of ( <*E, F*> . i1) by FUNCT_2:def 1

        .= the carrier of E by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A31: i1 in ( dom xy) by TARSKI:def 2;

        

         A32: ( len (xy +* (i1,(a * x)))) = 2 by LemmaA;

        

         A33: ((xy +* (i1,(a * x))) . 1) = (a * x) by A31, FUNCT_7: 31;

        

         A34: ((xy +* (i1,(a * x))) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        reconsider x1x2 = (a * x) as Element of ( <*E, F*> . i1) by FINSEQ_1: 44;

        

         A36: (( reproj (i1,xy)) . x1x2) = (xy +* (i1,(a * x))) by NDIFF5def4

        .= <*(a * x), y*> by A32, A33, A34, FINSEQ_1: 44;

        

         A37: ( len (xy +* (i1,x))) = 2 by LemmaA;

        

         A38: ((xy +* (i1,x)) . 1) = x by A31, FUNCT_7: 31;

        

         A39: ((xy +* (i1,x)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A41: (( reproj (i1,xy)) . x) = (xy +* (i1,x)) by A27, NDIFF5def4

        .= <*x, y*> by A37, A38, A39, FINSEQ_1: 44;

         [(a * x), y] is set & [x, y] is set by TARSKI: 1;

        then

         A28: [x, y] is Point of [:E, F:] & [(a * x), y] is Point of [:E, F:] by PRVECT_3: 9;

        

        then

         A42: (L . ((a * x),y)) = (u . (( IsoCPRLSP (E,F)) . ((a * x),y))) by FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . (a * x))) by A36, defISO

        .= (L1 . (a * x)) by A29, FUNCT_1: 13;

        (L . (x,y)) = (u . (( IsoCPRLSP (E,F)) . (x,y))) by A28, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x)) by A41, defISO

        .= (L1 . x) by A29, FUNCT_1: 13;

        hence (L . ((a * x),y)) = (a * (L . (x,y))) by A42, LOPBAN_1:def 5;

      end;

      

       A44: for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))

      proof

        let x be Point of E, y1,y2 be Point of F;

        reconsider xy = <*x, y1*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

        

         A45: ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i2,xy))) as LinearOperator of F, G by LOPBAN10:def 3;

        

         A47: ( dom ( reproj (i2,xy))) = the carrier of ( <*E, F*> . i2) by FUNCT_2:def 1

        .= the carrier of F by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A49: i2 in ( dom xy) by TARSKI:def 2;

        

         A50: ( len (xy +* (i2,(y1 + y2)))) = 2 by LemmaA;

        

         A51: ((xy +* (i2,(y1 + y2))) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A52: ((xy +* (i2,(y1 + y2))) . 2) = (y1 + y2) by A49, FUNCT_7: 31;

        reconsider x1x2 = (y1 + y2) as Element of ( <*E, F*> . i2) by FINSEQ_1: 44;

        

         A54: (( reproj (i2,xy)) . x1x2) = (xy +* (i2,(y1 + y2))) by NDIFF5def4

        .= <*x, (y1 + y2)*> by A50, A51, A52, FINSEQ_1: 44;

        

         A55: ( len (xy +* (i2,y1))) = 2 by LemmaA;

        

         A56: ((xy +* (i2,y1)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A57: ((xy +* (i2,y1)) . 2) = y1 by A49, FUNCT_7: 31;

        

         A59: (( reproj (i2,xy)) . y1) = (xy +* (i2,y1)) by A45, NDIFF5def4

        .= <*x, y1*> by A55, A56, A57, FINSEQ_1: 44;

        

         A60: ( len (xy +* (i2,y2))) = 2 by LemmaA;

        

         A61: ((xy +* (i2,y2)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A62: ((xy +* (i2,y2)) . 2) = y2 by A49, FUNCT_7: 31;

        

         A64: (( reproj (i2,xy)) . y2) = (xy +* (i2,y2)) by A45, NDIFF5def4

        .= <*x, y2*> by A60, A61, A62, FINSEQ_1: 44;

         [x, (y1 + y2)] is set & [x, y1] is set & [x, y2] is set by TARSKI: 1;

        then

         A46: [x, (y1 + y2)] is Point of [:E, F:] & [x, y1] is Point of [:E, F:] & [x, y2] is Point of [:E, F:] by PRVECT_3: 9;

        

        then

         A65: (L . (x,(y1 + y2))) = (u . (( IsoCPRLSP (E,F)) . (x,(y1 + y2)))) by FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . (y1 + y2))) by A54, defISO

        .= (L1 . (y1 + y2)) by A47, FUNCT_1: 13;

        

         A66: (L . (x,y1)) = (u . (( IsoCPRLSP (E,F)) . (x,y1))) by A46, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y1)) by A59, defISO

        .= (L1 . y1) by A47, FUNCT_1: 13;

        (L . (x,y2)) = (u . (( IsoCPRLSP (E,F)) . (x,y2))) by A46, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y2)) by A64, defISO

        .= (L1 . y2) by A47, FUNCT_1: 13;

        hence (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2))) by A65, A66, VECTSP_1:def 20;

      end;

      for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y)))

      proof

        let x be Point of E, y be Point of F, a be Real;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

        

         A68: ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i2,xy))) as LinearOperator of F, G by LOPBAN10:def 3;

        

         A70: ( dom ( reproj (i2,xy))) = the carrier of ( <*E, F*> . i2) by FUNCT_2:def 1

        .= the carrier of F by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A72: i2 in ( dom xy) by TARSKI:def 2;

        then

         A80: ((xy +* (i2,y)) . 2) = y by FUNCT_7: 31;

        

         A73: ( len (xy +* (i2,(a * y)))) = 2 by LemmaA;

        

         A74: ((xy +* (i2,(a * y))) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A75: ((xy +* (i2,(a * y))) . 2) = (a * y) by A72, FUNCT_7: 31;

        reconsider x1x2 = (a * y) as Element of ( <*E, F*> . i2) by FINSEQ_1: 44;

        

         A77: (( reproj (i2,xy)) . x1x2) = (xy +* (i2,(a * y))) by NDIFF5def4

        .= <*x, (a * y)*> by A73, A74, A75, FINSEQ_1: 44;

        

         A78: ( len (xy +* (i2,y))) = 2 by LemmaA;

        

         A79: ((xy +* (i2,y)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A82: (( reproj (i2,xy)) . y) = (xy +* (i2,y)) by A68, NDIFF5def4

        .= <*x, y*> by A78, A79, A80, FINSEQ_1: 44;

         [x, y] is set & [x, (a * y)] is set by TARSKI: 1;

        then

         A69: [x, y] is Point of [:E, F:] & [x, (a * y)] is Point of [:E, F:] by PRVECT_3: 9;

        

        then

         A83: (L . (x,(a * y))) = (u . (( IsoCPRLSP (E,F)) . (x,(a * y)))) by FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . (a * y))) by A77, defISO

        .= (L1 . (a * y)) by A70, FUNCT_1: 13;

        (L . (x,y)) = (u . (( IsoCPRLSP (E,F)) . (x,y))) by A69, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y)) by A82, defISO

        .= (L1 . y) by A70, FUNCT_1: 13;

        hence (L . (x,(a * y))) = (a * (L . (x,y))) by A83, LOPBAN_1:def 5;

      end;

      hence thesis by A2, A26, A44, LOPBAN_8: 11;

    end;

    theorem :: LOPBAN12:8

    

     IS02: for u be BilinearOperator of E, F, G holds (u * (( IsoCPRLSP (E,F)) " )) is MultilinearOperator of <*E, F*>, G

    proof

      let u be BilinearOperator of E, F, G;

      reconsider M = (u * (( IsoCPRLSP (E,F)) " )) as Function of ( product <*E, F*>), G;

      

       A1: ( dom <*E, F*>) = ( Seg ( len <*E, F*>)) by FINSEQ_1:def 3

      .= {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

      then

      reconsider i1 = 1, i2 = 2 as Element of ( dom <*E, F*>) by TARSKI:def 2;

      for i be Element of ( dom <*E, F*>), s be Element of ( product <*E, F*>) holds (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G

      proof

        let i be Element of ( dom <*E, F*>), s be Element of ( product <*E, F*>);

        consider x be Point of E, y be Point of F such that

         A3: s = <*x, y*> by PRVECT_3: 14;

        ( len s) = 2 by A3, FINSEQ_1: 44;

        then

         A5: ( dom s) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        per cases by A1, TARSKI:def 2;

          suppose

           A6: i = 1;

          then

           A7: ( <*E, F*> . i) = E by FINSEQ_1: 44;

          then

          reconsider L = (M * ( reproj (i,s))) as Function of E, G;

          

           A8: ( dom ( reproj (i,s))) = the carrier of ( <*E, F*> . i) by FUNCT_2:def 1

          .= the carrier of E by A6, FINSEQ_1: 44;

          

           A9: for z be Point of E holds (( reproj (i,s)) . z) = <*z, y*>

          proof

            let x1 be Point of E;

            

             A10: ( len (s +* (i,x1))) = 2 by LemmaA;

            

             A11: ((s +* (i,x1)) . 1) = x1 by A1, A5, A6, FUNCT_7: 31;

            

             A12: ((s +* (i,x1)) . 2) = (s . 2) by A6, FUNCT_7: 32

            .= y by A3, FINSEQ_1: 44;

            

            thus (( reproj (i,s)) . x1) = (s +* (i,x1)) by A7, NDIFF5def4

            .= <*x1, y*> by A10, A11, A12, FINSEQ_1: 44;

          end;

          

           A14: for x1,x2 be Point of E holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

          proof

            let x1,x2 be Point of E;

            reconsider x1y = <*x1, y*>, x2y = <*x2, y*>, x12y = <*(x1 + x2), y*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

            

             A18: (L . x1) = (M . (( reproj (i,s)) . x1)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x1, y*>) by A9

            .= (u . ((( IsoCPRLSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x1,y)) by defISOA1;

            

             A19: (L . x2) = (M . (( reproj (i,s)) . x2)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x2, y*>) by A9

            .= (u . ((( IsoCPRLSP (E,F)) " ) . x2y)) by FUNCT_2: 15

            .= (u . (x2,y)) by defISOA1;

            (L . (x1 + x2)) = (M . (( reproj (i,s)) . (x1 + x2))) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*(x1 + x2), y*>) by A9

            .= (u . ((( IsoCPRLSP (E,F)) " ) . x12y)) by FUNCT_2: 15

            .= (u . ((x1 + x2),y)) by defISOA1;

            hence (L . (x1 + x2)) = ((L . x1) + (L . x2)) by A18, A19, LOPBAN_8: 11;

          end;

          for x1 be Point of E, a be Real holds (L . (a * x1)) = (a * (L . x1))

          proof

            let x1 be Point of E, a be Real;

            reconsider ax1y = <*(a * x1), y*>, x1y = <*x1, y*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

            

             A23: (L . x1) = (M . (( reproj (i,s)) . x1)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x1, y*>) by A9

            .= (u . ((( IsoCPRLSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x1,y)) by defISOA1;

            (L . (a * x1)) = (M . (( reproj (i,s)) . (a * x1))) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*(a * x1), y*>) by A9

            .= (u . ((( IsoCPRLSP (E,F)) " ) . ax1y)) by FUNCT_2: 15

            .= (u . ((a * x1),y)) by defISOA1;

            hence (L . (a * x1)) = (a * (L . x1)) by A23, LOPBAN_8: 11;

          end;

          hence (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G by A7, A14, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

          suppose

           A25: i = 2;

          then

           A26: ( <*E, F*> . i) = F by FINSEQ_1: 44;

          then

          reconsider L = (M * ( reproj (i,s))) as Function of F, G;

          

           A27: ( dom ( reproj (i,s))) = the carrier of ( <*E, F*> . i) by FUNCT_2:def 1

          .= the carrier of F by A25, FINSEQ_1: 44;

          

           A28: for z be Point of F holds (( reproj (i,s)) . z) = <*x, z*>

          proof

            let y1 be Point of F;

            

             A29: ( len (s +* (i,y1))) = 2 by LemmaA;

            

             A30: ((s +* (i,y1)) . 2) = y1 by A1, A5, A25, FUNCT_7: 31;

            

             A31: ((s +* (i,y1)) . 1) = (s . 1) by A25, FUNCT_7: 32

            .= x by A3, FINSEQ_1: 44;

            

            thus (( reproj (i,s)) . y1) = (s +* (i,y1)) by A26, NDIFF5def4

            .= <*x, y1*> by A29, A30, A31, FINSEQ_1: 44;

          end;

          

           A33: for y1,y2 be Point of F holds (L . (y1 + y2)) = ((L . y1) + (L . y2))

          proof

            let y1,y2 be Point of F;

            reconsider y1y = <*x, y1*>, y2y = <*x, y2*>, y12y = <*x, (y1 + y2)*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

            

             A37: (L . y1) = (M . (( reproj (i,s)) . y1)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x, y1*>) by A28

            .= (u . ((( IsoCPRLSP (E,F)) " ) . y1y)) by FUNCT_2: 15

            .= (u . (x,y1)) by defISOA1;

            

             A38: (L . y2) = (M . (( reproj (i,s)) . y2)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x, y2*>) by A28

            .= (u . ((( IsoCPRLSP (E,F)) " ) . y2y)) by FUNCT_2: 15

            .= (u . (x,y2)) by defISOA1;

            (L . (y1 + y2)) = (M . (( reproj (i,s)) . (y1 + y2))) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x, (y1 + y2)*>) by A28

            .= (u . ((( IsoCPRLSP (E,F)) " ) . y12y)) by FUNCT_2: 15

            .= (u . (x,(y1 + y2))) by defISOA1;

            hence (L . (y1 + y2)) = ((L . y1) + (L . y2)) by A37, A38, LOPBAN_8: 11;

          end;

          for y1 be Point of F, a be Real holds (L . (a * y1)) = (a * (L . y1))

          proof

            let y1 be Point of F, a be Real;

            reconsider ax1y = <*x, (a * y1)*>, x1y = <*x, y1*> as Point of ( product <*E, F*>) by PRVECT_3: 14;

            

             A42: (L . y1) = (M . (( reproj (i,s)) . y1)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x, y1*>) by A28

            .= (u . ((( IsoCPRLSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x,y1)) by defISOA1;

            (L . (a * y1)) = (M . (( reproj (i,s)) . (a * y1))) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPRLSP (E,F)) " )) . <*x, (a * y1)*>) by A28

            .= (u . ((( IsoCPRLSP (E,F)) " ) . ax1y)) by FUNCT_2: 15

            .= (u . (x,(a * y1))) by defISOA1;

            hence (L . (a * y1)) = (a * (L . y1)) by A42, LOPBAN_8: 11;

          end;

          hence (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G by A26, A33, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

      end;

      hence thesis by LOPBAN10:def 3;

    end;

    theorem :: LOPBAN12:9

    

     IS03: ex I be LinearOperator of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)), ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z)) st I is bijective & for u be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds (I . u) = (u * (( IsoCPRLSP (X,Y)) " ))

    proof

      set F1 = the carrier of ( R_VectorSpace_of_BilinearOperators (X,Y,Z));

      set F2 = the carrier of ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z));

      defpred P1[ Function, Function] means $2 = ($1 * (( IsoCPRLSP (X,Y)) " ));

      

       A1: for x be Element of F1 holds ex y be Element of F2 st P1[x, y]

      proof

        let x be Element of F1;

        reconsider u = x as BilinearOperator of X, Y, Z by LOPBAN_9:def 1;

        (u * (( IsoCPRLSP (X,Y)) " )) is MultilinearOperator of <*X, Y*>, Z by IS02;

        then

        reconsider v = (u * (( IsoCPRLSP (X,Y)) " )) as Element of F2 by LOPBAN10:def 4;

        take v;

        thus thesis;

      end;

      consider I be Function of F1, F2 such that

       A2: for x be Element of F1 holds P1[x, (I . x)] from FUNCT_2:sch 3( A1);

      

       A3: for x1,x2 be object st x1 in F1 & x2 in F1 & (I . x1) = (I . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A4: x1 in F1 & x2 in F1 & (I . x1) = (I . x2);

        then

        reconsider u1 = x1, u2 = x2 as Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z));

        reconsider v1 = u1, v2 = u2 as BilinearOperator of X, Y, Z by LOPBAN_9:def 1;

        (I . v1) = (v1 * (( IsoCPRLSP (X,Y)) " )) by A2;

        then (v1 * (( IsoCPRLSP (X,Y)) " )) = (v2 * (( IsoCPRLSP (X,Y)) " )) by A2, A4;

        then (v1 * ((( IsoCPRLSP (X,Y)) " ) * ( IsoCPRLSP (X,Y)))) = ((v2 * (( IsoCPRLSP (X,Y)) " )) * ( IsoCPRLSP (X,Y))) by RELAT_1: 36;

        then

         A6: (v1 * ((( IsoCPRLSP (X,Y)) " ) * ( IsoCPRLSP (X,Y)))) = (v2 * ((( IsoCPRLSP (X,Y)) " ) * ( IsoCPRLSP (X,Y)))) by RELAT_1: 36;

        ( IsoCPRLSP (X,Y)) is one-to-one & ( rng ( IsoCPRLSP (X,Y))) = the carrier of ( product <*X, Y*>) by FUNCT_2:def 3;

        then

         A7: ((( IsoCPRLSP (X,Y)) " ) * ( IsoCPRLSP (X,Y))) = ( id [:X, Y:]) by FUNCT_2: 29;

        then (v1 * ((( IsoCPRLSP (X,Y)) " ) * ( IsoCPRLSP (X,Y)))) = v1 by FUNCT_2: 17;

        hence thesis by A6, A7, FUNCT_2: 17;

      end;

      

       A9: for y be object st y in F2 holds ex x be object st x in F1 & y = (I . x)

      proof

        let y be object;

        assume y in F2;

        then

        reconsider u = y as Point of ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z));

        reconsider u1 = u as MultilinearOperator of <*X, Y*>, Z by LOPBAN10:def 4;

        reconsider v1 = (u1 * ( IsoCPRLSP (X,Y))) as BilinearOperator of X, Y, Z by IS01;

        reconsider v = v1 as Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)) by LOPBAN_9:def 1;

        take v;

        thus v in F1;

        ( IsoCPRLSP (X,Y)) is one-to-one & ( rng ( IsoCPRLSP (X,Y))) = the carrier of ( product <*X, Y*>) by FUNCT_2:def 3;

        then

         A10: (( IsoCPRLSP (X,Y)) * (( IsoCPRLSP (X,Y)) " )) = ( id ( product <*X, Y*>)) by FUNCT_2: 29;

        

        thus (I . v) = ((u1 * ( IsoCPRLSP (X,Y))) * (( IsoCPRLSP (X,Y)) " )) by A2

        .= (u1 * (( IsoCPRLSP (X,Y)) * (( IsoCPRLSP (X,Y)) " ))) by RELAT_1: 36

        .= y by A10, FUNCT_2: 17;

      end;

      

       A12: for x,y be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds (I . (x + y)) = ((I . x) + (I . y))

      proof

        let x,y be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z));

        

         A13: (I . x) = (x * (( IsoCPRLSP (X,Y)) " )) by A2;

        

         A14: (I . y) = (y * (( IsoCPRLSP (X,Y)) " )) by A2;

        

         A15: (I . (x + y)) = ((x + y) * (( IsoCPRLSP (X,Y)) " )) by A2;

        reconsider f = (I . x), g = (I . y), h = (I . (x + y)) as Point of ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z));

        for xy be VECTOR of ( product <*X, Y*>) holds (h . xy) = ((f . xy) + (g . xy))

        proof

          let xy be VECTOR of ( product <*X, Y*>);

          consider p be Point of X, q be Point of Y such that

           A16: xy = <*p, q*> by PRVECT_3: 14;

          

           A17: (f . xy) = (x . ((( IsoCPRLSP (X,Y)) " ) . xy)) by A13, FUNCT_2: 15

          .= (x . (p,q)) by A16, defISOA1;

          

           A18: (g . xy) = (y . ((( IsoCPRLSP (X,Y)) " ) . xy)) by A14, FUNCT_2: 15

          .= (y . (p,q)) by A16, defISOA1;

          (h . xy) = ((x + y) . ((( IsoCPRLSP (X,Y)) " ) . xy)) by A15, FUNCT_2: 15

          .= ((x + y) . (p,q)) by A16, defISOA1;

          hence (h . xy) = ((f . xy) + (g . xy)) by A17, A18, LOPBAN_9: 2;

        end;

        hence thesis by LOPBAN10: 11;

      end;

      for x be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)), a be Real holds (I . (a * x)) = (a * (I . x))

      proof

        let x be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)), a be Real;

        

         A20: (I . x) = (x * (( IsoCPRLSP (X,Y)) " )) by A2;

        

         A21: (I . (a * x)) = ((a * x) * (( IsoCPRLSP (X,Y)) " )) by A2;

        reconsider f = (I . x), g = (I . (a * x)) as Point of ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z));

        for xy be VECTOR of ( product <*X, Y*>) holds (g . xy) = (a * (f . xy))

        proof

          let xy be VECTOR of ( product <*X, Y*>);

          consider p be Point of X, q be Point of Y such that

           A22: xy = <*p, q*> by PRVECT_3: 14;

          

           A23: (f . xy) = (x . ((( IsoCPRLSP (X,Y)) " ) . xy)) by A20, FUNCT_2: 15

          .= (x . (p,q)) by A22, defISOA1;

          (g . xy) = ((a * x) . ((( IsoCPRLSP (X,Y)) " ) . xy)) by A21, FUNCT_2: 15

          .= ((a * x) . (p,q)) by A22, defISOA1;

          hence (g . xy) = (a * (f . xy)) by A23, LOPBAN_9: 3;

        end;

        hence thesis by LOPBAN10: 12;

      end;

      then

      reconsider I as LinearOperator of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)), ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;

      take I;

      I is one-to-one onto by A3, A9, FUNCT_2: 10, FUNCT_2: 19;

      hence thesis by A2;

    end;

    theorem :: LOPBAN12:10

    ex I be LinearOperator of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z)))), ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z)) st I is bijective & for u be Point of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z)))) holds for x be Point of X, y be Point of Y holds ((I . u) . <*x, y*>) = ((u . x) . y)

    proof

      consider I be LinearOperator of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z)))), ( R_VectorSpace_of_BilinearOperators (X,Y,Z)) such that

       A1: I is bijective & for u be Point of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z)))) holds for x be Point of X, y be Point of Y holds ((I . u) . (x,y)) = ((u . x) . y) by LOPBAN_9: 26;

      consider J be LinearOperator of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)), ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z)) such that

       A2: J is bijective & for u be Point of ( R_VectorSpace_of_BilinearOperators (X,Y,Z)) holds (J . u) = (u * (( IsoCPRLSP (X,Y)) " )) by IS03;

      reconsider K = (J * I) as LinearOperator of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z)))), ( R_VectorSpace_of_MultilinearOperators ( <*X, Y*>,Z)) by LOPBAN_2: 1;

      take K;

      thus K is bijective by A1, A2, FUNCT_2: 27;

      let u be Point of ( R_VectorSpace_of_LinearOperators (X,( R_VectorSpace_of_LinearOperators (Y,Z))));

      let x be Point of X, y be Point of Y;

      

       A3: (K . u) = (J . (I . u)) by FUNCT_2: 15;

      reconsider xy = <*x, y*> as Point of ( product <*X, Y*>) by PRVECT_3: 14;

      

      thus ((K . u) . <*x, y*>) = (((I . u) * (( IsoCPRLSP (X,Y)) " )) . xy) by A2, A3

      .= ((I . u) . ((( IsoCPRLSP (X,Y)) " ) . xy)) by FUNCT_2: 15

      .= ((I . u) . (x,y)) by defISOA1

      .= ((u . x) . y) by A1;

    end;

    begin

    reserve X,Y,Z,E,F,G for RealNormSpace;

    reserve S,T for RealNormSpace-Sequence;

    theorem :: LOPBAN12:11

    

     LemmaA: for s be Point of ( product <*E, F*>), i be Element of ( dom <*E, F*>), x1 be object holds ( len (s +* (i,x1))) = 2

    proof

      let s be Point of ( product <*E, F*>), i be Element of ( dom <*E, F*>), x1 be object;

      consider x be Point of E, y be Point of F such that

       A3: s = <*x, y*> by PRVECT_3: 19;

      

       A1: ( len s) = 2 by FINSEQ_1: 44, A3;

      ( dom (s +* (i,x1))) = ( dom s) by FUNCT_7: 30

      .= ( Seg 2) by A1, FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: LOPBAN12:12

    

     IS01A: for u be Lipschitzian MultilinearOperator of <*E, F*>, G holds (u * ( IsoCPNrSP (E,F))) is Lipschitzian BilinearOperator of E, F, G

    proof

      let u be Lipschitzian MultilinearOperator of <*E, F*>, G;

      reconsider L = (u * ( IsoCPNrSP (E,F))) as Function of [:E, F:], G;

      ( dom <*E, F*>) = ( Seg ( len <*E, F*>)) by FINSEQ_1:def 3

      .= {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

      then

      reconsider i1 = 1, i2 = 2 as Element of ( dom <*E, F*>) by TARSKI:def 2;

      

       A2: for x1,x2 be Point of E, y be Point of F holds (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y)))

      proof

        let x1,x2 be Point of E, y be Point of F;

        reconsider xy = <*x1, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

        

         A3: ( <*E, F*> . i1) = E by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i1,xy))) as LinearOperator of E, G by LOPBAN10:def 6;

        

         A5: ( dom ( reproj (i1,xy))) = the carrier of ( <*E, F*> . i1) by FUNCT_2:def 1

        .= the carrier of E by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A7: i1 in ( dom xy) by TARSKI:def 2;

        

         A8: ( len (xy +* (i1,(x1 + x2)))) = 2 by LemmaA;

        

         A9: ((xy +* (i1,(x1 + x2))) . 1) = (x1 + x2) by A7, FUNCT_7: 31;

        

         A10: ((xy +* (i1,(x1 + x2))) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        reconsider x1x2 = (x1 + x2) as Element of ( <*E, F*> . i1) by FINSEQ_1: 44;

        

         A12: (( reproj (i1,xy)) . x1x2) = (xy +* (i1,(x1 + x2))) by NDIFF_5:def 4

        .= <*(x1 + x2), y*> by A8, A9, A10, FINSEQ_1: 44;

        

         A13: ( len (xy +* (i1,x1))) = 2 by LemmaA;

        

         A14: ((xy +* (i1,x1)) . 1) = x1 by A7, FUNCT_7: 31;

        

         A15: ((xy +* (i1,x1)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A17: (( reproj (i1,xy)) . x1) = (xy +* (i1,x1)) by A3, NDIFF_5:def 4

        .= <*x1, y*> by A13, A14, A15, FINSEQ_1: 44;

        

         A18: ( len (xy +* (i1,x2))) = 2 by LemmaA;

        

         A19: ((xy +* (i1,x2)) . 1) = x2 by A7, FUNCT_7: 31;

        

         A20: ((xy +* (i1,x2)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A22: (( reproj (i1,xy)) . x2) = (xy +* (i1,x2)) by A3, NDIFF_5:def 4

        .= <*x2, y*> by A18, A19, A20, FINSEQ_1: 44;

         [(x1 + x2), y] is set & [x1, y] is set & [x2, y] is set by TARSKI: 1;

        then

         A4: [(x1 + x2), y] is Point of [:E, F:] & [x1, y] is Point of [:E, F:] & [x2, y] is Point of [:E, F:] by PRVECT_3: 18;

        

        then

         A23: (L . ((x1 + x2),y)) = (u . (( IsoCPNrSP (E,F)) . ((x1 + x2),y))) by FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . (x1 + x2))) by A12, NDIFF_7:def 3

        .= (L1 . (x1 + x2)) by A5, FUNCT_1: 13;

        

         A24: (L . (x1,y)) = (u . (( IsoCPNrSP (E,F)) . (x1,y))) by A4, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x1)) by A17, NDIFF_7:def 3

        .= (L1 . x1) by A5, FUNCT_1: 13;

        (L . (x2,y)) = (u . (( IsoCPNrSP (E,F)) . (x2,y))) by A4, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x2)) by A22, NDIFF_7:def 3

        .= (L1 . x2) by A5, FUNCT_1: 13;

        hence (L . ((x1 + x2),y)) = ((L . (x1,y)) + (L . (x2,y))) by A23, A24, VECTSP_1:def 20;

      end;

      

       A26: for x be Point of E, y be Point of F, a be Real holds (L . ((a * x),y)) = (a * (L . (x,y)))

      proof

        let x be Point of E, y be Point of F, a be Real;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

        

         A27: ( <*E, F*> . i1) = E by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i1,xy))) as LinearOperator of E, G by LOPBAN10:def 6;

        

         A29: ( dom ( reproj (i1,xy))) = the carrier of ( <*E, F*> . i1) by FUNCT_2:def 1

        .= the carrier of E by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A31: i1 in ( dom xy) by TARSKI:def 2;

        

         A32: ( len (xy +* (i1,(a * x)))) = 2 by LemmaA;

        

         A33: ((xy +* (i1,(a * x))) . 1) = (a * x) by A31, FUNCT_7: 31;

        

         A34: ((xy +* (i1,(a * x))) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        reconsider x1x2 = (a * x) as Element of ( <*E, F*> . i1) by FINSEQ_1: 44;

        

         A36: (( reproj (i1,xy)) . x1x2) = (xy +* (i1,(a * x))) by NDIFF_5:def 4

        .= <*(a * x), y*> by A32, A33, A34, FINSEQ_1: 44;

        

         A37: ( len (xy +* (i1,x))) = 2 by LemmaA;

        

         A38: ((xy +* (i1,x)) . 1) = x by A31, FUNCT_7: 31;

        

         A39: ((xy +* (i1,x)) . 2) = (xy . i2) by FUNCT_7: 32

        .= y by FINSEQ_1: 44;

        

         A41: (( reproj (i1,xy)) . x) = (xy +* (i1,x)) by A27, NDIFF_5:def 4

        .= <*x, y*> by A37, A38, A39, FINSEQ_1: 44;

         [(a * x), y] is set & [x, y] is set by TARSKI: 1;

        then

         A28: [x, y] is Point of [:E, F:] & [(a * x), y] is Point of [:E, F:] by PRVECT_3: 18;

        

        then

         A42: (L . ((a * x),y)) = (u . (( IsoCPNrSP (E,F)) . ((a * x),y))) by FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . (a * x))) by A36, NDIFF_7:def 3

        .= (L1 . (a * x)) by A29, FUNCT_1: 13;

        (L . (x,y)) = (u . (( IsoCPNrSP (E,F)) . (x,y))) by A28, FUNCT_2: 15

        .= (u . (( reproj (i1,xy)) . x)) by A41, NDIFF_7:def 3

        .= (L1 . x) by A29, FUNCT_1: 13;

        hence (L . ((a * x),y)) = (a * (L . (x,y))) by A42, LOPBAN_1:def 5;

      end;

      

       A44: for x be Point of E, y1,y2 be Point of F holds (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2)))

      proof

        let x be Point of E, y1,y2 be Point of F;

        reconsider xy = <*x, y1*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

        

         A45: ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i2,xy))) as LinearOperator of F, G by LOPBAN10:def 6;

        

         A47: ( dom ( reproj (i2,xy))) = the carrier of ( <*E, F*> . i2) by FUNCT_2:def 1

        .= the carrier of F by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A49: i2 in ( dom xy) by TARSKI:def 2;

        

         A50: ( len (xy +* (i2,(y1 + y2)))) = 2 by LemmaA;

        

         A51: ((xy +* (i2,(y1 + y2))) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A52: ((xy +* (i2,(y1 + y2))) . 2) = (y1 + y2) by A49, FUNCT_7: 31;

        reconsider x1x2 = (y1 + y2) as Element of ( <*E, F*> . i2) by FINSEQ_1: 44;

        

         A54: (( reproj (i2,xy)) . x1x2) = (xy +* (i2,(y1 + y2))) by NDIFF_5:def 4

        .= <*x, (y1 + y2)*> by A50, A51, A52, FINSEQ_1: 44;

        

         A55: ( len (xy +* (i2,y1))) = 2 by LemmaA;

        

         A56: ((xy +* (i2,y1)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A57: ((xy +* (i2,y1)) . 2) = y1 by A49, FUNCT_7: 31;

        

         A59: (( reproj (i2,xy)) . y1) = (xy +* (i2,y1)) by A45, NDIFF_5:def 4

        .= <*x, y1*> by A55, A56, A57, FINSEQ_1: 44;

        

         A60: ( len (xy +* (i2,y2))) = 2 by LemmaA;

        

         A61: ((xy +* (i2,y2)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A62: ((xy +* (i2,y2)) . 2) = y2 by A49, FUNCT_7: 31;

        

         A64: (( reproj (i2,xy)) . y2) = (xy +* (i2,y2)) by A45, NDIFF_5:def 4

        .= <*x, y2*> by A60, A61, A62, FINSEQ_1: 44;

         [x, (y1 + y2)] is set & [x, y1] is set & [x, y2] is set by TARSKI: 1;

        then

         A46: [x, (y1 + y2)] is Point of [:E, F:] & [x, y1] is Point of [:E, F:] & [x, y2] is Point of [:E, F:] by PRVECT_3: 18;

        

        then

         A65: (L . (x,(y1 + y2))) = (u . (( IsoCPNrSP (E,F)) . (x,(y1 + y2)))) by FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . (y1 + y2))) by A54, NDIFF_7:def 3

        .= (L1 . (y1 + y2)) by A47, FUNCT_1: 13;

        

         A66: (L . (x,y1)) = (u . (( IsoCPNrSP (E,F)) . (x,y1))) by A46, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y1)) by A59, NDIFF_7:def 3

        .= (L1 . y1) by A47, FUNCT_1: 13;

        (L . (x,y2)) = (u . (( IsoCPNrSP (E,F)) . (x,y2))) by A46, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y2)) by A64, NDIFF_7:def 3

        .= (L1 . y2) by A47, FUNCT_1: 13;

        hence (L . (x,(y1 + y2))) = ((L . (x,y1)) + (L . (x,y2))) by A65, A66, VECTSP_1:def 20;

      end;

      for x be Point of E, y be Point of F, a be Real holds (L . (x,(a * y))) = (a * (L . (x,y)))

      proof

        let x be Point of E, y be Point of F, a be Real;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

        

         A68: ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        then

        reconsider L1 = (u * ( reproj (i2,xy))) as LinearOperator of F, G by LOPBAN10:def 6;

        

         A70: ( dom ( reproj (i2,xy))) = the carrier of ( <*E, F*> . i2) by FUNCT_2:def 1

        .= the carrier of F by FINSEQ_1: 44;

        ( len xy) = 2 by FINSEQ_1: 44;

        then ( dom xy) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then

         A72: i2 in ( dom xy) by TARSKI:def 2;

        then

         A75: ((xy +* (i2,(a * y))) . 2) = (a * y) by FUNCT_7: 31;

        

         A73: ( len (xy +* (i2,(a * y)))) = 2 by LemmaA;

        

         A74: ((xy +* (i2,(a * y))) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        reconsider x1x2 = (a * y) as Element of ( <*E, F*> . i2) by FINSEQ_1: 44;

        

         A77: (( reproj (i2,xy)) . x1x2) = (xy +* (i2,(a * y))) by NDIFF_5:def 4

        .= <*x, (a * y)*> by A73, A74, A75, FINSEQ_1: 44;

        

         A78: ( len (xy +* (i2,y))) = 2 by LemmaA;

        

         A79: ((xy +* (i2,y)) . 1) = (xy . i1) by FUNCT_7: 32

        .= x by FINSEQ_1: 44;

        

         A80: ((xy +* (i2,y)) . 2) = y by A72, FUNCT_7: 31;

        

         A82: (( reproj (i2,xy)) . y) = (xy +* (i2,y)) by A68, NDIFF_5:def 4

        .= <*x, y*> by A78, A79, A80, FINSEQ_1: 44;

         [x, y] is set & [x, (a * y)] is set by TARSKI: 1;

        then

         A69: [x, y] is Point of [:E, F:] & [x, (a * y)] is Point of [:E, F:] by PRVECT_3: 18;

        

        then

         A83: (L . (x,(a * y))) = (u . (( IsoCPNrSP (E,F)) . (x,(a * y)))) by FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . (a * y))) by A77, NDIFF_7:def 3

        .= (L1 . (a * y)) by A70, FUNCT_1: 13;

        (L . (x,y)) = (u . (( IsoCPNrSP (E,F)) . (x,y))) by A69, FUNCT_2: 15

        .= (u . (( reproj (i2,xy)) . y)) by A82, NDIFF_7:def 3

        .= (L1 . y) by A70, FUNCT_1: 13;

        hence (L . (x,(a * y))) = (a * (L . (x,y))) by A83, LOPBAN_1:def 5;

      end;

      then

      reconsider L as BilinearOperator of E, F, G by A2, A26, A44, LOPBAN_8: 12;

      ex K be Real st 0 <= K & for x be VECTOR of E, y be VECTOR of F holds ||.(L . (x,y)).|| <= ((K * ||.x.||) * ||.y.||)

      proof

        consider K be Real such that

         A85: 0 <= K & for s be Point of ( product <*E, F*>) holds ||.(u . s).|| <= (K * ( NrProduct s)) by LOPBAN10:def 10;

        take K;

        thus 0 <= K by A85;

        let x be VECTOR of E, y be VECTOR of F;

        reconsider xy = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

         [x, y] is set by TARSKI: 1;

        then [x, y] is Point of [:E, F:] by PRVECT_3: 18;

        

        then

         A87: (L . (x,y)) = (u . (( IsoCPNrSP (E,F)) . (x,y))) by FUNCT_2: 15

        .= (u . <*x, y*>) by NDIFF_7:def 3;

        reconsider s = <*x, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

        consider Nx be FinSequence of REAL such that

         A88: ( dom Nx) = ( dom <*E, F*>) & (for i be Element of ( dom <*E, F*>) holds (Nx . i) = ||.(s . i).||) & ( NrProduct s) = ( Product Nx) by LOPBAN10:def 9;

        ( dom Nx) = ( Seg ( len <*E, F*>)) by A88, FINSEQ_1:def 3

        .= ( Seg 2) by FINSEQ_1: 44;

        then

         A89: ( len Nx) = 2 by FINSEQ_1:def 3;

        

         A90: ( <*E, F*> . i1) = E & ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        

         A91: (Nx . 1) = ||.(s . i1).|| by A88

        .= ||.x.|| by A90, FINSEQ_1: 44;

        (Nx . 2) = ||.(s . i2).|| by A88

        .= ||.y.|| by A90, FINSEQ_1: 44;

        then Nx = <* ||.x.||, ||.y.||*> by A89, A91, FINSEQ_1: 44;

        then ( Product Nx) = ( ||.x.|| * ||.y.||) by RVSUM_1: 99;

        then ||.(L . (x,y)).|| <= (K * ( ||.x.|| * ||.y.||)) by A85, A87, A88;

        hence thesis;

      end;

      hence thesis by LOPBAN_9:def 3;

    end;

    theorem :: LOPBAN12:13

    

     IS02A: for u be Lipschitzian BilinearOperator of E, F, G holds (u * (( IsoCPNrSP (E,F)) " )) is Lipschitzian MultilinearOperator of <*E, F*>, G

    proof

      let u be Lipschitzian BilinearOperator of E, F, G;

      reconsider M = (u * (( IsoCPNrSP (E,F)) " )) as Function of ( product <*E, F*>), G;

      

       A1: ( dom <*E, F*>) = ( Seg ( len <*E, F*>)) by FINSEQ_1:def 3

      .= {1, 2} by FINSEQ_1: 2, FINSEQ_1: 44;

      then

      reconsider i1 = 1, i2 = 2 as Element of ( dom <*E, F*>) by TARSKI:def 2;

      for i be Element of ( dom <*E, F*>), s be Element of ( product <*E, F*>) holds (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G

      proof

        let i be Element of ( dom <*E, F*>), s be Element of ( product <*E, F*>);

        consider x be Point of E, y be Point of F such that

         A3: s = <*x, y*> by PRVECT_3: 19;

        ( len s) = 2 by A3, FINSEQ_1: 44;

        then

         A5: ( dom s) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

        per cases by A1, TARSKI:def 2;

          suppose

           A6: i = 1;

          then

           A7: ( <*E, F*> . i) = E by FINSEQ_1: 44;

          then

          reconsider L = (M * ( reproj (i,s))) as Function of E, G;

          

           A8: ( dom ( reproj (i,s))) = the carrier of ( <*E, F*> . i) by FUNCT_2:def 1

          .= the carrier of E by A6, FINSEQ_1: 44;

          

           A9: for z be Point of E holds (( reproj (i,s)) . z) = <*z, y*>

          proof

            let x1 be Point of E;

            

             A10: ( len (s +* (i,x1))) = 2 by LemmaA;

            

             A11: ((s +* (i,x1)) . 1) = x1 by A1, A5, A6, FUNCT_7: 31;

            

             A12: ((s +* (i,x1)) . 2) = (s . 2) by A6, FUNCT_7: 32

            .= y by A3, FINSEQ_1: 44;

            

            thus (( reproj (i,s)) . x1) = (s +* (i,x1)) by A7, NDIFF_5:def 4

            .= <*x1, y*> by A10, A11, A12, FINSEQ_1: 44;

          end;

          

           A14: for x1,x2 be Point of E holds (L . (x1 + x2)) = ((L . x1) + (L . x2))

          proof

            let x1,x2 be Point of E;

            reconsider x1y = <*x1, y*>, x2y = <*x2, y*>, x12y = <*(x1 + x2), y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

            

             A18: (L . x1) = (M . (( reproj (i,s)) . x1)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x1, y*>) by A9

            .= (u . ((( IsoCPNrSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x1,y)) by NDIFF_7: 18;

            

             A19: (L . x2) = (M . (( reproj (i,s)) . x2)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x2, y*>) by A9

            .= (u . ((( IsoCPNrSP (E,F)) " ) . x2y)) by FUNCT_2: 15

            .= (u . (x2,y)) by NDIFF_7: 18;

            (L . (x1 + x2)) = (M . (( reproj (i,s)) . (x1 + x2))) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*(x1 + x2), y*>) by A9

            .= (u . ((( IsoCPNrSP (E,F)) " ) . x12y)) by FUNCT_2: 15

            .= (u . ((x1 + x2),y)) by NDIFF_7: 18;

            hence (L . (x1 + x2)) = ((L . x1) + (L . x2)) by A18, A19, LOPBAN_8: 12;

          end;

          for x1 be Point of E, a be Real holds (L . (a * x1)) = (a * (L . x1))

          proof

            let x1 be Point of E, a be Real;

            reconsider ax1y = <*(a * x1), y*>, x1y = <*x1, y*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

            

             A23: (L . x1) = (M . (( reproj (i,s)) . x1)) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x1, y*>) by A9

            .= (u . ((( IsoCPNrSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x1,y)) by NDIFF_7: 18;

            (L . (a * x1)) = (M . (( reproj (i,s)) . (a * x1))) by A8, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*(a * x1), y*>) by A9

            .= (u . ((( IsoCPNrSP (E,F)) " ) . ax1y)) by FUNCT_2: 15

            .= (u . ((a * x1),y)) by NDIFF_7: 18;

            hence (L . (a * x1)) = (a * (L . x1)) by A23, LOPBAN_8: 12;

          end;

          hence (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G by A7, A14, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

          suppose

           A25: i = 2;

          then

           A26: ( <*E, F*> . i) = F by FINSEQ_1: 44;

          then

          reconsider L = (M * ( reproj (i,s))) as Function of F, G;

          

           A27: ( dom ( reproj (i,s))) = the carrier of ( <*E, F*> . i) by FUNCT_2:def 1

          .= the carrier of F by A25, FINSEQ_1: 44;

          

           A28: for z be Point of F holds (( reproj (i,s)) . z) = <*x, z*>

          proof

            let y1 be Point of F;

            

             A29: ( len (s +* (i,y1))) = 2 by LemmaA;

            

             A30: ((s +* (i,y1)) . 2) = y1 by A1, A5, A25, FUNCT_7: 31;

            

             A31: ((s +* (i,y1)) . 1) = (s . 1) by A25, FUNCT_7: 32

            .= x by A3, FINSEQ_1: 44;

            

            thus (( reproj (i,s)) . y1) = (s +* (i,y1)) by A26, NDIFF_5:def 4

            .= <*x, y1*> by A29, A30, A31, FINSEQ_1: 44;

          end;

          

           A33: for y1,y2 be Point of F holds (L . (y1 + y2)) = ((L . y1) + (L . y2))

          proof

            let y1,y2 be Point of F;

            reconsider y1y = <*x, y1*>, y2y = <*x, y2*>, y12y = <*x, (y1 + y2)*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

            

             A37: (L . y1) = (M . (( reproj (i,s)) . y1)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x, y1*>) by A28

            .= (u . ((( IsoCPNrSP (E,F)) " ) . y1y)) by FUNCT_2: 15

            .= (u . (x,y1)) by NDIFF_7: 18;

            

             A38: (L . y2) = (M . (( reproj (i,s)) . y2)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x, y2*>) by A28

            .= (u . ((( IsoCPNrSP (E,F)) " ) . y2y)) by FUNCT_2: 15

            .= (u . (x,y2)) by NDIFF_7: 18;

            (L . (y1 + y2)) = (M . (( reproj (i,s)) . (y1 + y2))) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x, (y1 + y2)*>) by A28

            .= (u . ((( IsoCPNrSP (E,F)) " ) . y12y)) by FUNCT_2: 15

            .= (u . (x,(y1 + y2))) by NDIFF_7: 18;

            hence (L . (y1 + y2)) = ((L . y1) + (L . y2)) by A37, A38, LOPBAN_8: 12;

          end;

          for y1 be Point of F, a be Real holds (L . (a * y1)) = (a * (L . y1))

          proof

            let y1 be Point of F, a be Real;

            reconsider ax1y = <*x, (a * y1)*>, x1y = <*x, y1*> as Point of ( product <*E, F*>) by PRVECT_3: 19;

            

             A42: (L . y1) = (M . (( reproj (i,s)) . y1)) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x, y1*>) by A28

            .= (u . ((( IsoCPNrSP (E,F)) " ) . x1y)) by FUNCT_2: 15

            .= (u . (x,y1)) by NDIFF_7: 18;

            (L . (a * y1)) = (M . (( reproj (i,s)) . (a * y1))) by A27, FUNCT_1: 13

            .= ((u * (( IsoCPNrSP (E,F)) " )) . <*x, (a * y1)*>) by A28

            .= (u . ((( IsoCPNrSP (E,F)) " ) . ax1y)) by FUNCT_2: 15

            .= (u . (x,(a * y1))) by NDIFF_7: 18;

            hence (L . (a * y1)) = (a * (L . y1)) by A42, LOPBAN_8: 12;

          end;

          hence (M * ( reproj (i,s))) is LinearOperator of ( <*E, F*> . i), G by A26, A33, LOPBAN_1:def 5, VECTSP_1:def 20;

        end;

      end;

      then

      reconsider M as MultilinearOperator of <*E, F*>, G by LOPBAN10:def 6;

      ex K be Real st 0 <= K & for s be Point of ( product <*E, F*>) holds ||.(M . s).|| <= (K * ( NrProduct s))

      proof

        consider K be Real such that

         A44: 0 <= K & for x be Point of E, y be Point of F holds ||.(u . (x,y)).|| <= ((K * ||.x.||) * ||.y.||) by LOPBAN_9:def 3;

        take K;

        thus 0 <= K by A44;

        let xy be Point of ( product <*E, F*>);

        consider x be Point of E, y be Point of F such that

         A45: xy = <*x, y*> by PRVECT_3: 19;

        

         A46: (M . xy) = (u . ((( IsoCPNrSP (E,F)) " ) . xy)) by FUNCT_2: 15

        .= (u . (x,y)) by A45, NDIFF_7: 18;

        consider Nx be FinSequence of REAL such that

         A47: ( dom Nx) = ( dom <*E, F*>) & (for i be Element of ( dom <*E, F*>) holds (Nx . i) = ||.(xy . i).||) & ( NrProduct xy) = ( Product Nx) by LOPBAN10:def 9;

        ( dom Nx) = ( Seg ( len <*E, F*>)) by A47, FINSEQ_1:def 3

        .= ( Seg 2) by FINSEQ_1: 44;

        then

         A48: ( len Nx) = 2 by FINSEQ_1:def 3;

        

         A49: ( <*E, F*> . i1) = E & ( <*E, F*> . i2) = F by FINSEQ_1: 44;

        

         A50: (Nx . 1) = ||.(xy . i1).|| by A47

        .= ||.x.|| by A45, A49, FINSEQ_1: 44;

        (Nx . 2) = ||.(xy . i2).|| by A47

        .= ||.y.|| by A45, A49, FINSEQ_1: 44;

        then Nx = <* ||.x.||, ||.y.||*> by A48, A50, FINSEQ_1: 44;

        then

         A51: ( NrProduct xy) = ( ||.x.|| * ||.y.||) by A47, RVSUM_1: 99;

         ||.(u . (x,y)).|| <= ((K * ||.x.||) * ||.y.||) by A44;

        hence thesis by A46, A51;

      end;

      hence thesis by LOPBAN10:def 10;

    end;

    theorem :: LOPBAN12:14

    

     IS03A: ex I be LinearOperator of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z)) st I is bijective isometric & for u be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds (I . u) = (u * (( IsoCPNrSP (X,Y)) " ))

    proof

      set F1 = the carrier of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

      set F2 = the carrier of ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z));

      defpred P1[ Function, Function] means $2 = ($1 * (( IsoCPNrSP (X,Y)) " ));

      

       A1: for x be Element of F1 holds ex y be Element of F2 st P1[x, y]

      proof

        let x be Element of F1;

        reconsider u = x as Lipschitzian BilinearOperator of X, Y, Z by LOPBAN_9:def 4;

        (u * (( IsoCPNrSP (X,Y)) " )) is Lipschitzian MultilinearOperator of <*X, Y*>, Z by IS02A;

        then

        reconsider v = (u * (( IsoCPNrSP (X,Y)) " )) as Element of F2 by LOPBAN10:def 11;

        take v;

        thus thesis;

      end;

      consider I be Function of F1, F2 such that

       A2: for x be Element of F1 holds P1[x, (I . x)] from FUNCT_2:sch 3( A1);

      

       A3: for x1,x2 be object st x1 in F1 & x2 in F1 & (I . x1) = (I . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A4: x1 in F1 & x2 in F1 & (I . x1) = (I . x2);

        then

        reconsider u1 = x1, u2 = x2 as Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

        reconsider v1 = u1, v2 = u2 as Lipschitzian BilinearOperator of X, Y, Z by LOPBAN_9:def 4;

        (I . v1) = (v1 * (( IsoCPNrSP (X,Y)) " )) by A2;

        then (v1 * (( IsoCPNrSP (X,Y)) " )) = (v2 * (( IsoCPNrSP (X,Y)) " )) by A2, A4;

        then (v1 * ((( IsoCPNrSP (X,Y)) " ) * ( IsoCPNrSP (X,Y)))) = ((v2 * (( IsoCPNrSP (X,Y)) " )) * ( IsoCPNrSP (X,Y))) by RELAT_1: 36;

        then

         A6: (v1 * ((( IsoCPNrSP (X,Y)) " ) * ( IsoCPNrSP (X,Y)))) = (v2 * ((( IsoCPNrSP (X,Y)) " ) * ( IsoCPNrSP (X,Y)))) by RELAT_1: 36;

        ( IsoCPNrSP (X,Y)) is one-to-one & ( rng ( IsoCPNrSP (X,Y))) = the carrier of ( product <*X, Y*>) by FUNCT_2:def 3;

        then

         A7: ((( IsoCPNrSP (X,Y)) " ) * ( IsoCPNrSP (X,Y))) = ( id [:X, Y:]) by FUNCT_2: 29;

        then (v1 * ((( IsoCPNrSP (X,Y)) " ) * ( IsoCPNrSP (X,Y)))) = v1 by FUNCT_2: 17;

        hence thesis by A6, A7, FUNCT_2: 17;

      end;

      for y be object st y in F2 holds ex x be object st x in F1 & y = (I . x)

      proof

        let y be object;

        assume y in F2;

        then

        reconsider u = y as Point of ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z));

        reconsider u1 = u as Lipschitzian MultilinearOperator of <*X, Y*>, Z by LOPBAN10:def 11;

        reconsider v1 = (u1 * ( IsoCPNrSP (X,Y))) as Lipschitzian BilinearOperator of X, Y, Z by IS01A;

        reconsider v = v1 as Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) by LOPBAN_9:def 4;

        take v;

        thus v in F1;

        ( IsoCPNrSP (X,Y)) is one-to-one & ( rng ( IsoCPNrSP (X,Y))) = the carrier of ( product <*X, Y*>) by FUNCT_2:def 3;

        then

         A10: (( IsoCPNrSP (X,Y)) * (( IsoCPNrSP (X,Y)) " )) = ( id ( product <*X, Y*>)) by FUNCT_2: 29;

        

        thus (I . v) = ((u1 * ( IsoCPNrSP (X,Y))) * (( IsoCPNrSP (X,Y)) " )) by A2

        .= (u1 * (( IsoCPNrSP (X,Y)) * (( IsoCPNrSP (X,Y)) " ))) by RELAT_1: 36

        .= y by A10, FUNCT_2: 17;

      end;

      then

       A9: I is onto by FUNCT_2: 10;

      

       A12: for x,y be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds (I . (x + y)) = ((I . x) + (I . y))

      proof

        let x,y be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

        

         A13: (I . x) = (x * (( IsoCPNrSP (X,Y)) " )) by A2;

        

         A14: (I . y) = (y * (( IsoCPNrSP (X,Y)) " )) by A2;

        

         A15: (I . (x + y)) = ((x + y) * (( IsoCPNrSP (X,Y)) " )) by A2;

        set f = (I . x), g = (I . y), h = (I . (x + y));

        for xy be VECTOR of ( product <*X, Y*>) holds (h . xy) = ((f . xy) + (g . xy))

        proof

          let xy be VECTOR of ( product <*X, Y*>);

          consider p be Point of X, q be Point of Y such that

           A16: xy = <*p, q*> by PRVECT_3: 19;

          

           A17: (f . xy) = (x . ((( IsoCPNrSP (X,Y)) " ) . xy)) by A13, FUNCT_2: 15

          .= (x . (p,q)) by A16, NDIFF_7: 18;

          

           A18: (g . xy) = (y . ((( IsoCPNrSP (X,Y)) " ) . xy)) by A14, FUNCT_2: 15

          .= (y . (p,q)) by A16, NDIFF_7: 18;

          (h . xy) = ((x + y) . ((( IsoCPNrSP (X,Y)) " ) . xy)) by A15, FUNCT_2: 15

          .= ((x + y) . (p,q)) by A16, NDIFF_7: 18;

          hence (h . xy) = ((f . xy) + (g . xy)) by A17, A18, LOPBAN_9: 19;

        end;

        hence thesis by LOPBAN10: 48;

      end;

      for x be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), a be Real holds (I . (a * x)) = (a * (I . x))

      proof

        let x be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), a be Real;

        

         A20: (I . x) = (x * (( IsoCPNrSP (X,Y)) " )) by A2;

        

         A21: (I . (a * x)) = ((a * x) * (( IsoCPNrSP (X,Y)) " )) by A2;

        set f = (I . x), g = (I . (a * x));

        for xy be VECTOR of ( product <*X, Y*>) holds (g . xy) = (a * (f . xy))

        proof

          let xy be VECTOR of ( product <*X, Y*>);

          consider p be Point of X, q be Point of Y such that

           A22: xy = <*p, q*> by PRVECT_3: 19;

          

           A23: (f . xy) = (x . ((( IsoCPNrSP (X,Y)) " ) . xy)) by A20, FUNCT_2: 15

          .= (x . (p,q)) by A22, NDIFF_7: 18;

          (g . xy) = ((a * x) . ((( IsoCPNrSP (X,Y)) " ) . xy)) by A21, FUNCT_2: 15

          .= ((a * x) . (p,q)) by A22, NDIFF_7: 18;

          hence (g . xy) = (a * (f . xy)) by A23, LOPBAN_9: 20;

        end;

        hence thesis by LOPBAN10: 49;

      end;

      then

      reconsider I as LinearOperator of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z)) by A12, LOPBAN_1:def 5, VECTSP_1:def 20;

      take I;

      

       A35: ( dom <*X, Y*>) = ( Seg ( len <*X, Y*>)) by FINSEQ_1:def 3

      .= ( Seg 2) by FINSEQ_1: 44;

      for u be Element of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds ||.(I . u).|| = ||.u.||

      proof

        let u be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z));

        reconsider u1 = u as Lipschitzian BilinearOperator of X, Y, Z by LOPBAN_9:def 4;

        reconsider v1 = (I . u) as Lipschitzian MultilinearOperator of <*X, Y*>, Z by LOPBAN10:def 11;

        

         A26: ||.u.|| = ( upper_bound ( PreNorms ( modetrans (u,X,Y,Z)))) by LOPBAN_9:def 8

        .= ( upper_bound ( PreNorms u1));

        

         A27: ||.(I . u).|| = ( upper_bound ( PreNorms ( modetrans (v1, <*X, Y*>,Z)))) by LOPBAN10:def 15

        .= ( upper_bound ( PreNorms v1));

        for z be object holds z in ( PreNorms u1) iff z in ( PreNorms v1)

        proof

          let z be object;

          hereby

            assume z in ( PreNorms u1);

            then

            consider x be VECTOR of X, y be VECTOR of Y such that

             A28: z = ||.(u1 . (x,y)).|| & ||.x.|| <= 1 & ||.y.|| <= 1;

            reconsider s = <*x, y*> as Point of ( product <*X, Y*>) by PRVECT_3: 19;

            

             A29: ( <*X, Y*> . 1) = X & ( <*X, Y*> . 2) = Y by FINSEQ_1: 44;

            

             A30: (v1 . s) = ((u * (( IsoCPNrSP (X,Y)) " )) . s) by A2

            .= (u . ((( IsoCPNrSP (X,Y)) " ) . s)) by FUNCT_2: 15

            .= (u1 . (x,y)) by NDIFF_7: 18;

            for i be Element of ( dom <*X, Y*>) holds ||.(s . i).|| <= 1

            proof

              let i be Element of ( dom <*X, Y*>);

              i = 1 or i = 2 by FINSEQ_1: 2, TARSKI:def 2, A35;

              hence thesis by A28, A29, FINSEQ_1: 44;

            end;

            hence z in ( PreNorms v1) by A28, A30;

          end;

          assume z in ( PreNorms v1);

          then

          consider s be VECTOR of ( product <*X, Y*>) such that

           A31: z = ||.(v1 . s).|| & for i be Element of ( dom <*X, Y*>) holds ||.(s . i).|| <= 1;

          consider x be Point of X, y be Point of Y such that

           A32: s = <*x, y*> by PRVECT_3: 19;

          

           A33: (v1 . s) = ((u * (( IsoCPNrSP (X,Y)) " )) . s) by A2

          .= (u . ((( IsoCPNrSP (X,Y)) " ) . s)) by FUNCT_2: 15

          .= (u1 . (x,y)) by A32, NDIFF_7: 18;

          

           A34: ( <*X, Y*> . 1) = X & ( <*X, Y*> . 2) = Y by FINSEQ_1: 44;

          reconsider i1 = 1, i2 = 2 as Element of ( dom <*X, Y*>) by A35, FINSEQ_1: 2, TARSKI:def 2;

           ||.(s . i1).|| <= 1 & ||.(s . i2).|| <= 1 by A31;

          then ||.x.|| <= 1 & ||.y.|| <= 1 by A32, A34, FINSEQ_1: 44;

          hence z in ( PreNorms u1) by A31, A33;

        end;

        hence thesis by A26, A27, TARSKI: 2;

      end;

      hence thesis by A2, NDIFF_7: 7, A3, A9, FUNCT_2: 19;

    end;

    theorem :: LOPBAN12:15

    

     IS04A: ex I be LinearOperator of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))), ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z)) st I is bijective isometric & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.u.|| = ||.(I . u).|| & for x be Point of X, y be Point of Y holds ((I . u) . <*x, y*>) = ((u . x) . y)

    proof

      consider I be LinearOperator of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))), ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) such that

       A1: I is bijective & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.u.|| = ||.(I . u).|| & for x be Point of X, y be Point of Y holds ((I . u) . (x,y)) = ((u . x) . y) by LOPBAN_9: 27;

      consider J be LinearOperator of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)), ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z)) such that

       A2: J is bijective isometric & for u be Point of ( R_NormSpace_of_BoundedBilinearOperators (X,Y,Z)) holds (J . u) = (u * (( IsoCPNrSP (X,Y)) " )) by IS03A;

      reconsider K = (J * I) as LinearOperator of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))), ( R_NormSpace_of_BoundedMultilinearOperators ( <*X, Y*>,Z)) by LOPBAN_2: 1;

      take K;

      thus K is bijective by A1, A2, FUNCT_2: 27;

      

       A3: for x be Element of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z)))) holds ||.(K . x).|| = ||.x.||

      proof

        let x be Element of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z))));

        

        thus ||.(K . x).|| = ||.(J . (I . x)).|| by FUNCT_2: 15

        .= ||.(I . x).|| by A2, NDIFF_7: 7

        .= ||.x.|| by A1;

      end;

      hence K is isometric by NDIFF_7: 7;

      let u be Point of ( R_NormSpace_of_BoundedLinearOperators (X,( R_NormSpace_of_BoundedLinearOperators (Y,Z))));

      thus ||.(K . u).|| = ||.u.|| by A3;

      let x be Point of X, y be Point of Y;

      

       A4: (K . u) = (J . (I . u)) by FUNCT_2: 15;

      reconsider xy = <*x, y*> as Point of ( product <*X, Y*>) by PRVECT_3: 19;

      

      thus ((K . u) . <*x, y*>) = (((I . u) * (( IsoCPNrSP (X,Y)) " )) . xy) by A2, A4

      .= ((I . u) . ((( IsoCPNrSP (X,Y)) " ) . xy)) by FUNCT_2: 15

      .= ((I . u) . (x,y)) by NDIFF_7: 18

      .= ((u . x) . y) by A1;

    end;

    theorem :: LOPBAN12:16

    for X,Y be RealNormSpace-Sequence, Z be RealNormSpace holds ex I be LinearOperator of ( R_NormSpace_of_BoundedLinearOperators (( product X),( R_NormSpace_of_BoundedLinearOperators (( product Y),Z)))), ( R_NormSpace_of_BoundedMultilinearOperators ( <*( product X), ( product Y)*>,Z)) st I is bijective isometric & for u be Point of ( R_NormSpace_of_BoundedLinearOperators (( product X),( R_NormSpace_of_BoundedLinearOperators (( product Y),Z)))) holds ||.u.|| = ||.(I . u).|| & for x be Point of ( product X), y be Point of ( product Y) holds ((I . u) . <*x, y*>) = ((u . x) . y) by IS04A;