prvect_3.miz



    begin

    reserve G,F for RealLinearSpace;

    theorem :: PRVECT_3:1

    for D,E,F,G be non empty set holds ex I be Function of [: [:D, E:], [:F, G:]:], [: [:D, F:], [:E, G:]:] st I is one-to-one & I is onto & for d,e,f,g be set st d in D & e in E & f in F & g in G holds (I . ( [d, e], [f, g])) = [ [d, f], [e, g]]

    proof

      let D,E,F,G be non empty set;

      defpred P0[ object, object, object] means ex d,e,f,g be set st d in D & e in E & f in F & g in G & $1 = [d, e] & $2 = [f, g] & $3 = [ [d, f], [e, g]];

      

       A1: for x,y be object st x in [:D, E:] & y in [:F, G:] holds ex z be object st z in [: [:D, F:], [:E, G:]:] & P0[x, y, z]

      proof

        let x,y be object;

        assume

         A2: x in [:D, E:] & y in [:F, G:];

        consider d,e be object such that

         A3: d in D & e in E & x = [d, e] by A2, ZFMISC_1:def 2;

        consider f,g be object such that

         A4: f in F & g in G & y = [f, g] by A2, ZFMISC_1:def 2;

         [d, f] in [:D, F:] & [e, g] in [:E, G:] by A3, A4, ZFMISC_1: 87;

        then [ [d, f], [e, g]] in [: [:D, F:], [:E, G:]:] by ZFMISC_1: 87;

        hence thesis by A3, A4;

      end;

      consider I be Function of [: [:D, E:], [:F, G:]:], [: [:D, F:], [:E, G:]:] such that

       A5: for x,y be object st x in [:D, E:] & y in [:F, G:] holds P0[x, y, (I . (x,y))] from BINOP_1:sch 1( A1);

      

       A6: for d,e,f,g be set st d in D & e in E & f in F & g in G holds (I . ( [d, e], [f, g])) = [ [d, f], [e, g]]

      proof

        let d,e,f,g be set;

        assume

         A7: d in D & e in E & f in F & g in G;

        

         A8: [d, e] in [:D, E:] & [f, g] in [:F, G:] by A7, ZFMISC_1: 87;

        consider d1,e1,f1,g1 be set such that

         A9: d1 in D & e1 in E & f1 in F & g1 in G & [d, e] = [d1, e1] & [f, g] = [f1, g1] & (I . ( [d, e], [f, g])) = [ [d1, f1], [e1, g1]] by A8, A5;

        d1 = d & e1 = e & f1 = f & g1 = g by A9, XTUPLE_0: 1;

        hence (I . ( [d, e], [f, g])) = [ [d, f], [e, g]] by A9;

      end;

      

       A10: I is one-to-one

      proof

        now

          let z1,z2 be object;

          assume

           A11: z1 in [: [:D, E:], [:F, G:]:] & z2 in [: [:D, E:], [:F, G:]:] & (I . z1) = (I . z2);

          consider de1,fg1 be object such that

           A12: de1 in [:D, E:] & fg1 in [:F, G:] & z1 = [de1, fg1] by A11, ZFMISC_1:def 2;

          consider d1,e1 be object such that

           A13: d1 in D & e1 in E & de1 = [d1, e1] by A12, ZFMISC_1:def 2;

          consider f1,g1 be object such that

           A14: f1 in F & g1 in G & fg1 = [f1, g1] by A12, ZFMISC_1:def 2;

          consider de2,fg2 be object such that

           A15: de2 in [:D, E:] & fg2 in [:F, G:] & z2 = [de2, fg2] by A11, ZFMISC_1:def 2;

          consider d2,e2 be object such that

           A16: d2 in D & e2 in E & de2 = [d2, e2] by A15, ZFMISC_1:def 2;

          consider f2,g2 be object such that

           A17: f2 in F & g2 in G & fg2 = [f2, g2] by A15, ZFMISC_1:def 2;

           [ [d1, f1], [e1, g1]] = (I . ( [d1, e1], [f1, g1])) by A6, A13, A14

          .= (I . ( [d2, e2], [f2, g2])) by A11, A12, A13, A14, A15, A16, A17

          .= [ [d2, f2], [e2, g2]] by A6, A16, A17;

          then [d1, f1] = [d2, f2] & [e1, g1] = [e2, g2] by XTUPLE_0: 1;

          then d1 = d2 & f1 = f2 & e1 = e2 & g1 = g2 by XTUPLE_0: 1;

          hence z1 = z2 by A12, A13, A14, A15, A16, A17;

        end;

        hence thesis by FUNCT_2: 19;

      end;

      I is onto

      proof

        now

          let w be object;

          assume

           A18: w in [: [:D, F:], [:E, G:]:];

          consider df,eg be object such that

           A19: df in [:D, F:] & eg in [:E, G:] & w = [df, eg] by A18, ZFMISC_1:def 2;

          consider d,f be object such that

           A20: d in D & f in F & df = [d, f] by A19, ZFMISC_1:def 2;

          consider e,g be object such that

           A21: e in E & g in G & eg = [e, g] by A19, ZFMISC_1:def 2;

          

           A22: [d, e] in [:D, E:] & [f, g] in [:F, G:] by A20, A21, ZFMISC_1: 87;

          reconsider z = [ [d, e], [f, g]] as Element of [: [:D, E:], [:F, G:]:] by A22, ZFMISC_1: 87;

          w = (I . ( [d, e], [f, g])) by A6, A19, A20, A21;

          then w = (I . z);

          hence w in ( rng I) by FUNCT_2: 112;

        end;

        then [: [:D, F:], [:E, G:]:] c= ( rng I) by TARSKI:def 3;

        then [: [:D, F:], [:E, G:]:] = ( rng I) by XBOOLE_0:def 10;

        hence thesis by FUNCT_2:def 3;

      end;

      hence thesis by A6, A10;

    end;

    theorem :: PRVECT_3:2

    

     Th2: for X be non empty set, D be Function st ( dom D) = {1} & (D . 1) = X holds ex I be Function of X, ( product D) st I is one-to-one & I is onto & for x be object st x in X holds (I . x) = <*x*>

    proof

      let X be non empty set, D be Function;

      assume

       A1: ( dom D) = {1} & (D . 1) = X;

      defpred P[ object, object] means $2 = <*$1*>;

      

       A2: for x be object st x in X holds ex z be object st z in ( product D) & P[x, z]

      proof

        let x be object;

        assume

         A3: x in X;

        

         A4: ( dom <*x*>) = ( Seg ( len <*x*>)) by FINSEQ_1:def 3

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

        now

          let i be object;

          assume i in ( dom <*x*>);

          then i = 1 by A4, TARSKI:def 1;

          hence ( <*x*> . i) in (D . i) by A1, A3, FINSEQ_1: 40;

        end;

        then <*x*> in ( product D) by A4, A1, CARD_3: 9;

        hence ex z be object st z in ( product D) & P[x, z];

      end;

      consider I be Function of X, ( product D) such that

       A5: for x be object st x in X holds P[x, (I . x)] from FUNCT_2:sch 1( A2);

      now

        assume {} in ( rng D);

        then ex x be object st x in ( dom D) & (D . x) = {} by FUNCT_1:def 3;

        hence contradiction by A1, TARSKI:def 1;

      end;

      then

       A6: ( product D) <> {} by CARD_3: 26;

      now

        let z1,z2 be object;

        assume

         A7: z1 in X & z2 in X & (I . z1) = (I . z2);

         <*z1*> = (I . z1) by A5, A7

        .= <*z2*> by A5, A7;

        hence z1 = z2 by FINSEQ_1: 76;

      end;

      then

       A8: I is one-to-one by A6, FUNCT_2: 19;

      now

        let w be object;

        assume w in ( product D);

        then

        consider g be Function such that

         A9: w = g & ( dom g) = ( dom D) & for i be object st i in ( dom D) holds (g . i) in (D . i) by CARD_3:def 5;

        reconsider g as FinSequence by A1, A9, FINSEQ_1: 2, FINSEQ_1:def 2;

        set x = (g . 1);

        

         A10: ( len g) = 1 by A1, A9, FINSEQ_1: 2, FINSEQ_1:def 3;

        1 in ( dom D) by A1, TARSKI:def 1;

        then

         A11: x in X & w = <*x*> by A9, A10, A1, FINSEQ_1: 40;

        then w = (I . x) by A5;

        hence w in ( rng I) by A11, A6, FUNCT_2: 112;

      end;

      then ( product D) c= ( rng I) by TARSKI:def 3;

      then ( product D) = ( rng I) by XBOOLE_0:def 10;

      then I is onto by FUNCT_2:def 3;

      hence thesis by A5, A8;

    end;

    theorem :: PRVECT_3:3

    

     Th3: for X,Y be non empty set, D be Function st ( dom D) = {1, 2} & (D . 1) = X & (D . 2) = Y holds ex I be Function of [:X, Y:], ( product D) st I is one-to-one & I is onto & for x,y be object st x in X & y in Y holds (I . (x,y)) = <*x, y*>

    proof

      let X,Y be non empty set, D be Function;

      assume

       A1: ( dom D) = {1, 2} & (D . 1) = X & (D . 2) = Y;

      defpred P[ object, object, object] means $3 = <*$1, $2*>;

      

       A2: for x,y be object st x in X & y in Y holds ex z be object st z in ( product D) & P[x, y, z]

      proof

        let x,y be object;

        assume

         A3: x in X & y in Y;

        

         A4: ( dom <*x, y*>) = ( Seg ( len <*x, y*>)) by FINSEQ_1:def 3

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

        now

          let i be object;

          assume i in ( dom <*x, y*>);

          then i = 1 or i = 2 by A4, TARSKI:def 2;

          hence ( <*x, y*> . i) in (D . i) by A1, A3, FINSEQ_1: 44;

        end;

        then <*x, y*> in ( product D) by A4, A1, CARD_3: 9;

        hence ex z be object st z in ( product D) & P[x, y, z];

      end;

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

       A5: for x,y be object st x in X & y in Y holds P[x, y, (I . (x,y))] from BINOP_1:sch 1( A2);

      now

        assume {} in ( rng D);

        then ex x be object st x in ( dom D) & (D . x) = {} by FUNCT_1:def 3;

        hence contradiction by A1, TARSKI:def 2;

      end;

      then

       A6: ( product D) <> {} by CARD_3: 26;

      now

        let z1,z2 be object;

        assume

         A7: z1 in [:X, Y:] & z2 in [:X, Y:] & (I . z1) = (I . z2);

        then

        consider x1,y1 be object such that

         A8: x1 in X & y1 in Y & z1 = [x1, y1] by ZFMISC_1:def 2;

        consider x2,y2 be object such that

         A9: x2 in X & y2 in Y & z2 = [x2, y2] by A7, ZFMISC_1:def 2;

         <*x1, y1*> = (I . (x1,y1)) by A5, A8

        .= (I . (x2,y2)) by A7, A8, A9

        .= <*x2, y2*> by A5, A9;

        then x1 = x2 & y1 = y2 by FINSEQ_1: 77;

        hence z1 = z2 by A8, A9;

      end;

      then

       A10: I is one-to-one by A6, FUNCT_2: 19;

      now

        let w be object;

        assume w in ( product D);

        then

        consider g be Function such that

         A11: w = g & ( dom g) = ( dom D) & for i be object st i in ( dom D) holds (g . i) in (D . i) by CARD_3:def 5;

        reconsider g as FinSequence by A1, A11, FINSEQ_1: 2, FINSEQ_1:def 2;

        set x = (g . 1);

        set y = (g . 2);

        

         A12: ( len g) = 2 by A1, A11, FINSEQ_1: 2, FINSEQ_1:def 3;

        1 in ( dom D) & 2 in ( dom D) by A1, TARSKI:def 2;

        then

         A13: x in X & y in Y & w = <*x, y*> by A11, A12, A1, FINSEQ_1: 44;

        reconsider z = [x, y] as Element of [:X, Y:] by A13, ZFMISC_1: 87;

        w = (I . (x,y)) by A5, A13

        .= (I . z);

        hence w in ( rng I) by A6, FUNCT_2: 112;

      end;

      then ( product D) c= ( rng I) by TARSKI:def 3;

      then ( product D) = ( rng I) by XBOOLE_0:def 10;

      then I is onto by FUNCT_2:def 3;

      hence thesis by A5, A10;

    end;

    theorem :: PRVECT_3:4

    

     Th4: for X be non empty set holds ex I be Function of X, ( product <*X*>) st I is one-to-one & I is onto & for x be object st x in X holds (I . x) = <*x*>

    proof

      let X be non empty set;

      ( dom <*X*>) = {1} & ( <*X*> . 1) = X by FINSEQ_1: 2, FINSEQ_1: 38, FINSEQ_1: 40;

      hence thesis by Th2;

    end;

    registration

      let X,Y be non-empty non empty FinSequence;

      cluster (X ^ Y) -> non-empty;

      correctness

      proof

        now

          let z be object;

          assume

           A1: z in ( dom (X ^ Y));

          then

          reconsider k = z as Element of NAT ;

          per cases by A1, FINSEQ_1: 25;

            suppose

             A2: k in ( dom X);

            then (X . k) = ((X ^ Y) . k) by FINSEQ_1:def 7;

            hence ((X ^ Y) . z) is non empty by A2;

          end;

            suppose ex n be Nat st n in ( dom Y) & k = (( len X) + n);

            then

            consider n be Nat such that

             A3: n in ( dom Y) & k = (( len X) + n);

            (Y . n) = ((X ^ Y) . k) by A3, FINSEQ_1:def 7;

            hence ((X ^ Y) . z) is non empty by A3;

          end;

        end;

        hence thesis by FUNCT_1:def 9;

      end;

    end

    theorem :: PRVECT_3:5

    

     Th5: for X,Y be non empty set holds ex I be Function of [:X, Y:], ( product <*X, Y*>) st I is one-to-one & I is onto & for x,y be object st x in X & y in Y holds (I . (x,y)) = <*x, y*>

    proof

      let X,Y be non empty set;

      ( dom <*X, Y*>) = {1, 2} & ( <*X, Y*> . 1) = X & ( <*X, Y*> . 2) = Y by FINSEQ_1: 2, FINSEQ_1: 44, FINSEQ_1: 89;

      hence thesis by Th3;

    end;

    theorem :: PRVECT_3:6

    

     Th6: for X,Y be non-empty non empty FinSequence holds ex I be Function of [:( product X), ( product Y):], ( product (X ^ Y)) st I is one-to-one & I is onto & for x,y be FinSequence st x in ( product X) & y in ( product Y) holds (I . (x,y)) = (x ^ y)

    proof

      let X,Y be non-empty non empty FinSequence;

      defpred P[ object, object, object] means ex x,y be FinSequence st x = $1 & y = $2 & $3 = (x ^ y);

      

       A1: for x,y be object st x in ( product X) & y in ( product Y) holds ex z be object st z in ( product (X ^ Y)) & P[x, y, z]

      proof

        let x,y be object;

        assume

         A2: x in ( product X) & y in ( product Y);

        then

        consider g be Function such that

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

        

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

        then

        reconsider g as FinSequence by FINSEQ_1:def 2;

        consider h be Function such that

         A5: y = h & ( dom h) = ( dom Y) & for z be object st z in ( dom Y) holds (h . z) in (Y . z) by A2, CARD_3:def 5;

        

         A6: ( dom h) = ( Seg ( len Y)) by A5, FINSEQ_1:def 3;

        then

        reconsider h as FinSequence by FINSEQ_1:def 2;

        

         A7: ( len g) = ( len X) & ( len h) = ( len Y) by A4, A6, FINSEQ_1:def 3;

        

         A8: ( dom (g ^ h)) = ( Seg (( len g) + ( len h))) by FINSEQ_1:def 7

        .= ( Seg ( len (X ^ Y))) by A7, FINSEQ_1: 22

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

        for z be object st z in ( dom (X ^ Y)) holds ((g ^ h) . z) in ((X ^ Y) . z)

        proof

          let z be object;

          assume

           A9: z in ( dom (X ^ Y));

          then

          reconsider k = z as Element of NAT ;

          per cases by A9, FINSEQ_1: 25;

            suppose

             A10: k in ( dom X);

            then

             A11: (g . k) in (X . k) by A3;

            (g . k) = ((g ^ h) . k) by A10, A3, FINSEQ_1:def 7;

            hence ((g ^ h) . z) in ((X ^ Y) . z) by A11, A10, FINSEQ_1:def 7;

          end;

            suppose ex n be Nat st n in ( dom Y) & k = (( len X) + n);

            then

            consider n be Nat such that

             A12: n in ( dom Y) & k = (( len X) + n);

            

             A13: (h . n) in (Y . n) by A12, A5;

            (h . n) = ((g ^ h) . k) by A12, A7, A5, FINSEQ_1:def 7;

            hence ((g ^ h) . z) in ((X ^ Y) . z) by A13, A12, FINSEQ_1:def 7;

          end;

        end;

        then (g ^ h) in ( product (X ^ Y)) by A8, CARD_3: 9;

        hence thesis by A3, A5;

      end;

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

       A14: for x,y be object st x in ( product X) & y in ( product Y) holds P[x, y, (I . (x,y))] from BINOP_1:sch 1( A1);

      

       A15: for x,y be FinSequence st x in ( product X) & y in ( product Y) holds (I . (x,y)) = (x ^ y)

      proof

        let x,y be FinSequence;

        assume x in ( product X) & y in ( product Y);

        then ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1) by A14;

        hence thesis;

      end;

      now

        let z1,z2 be object;

        assume

         A16: z1 in [:( product X), ( product Y):] & z2 in [:( product X), ( product Y):] & (I . z1) = (I . z2);

        consider x1,y1 be object such that

         A17: x1 in ( product X) & y1 in ( product Y) & z1 = [x1, y1] by A16, ZFMISC_1:def 2;

        consider x2,y2 be object such that

         A18: x2 in ( product X) & y2 in ( product Y) & z2 = [x2, y2] by A16, ZFMISC_1:def 2;

        consider xx1,yy1 be FinSequence such that

         A19: xx1 = x1 & yy1 = y1 & (I . (x1,y1)) = (xx1 ^ yy1) by A14, A17;

        consider xx2,yy2 be FinSequence such that

         A20: xx2 = x2 & yy2 = y2 & (I . (x2,y2)) = (xx2 ^ yy2) by A14, A18;

        

         A21: ( dom xx1) = ( dom X) by A17, A19, CARD_3: 9

        .= ( dom xx2) by A18, A20, CARD_3: 9;

        xx1 = ((xx1 ^ yy1) | ( dom xx1)) by FINSEQ_1: 21

        .= xx2 by A16, A17, A18, A19, A20, A21, FINSEQ_1: 21;

        hence z1 = z2 by A16, A17, A18, A19, A20, FINSEQ_1: 33;

      end;

      then

       A22: I is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in ( product (X ^ Y));

        then

        consider g be Function such that

         A23: w = g & ( dom g) = ( dom (X ^ Y)) & for i be object st i in ( dom (X ^ Y)) holds (g . i) in ((X ^ Y) . i) by CARD_3:def 5;

        

         A24: ( dom g) = ( Seg ( len (X ^ Y))) by A23, FINSEQ_1:def 3;

        then

        reconsider g as FinSequence by FINSEQ_1:def 2;

        set x = (g | ( len X));

        set y = (g /^ ( len X));

        

         A26: (x ^ y) = g by RFINSEQ: 8;

        

         A27: ( len (X ^ Y)) = (( len X) + ( len Y)) by FINSEQ_1: 22;

        then

         A28: ( len X) <= ( len (X ^ Y)) by NAT_1: 11;

        

         A29: ( len g) = ( len (X ^ Y)) by A24, FINSEQ_1:def 3;

        then ( len (g | ( len X))) = ( len X) by A27, FINSEQ_1: 59, NAT_1: 11;

        

        then

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

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

        for z be object st z in ( dom X) holds (x . z) in (X . z)

        proof

          let z be object;

          assume

           A31: z in ( dom X);

          then

          reconsider k = z as Element of NAT ;

          

           A32: ( dom X) c= ( dom (X ^ Y)) by FINSEQ_1: 26;

          

           A33: (x . k) = (g . k) by A31, A26, A30, FINSEQ_1:def 7;

          (X . k) = ((X ^ Y) . k) by A31, FINSEQ_1:def 7;

          hence (x . z) in (X . z) by A33, A23, A31, A32;

        end;

        then

         A34: x in ( product X) by A30, CARD_3: 9;

        ( dom x) = ( Seg ( len X)) by A30, FINSEQ_1:def 3;

        then

         A35: ( len x) = ( len X) by FINSEQ_1:def 3;

        ( len y) = (( len g) - ( len X)) by A28, A29, RFINSEQ:def 1

        .= ( len Y) by A29, A27;

        then ( Seg ( len y)) = ( dom Y) by FINSEQ_1:def 3;

        then

         A36: ( dom y) = ( dom Y) by FINSEQ_1:def 3;

        for z be object st z in ( dom Y) holds (y . z) in (Y . z)

        proof

          let z be object;

          assume

           A37: z in ( dom Y);

          then

          reconsider k = z as Element of NAT ;

          

           A38: (y . k) = (g . (( len X) + k)) by A37, A26, A35, A36, FINSEQ_1:def 7;

          (Y . k) = ((X ^ Y) . (( len X) + k)) by A37, FINSEQ_1:def 7;

          hence (y . z) in (Y . z) by A38, A23, A37, FINSEQ_1: 28;

        end;

        then

         A39: y in ( product Y) by A36, CARD_3: 9;

        reconsider z = [x, y] as Element of [:( product X), ( product Y):] by A34, A39, ZFMISC_1: 87;

        w = (I . (x,y)) by A23, A26, A15, A34, A39

        .= (I . z);

        hence w in ( rng I) by FUNCT_2: 112;

      end;

      then ( product (X ^ Y)) c= ( rng I) by TARSKI:def 3;

      then ( product (X ^ Y)) = ( rng I) by XBOOLE_0:def 10;

      then I is onto by FUNCT_2:def 3;

      hence thesis by A15, A22;

    end;

    

     Lm1: for G,F be non empty 1-sorted, x be set st x in [:the carrier of G, the carrier of F:] holds ex x1 be Point of G, x2 be Point of F st x = [x1, x2] by SUBSET_1: 43;

    definition

      let G,F be non empty addLoopStr;

      :: PRVECT_3:def1

      func prod_ADD (G,F) -> BinOp of [:the carrier of G, the carrier of F:] means

      : Def1: for g1,g2 be Point of G, f1,f2 be Point of F holds (it . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)];

      existence

      proof

        defpred ADP[ object, object, object] means ex g1,g2 be Point of G, f1,f2 be Point of F st $1 = [g1, f1] & $2 = [g2, f2] & $3 = [(g1 + g2), (f1 + f2)];

        

         A1: for x,y be object st x in [:the carrier of G, the carrier of F:] & y in [:the carrier of G, the carrier of F:] holds ex z be object st z in [:the carrier of G, the carrier of F:] & ADP[x, y, z]

        proof

          let x,y be object;

          assume

           A2: x in [:the carrier of G, the carrier of F:] & y in [:the carrier of G, the carrier of F:];

          then

          consider x1 be Point of G, x2 be Point of F such that

           A3: x = [x1, x2] by Lm1;

          consider y1 be Point of G, y2 be Point of F such that

           A4: y = [y1, y2] by Lm1, A2;

          reconsider z = [(x1 + y1), (x2 + y2)] as Element of [:the carrier of G, the carrier of F:];

          z in [:the carrier of G, the carrier of F:] & ADP[x, y, z] by A3, A4;

          hence thesis;

        end;

        consider ADGF be Function of [: [:the carrier of G, the carrier of F:], [:the carrier of G, the carrier of F:]:], [:the carrier of G, the carrier of F:] such that

         A5: for x,y be object st x in [:the carrier of G, the carrier of F:] & y in [:the carrier of G, the carrier of F:] holds ADP[x, y, (ADGF . (x,y))] from BINOP_1:sch 1( A1);

        now

          let g1,g2 be Point of G, f1,f2 be Point of F;

          consider gg1,gg2 be Point of G, ff1,ff2 be Point of F such that

           A6: [g1, f1] = [gg1, ff1] & [g2, f2] = [gg2, ff2] & (ADGF . ( [g1, f1], [g2, f2])) = [(gg1 + gg2), (ff1 + ff2)] by A5;

          g1 = gg1 & f1 = ff1 & g2 = gg2 & f2 = ff2 by A6, XTUPLE_0: 1;

          hence (ADGF . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)] by A6;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let H1,H2 be BinOp of [:the carrier of G, the carrier of F:];

        assume

         A7: for g1,g2 be Point of G, f1,f2 be Point of F holds (H1 . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)];

        assume

         A8: for g1,g2 be Point of G, f1,f2 be Point of F holds (H2 . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)];

        now

          let x,y be Element of [:the carrier of G, the carrier of F:];

          consider x1 be Point of G, x2 be Point of F such that

           A9: x = [x1, x2] by Lm1;

          consider y1 be Point of G, y2 be Point of F such that

           A10: y = [y1, y2] by Lm1;

          

          thus (H1 . (x,y)) = [(x1 + y1), (x2 + y2)] by A7, A9, A10

          .= (H2 . (x,y)) by A8, A9, A10;

        end;

        hence H1 = H2;

      end;

    end

    definition

      let G,F be non empty RLSStruct;

      :: PRVECT_3:def2

      func prod_MLT (G,F) -> Function of [: REAL , [:the carrier of G, the carrier of F:]:], [:the carrier of G, the carrier of F:] means

      : Def2: for r be Real, g be Point of G, f be Point of F holds (it . (r, [g, f])) = [(r * g), (r * f)];

      existence

      proof

        defpred MLT[ object, object, object] means ex r be Element of REAL , g be Point of G, f be Point of F st r = $1 & $2 = [g, f] & $3 = [(r * g), (r * f)];

        set CarrG = the carrier of G;

        set CarrF = the carrier of F;

        

         A1: for x,y be object st x in REAL & y in [:CarrG, CarrF:] holds ex z be object st z in [:CarrG, CarrF:] & MLT[x, y, z]

        proof

          let x,y be object;

          assume

           A2: x in REAL & y in [:CarrG, CarrF:];

          then

          reconsider r = x as Element of REAL ;

          consider y1 be Point of G, y2 be Point of F such that

           A3: y = [y1, y2] by A2, Lm1;

          set z = [(r * y1), (r * y2)];

          z in [:CarrG, CarrF:] & MLT[x, y, z] by A3;

          hence thesis;

        end;

        consider MLTGF be Function of [: REAL , [:CarrG, CarrF:]:], [:CarrG, CarrF:] such that

         A4: for x,y be object st x in REAL & y in [:CarrG, CarrF:] holds MLT[x, y, (MLTGF . (x,y))] from BINOP_1:sch 1( A1);

        now

          let r be Real, g be Point of G, f be Point of F;

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

           MLT[rr, [g, f], (MLTGF . (rr, [g, f]))] by A4;

          then

          consider rr be Element of REAL , gg be Point of G, ff be Point of F such that

           A5: rr = r & [g, f] = [gg, ff] & (MLTGF . (r, [g, f])) = [(rr * gg), (r * ff)];

          g = gg & f = ff by A5, XTUPLE_0: 1;

          hence (MLTGF . (r, [g, f])) = [(r * g), (r * f)] by A5;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let H1,H2 be Function of [: REAL , [:the carrier of G, the carrier of F:]:], [:the carrier of G, the carrier of F:];

        assume

         A6: for r be Real, g be Point of G, f be Point of F holds (H1 . (r, [g, f])) = [(r * g), (r * f)];

        assume

         A7: for r be Real, g be Point of G, f be Point of F holds (H2 . (r, [g, f])) = [(r * g), (r * f)];

        now

          let r be Element of REAL , x be Element of [:the carrier of G, the carrier of F:];

          consider x1 be Point of G, x2 be Point of F such that

           A8: x = [x1, x2] by Lm1;

          

          thus (H1 . (r,x)) = [(r * x1), (r * x2)] by A6, A8

          .= (H2 . (r,x)) by A7, A8;

        end;

        hence H1 = H2;

      end;

    end

    definition

      let G,F be non empty addLoopStr;

      :: PRVECT_3:def3

      func prod_ZERO (G,F) -> Element of [:the carrier of G, the carrier of F:] equals [( 0. G), ( 0. F)];

      correctness ;

    end

    definition

      let G,F be non empty addLoopStr;

      :: PRVECT_3:def4

      func [:G,F:] -> strict non empty addLoopStr equals addLoopStr (# [:the carrier of G, the carrier of F:], ( prod_ADD (G,F)), ( prod_ZERO (G,F)) #);

      correctness ;

    end

    registration

      let G,F be Abelian non empty addLoopStr;

      cluster [:G, F:] -> Abelian;

      correctness

      proof

        let x,y be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G, y2 be Point of F such that

         A2: y = [y1, y2] by Lm1;

        

        thus (x + y) = [(x1 + y1), (x2 + y2)] by A1, A2, Def1

        .= (y + x) by A1, A2, Def1;

      end;

    end

    registration

      let G,F be add-associative non empty addLoopStr;

      cluster [:G, F:] -> add-associative;

      correctness

      proof

        let x,y,z be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G, y2 be Point of F such that

         A2: y = [y1, y2] by Lm1;

        consider z1 be Point of G, z2 be Point of F such that

         A3: z = [z1, z2] by Lm1;

        

         A4: ((x1 + y1) + z1) = (x1 + (y1 + z1)) & ((x2 + y2) + z2) = (x2 + (y2 + z2)) by RLVECT_1:def 3;

        

        thus ((x + y) + z) = (( prod_ADD (G,F)) . ( [(x1 + y1), (x2 + y2)], [z1, z2])) by A1, A2, A3, Def1

        .= [((x1 + y1) + z1), ((x2 + y2) + z2)] by Def1

        .= (( prod_ADD (G,F)) . ( [x1, x2], [(y1 + z1), (y2 + z2)])) by A4, Def1

        .= (x + (y + z)) by A1, A2, A3, Def1;

      end;

    end

    registration

      let G,F be right_zeroed non empty addLoopStr;

      cluster [:G, F:] -> right_zeroed;

      correctness

      proof

        let x be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        (x1 + ( 0. G)) = x1 & (x2 + ( 0. F)) = x2 by RLVECT_1:def 4;

        hence (x + ( 0. [:G, F:])) = x by A1, Def1;

      end;

    end

    registration

      let G,F be right_complementable non empty addLoopStr;

      cluster [:G, F:] -> right_complementable;

      correctness

      proof

        let x be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G such that

         A2: (x1 + y1) = ( 0. G) by ALGSTR_0:def 11;

        consider y2 be Point of F such that

         A3: (x2 + y2) = ( 0. F) by ALGSTR_0:def 11;

        reconsider y = [y1, y2] as Element of [:G, F:];

        take y;

        thus thesis by A1, A2, A3, Def1;

      end;

    end

    theorem :: PRVECT_3:7

    for G,F be non empty addLoopStr holds (for x be set holds (x is Point of [:G, F:] iff ex x1 be Point of G, x2 be Point of F st x = [x1, x2])) & (for x,y be Point of [:G, F:], x1,y1 be Point of G, x2,y2 be Point of F st x = [x1, x2] & y = [y1, y2] holds (x + y) = [(x1 + y1), (x2 + y2)]) & ( 0. [:G, F:]) = [( 0. G), ( 0. F)] by Lm1, Def1;

    theorem :: PRVECT_3:8

    for G,F be add-associative right_zeroed right_complementable non empty addLoopStr, x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ( - x) = [( - x1), ( - x2)]

    proof

      let G,F be add-associative right_zeroed right_complementable non empty addLoopStr;

      let x be Point of [:G, F:];

      let x1 be Point of G, x2 be Point of F;

      assume

       A1: x = [x1, x2];

      reconsider y = [( - x1), ( - x2)] as Point of [:G, F:];

      (x + y) = [(x1 + ( - x1)), (x2 + ( - x2))] by A1, Def1

      .= [( 0. G), (x2 + ( - x2))] by RLVECT_1:def 10

      .= ( 0. [:G, F:]) by RLVECT_1:def 10;

      hence thesis by RLVECT_1:def 10;

    end;

    registration

      let G,F be Abelian add-associative right_zeroed right_complementable strict non empty addLoopStr;

      cluster [:G, F:] -> strict Abelian add-associative right_zeroed right_complementable;

      correctness ;

    end

    definition

      let G,F be non empty RLSStruct;

      :: PRVECT_3:def5

      func [:G,F:] -> strict non empty RLSStruct equals RLSStruct (# [:the carrier of G, the carrier of F:], ( prod_ZERO (G,F)), ( prod_ADD (G,F)), ( prod_MLT (G,F)) #);

      correctness ;

    end

    registration

      let G,F be Abelian non empty RLSStruct;

      cluster [:G, F:] -> Abelian;

      correctness

      proof

        let x,y be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G, y2 be Point of F such that

         A2: y = [y1, y2] by Lm1;

        (x + y) = [(x1 + y1), (x2 + y2)] by A1, A2, Def1;

        hence (x + y) = (y + x) by A1, A2, Def1;

      end;

    end

    registration

      let G,F be add-associative non empty RLSStruct;

      cluster [:G, F:] -> add-associative;

      correctness

      proof

        let x,y,z be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G, y2 be Point of F such that

         A2: y = [y1, y2] by Lm1;

        consider z1 be Point of G, z2 be Point of F such that

         A3: z = [z1, z2] by Lm1;

        

         A4: ((x1 + y1) + z1) = (x1 + (y1 + z1)) & ((x2 + y2) + z2) = (x2 + (y2 + z2)) by RLVECT_1:def 3;

        

        thus ((x + y) + z) = (( prod_ADD (G,F)) . ( [(x1 + y1), (x2 + y2)], [z1, z2])) by A1, A2, A3, Def1

        .= [(x1 + (y1 + z1)), (x2 + (y2 + z2))] by A4, Def1

        .= (( prod_ADD (G,F)) . ( [x1, x2], [(y1 + z1), (y2 + z2)])) by Def1

        .= (x + (y + z)) by A1, A2, A3, Def1;

      end;

    end

    registration

      let G,F be right_zeroed non empty RLSStruct;

      cluster [:G, F:] -> right_zeroed;

      correctness

      proof

        let x be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        (x1 + ( 0. G)) = x1 & (x2 + ( 0. F)) = x2 by RLVECT_1:def 4;

        hence (x + ( 0. [:G, F:])) = x by A1, Def1;

      end;

    end

    registration

      let G,F be right_complementable non empty RLSStruct;

      cluster [:G, F:] -> right_complementable;

      correctness

      proof

        let x be Element of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G such that

         A2: (x1 + y1) = ( 0. G) by ALGSTR_0:def 11;

        consider y2 be Point of F such that

         A3: (x2 + y2) = ( 0. F) by ALGSTR_0:def 11;

        reconsider y = [y1, y2] as Element of [:G, F:];

        take y;

        thus thesis by A1, A2, A3, Def1;

      end;

    end

    theorem :: PRVECT_3:9

    

     Th9: for G,F be non empty RLSStruct holds (for x be set holds (x is Point of [:G, F:] iff ex x1 be Point of G, x2 be Point of F st x = [x1, x2])) & (for x,y be Point of [:G, F:], x1,y1 be Point of G, x2,y2 be Point of F st x = [x1, x2] & y = [y1, y2] holds (x + y) = [(x1 + y1), (x2 + y2)]) & ( 0. [:G, F:]) = [( 0. G), ( 0. F)] & (for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F, a be Real st x = [x1, x2] holds (a * x) = [(a * x1), (a * x2)]) by Def2, Def1, Lm1;

    theorem :: PRVECT_3:10

    for G,F be add-associative right_zeroed right_complementable non empty RLSStruct, x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ( - x) = [( - x1), ( - x2)]

    proof

      let G,F be add-associative right_zeroed right_complementable non empty RLSStruct;

      let x be Point of [:G, F:], x1 be Point of G, x2 be Point of F;

      assume

       A1: x = [x1, x2];

      reconsider y = [( - x1), ( - x2)] as Point of [:G, F:];

      (x + y) = [(x1 + ( - x1)), (x2 + ( - x2))] by A1, Def1

      .= [( 0. G), (x2 + ( - x2))] by RLVECT_1:def 10

      .= ( 0. [:G, F:]) by RLVECT_1:def 10;

      hence thesis by RLVECT_1:def 10;

    end;

    registration

      let G,F be vector-distributive non empty RLSStruct;

      cluster [:G, F:] -> vector-distributive;

      correctness

      proof

        let a0 be Real, x,y be VECTOR of [:G, F:];

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

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        consider y1 be Point of G, y2 be Point of F such that

         A2: y = [y1, y2] by Lm1;

        

         A3: (a * (x1 + y1)) = ((a0 * x1) + (a0 * y1)) & (a * (x2 + y2)) = ((a0 * x2) + (a0 * y2)) by RLVECT_1:def 5;

        

        thus (a0 * (x + y)) = (( prod_MLT (G,F)) . (a, [(x1 + y1), (x2 + y2)])) by A1, A2, Def1

        .= [(a * (x1 + y1)), (a * (x2 + y2))] by Def2

        .= (( prod_ADD (G,F)) . ( [(a * x1), (a * x2)], [(a * y1), (a * y2)])) by A3, Def1

        .= (( prod_ADD (G,F)) . ((( prod_MLT (G,F)) . (a, [x1, x2])), [(a * y1), (a * y2)])) by Def2

        .= ((a0 * x) + (a0 * y)) by A1, A2, Def2;

      end;

    end

    registration

      let G,F be scalar-distributive non empty RLSStruct;

      cluster [:G, F:] -> scalar-distributive;

      correctness

      proof

        let a0,b0 be Real, x be VECTOR of [:G, F:];

        reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        

         A2: ((a + b) * x1) = ((a0 * x1) + (b0 * x1)) & ((a + b) * x2) = ((a0 * x2) + (b0 * x2)) by RLVECT_1:def 6;

        

        thus ((a0 + b0) * x) = [((a + b) * x1), ((a + b) * x2)] by A1, Def2

        .= (( prod_ADD (G,F)) . ( [(a * x1), (a * x2)], [(b * x1), (b * x2)])) by A2, Def1

        .= (( prod_ADD (G,F)) . ((( prod_MLT (G,F)) . (a, [x1, x2])), [(b * x1), (b * x2)])) by Def2

        .= ((a0 * x) + (b0 * x)) by A1, Def2;

      end;

    end

    registration

      let G,F be scalar-associative non empty RLSStruct;

      cluster [:G, F:] -> scalar-associative;

      correctness

      proof

        let a0,b0 be Real, x be VECTOR of [:G, F:];

        reconsider a = a0, b = b0 as Element of REAL by XREAL_0:def 1;

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        

         A2: ((a * b) * x1) = (a0 * (b0 * x1)) & ((a * b) * x2) = (a0 * (b0 * x2)) by RLVECT_1:def 7;

        

        thus ((a0 * b0) * x) = [((a * b) * x1), ((a * b) * x2)] by A1, Def2

        .= (( prod_MLT (G,F)) . (a, [(b * x1), (b * x2)])) by A2, Def2

        .= (a0 * (b0 * x)) by A1, Def2;

      end;

    end

    registration

      let G,F be scalar-unital non empty RLSStruct;

      cluster [:G, F:] -> scalar-unital;

      correctness

      proof

        let x be VECTOR of [:G, F:];

        consider x1 be Point of G, x2 be Point of F such that

         A1: x = [x1, x2] by Lm1;

        (1 * x1) = x1 & (1 * x2) = x2 by RLVECT_1:def 8;

        hence (1 * x) = x by A1, Def2;

      end;

    end

    registration

      let G be Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty RLSStruct;

      cluster <*G*> -> RealLinearSpace-yielding;

      correctness

      proof

        let S be set;

        assume S in ( rng <*G*>);

        then

        consider i be object such that

         A1: i in ( dom <*G*>) & ( <*G*> . i) = S by FUNCT_1:def 3;

        reconsider i as Element of NAT by A1;

        ( dom <*G*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

        then i = 1 by A1, TARSKI:def 1;

        hence S is RealLinearSpace by A1, FINSEQ_1: 40;

      end;

    end

    registration

      let G,F be Abelian add-associative right_zeroed right_complementable scalar-distributive vector-distributive scalar-associative scalar-unital non empty RLSStruct;

      cluster <*G, F*> -> RealLinearSpace-yielding;

      correctness

      proof

        let S be set;

        assume S in ( rng <*G, F*>);

        then

        consider i be object such that

         A1: i in ( dom <*G, F*>) & ( <*G, F*> . i) = S by FUNCT_1:def 3;

        ( dom <*G, F*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then i = 1 or i = 2 by A1, TARSKI:def 2;

        hence S is RealLinearSpace by A1, FINSEQ_1: 44;

      end;

    end

    begin

    theorem :: PRVECT_3:11

    

     Th11: for X be RealLinearSpace holds ex I be Function of X, ( product <*X*>) st I is one-to-one & I is onto & (for x be Point of X holds (I . x) = <*x*>) & (for v,w be Point of X holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of X, r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. X)) = ( 0. ( product <*X*>))

    proof

      let X be RealLinearSpace;

      set CarrX = the carrier of X;

      consider I be Function of CarrX, ( product <*CarrX*>) such that

       A1: I is one-to-one & I is onto & for x be object st x in CarrX holds (I . x) = <*x*> by Th4;

      ( len ( carr <*X*>)) = ( len <*X*>) by PRVECT_1:def 11;

      then

       A2: ( len ( carr <*X*>)) = 1 by FINSEQ_1: 40;

      

       A3: ( dom <*X*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      

       A4: ( <*X*> . 1) = X by FINSEQ_1:def 8;

      1 in {1} by TARSKI:def 1;

      then (( carr <*X*>) . 1) = the carrier of X by A3, A4, PRVECT_1:def 11;

      then

       A5: ( carr <*X*>) = <*CarrX*> by A2, FINSEQ_1: 40;

      then

      reconsider I as Function of X, ( product <*X*>);

      

       A6: for x be Point of X holds (I . x) = <*x*> by A1;

      

       A7: for v,w be Point of X holds (I . (v + w)) = ((I . v) + (I . w))

      proof

        let v,w be Point of X;

        

         A8: (I . v) = <*v*> & (I . w) = <*w*> & (I . (v + w)) = <*(v + w)*> by A1;

        

         A9: ( <*v*> . 1) = v & ( <*w*> . 1) = w by FINSEQ_1: 40;

        reconsider Iv = (I . v), Iw = (I . w) as Element of ( product ( carr <*X*>));

        1 in {1} by TARSKI:def 1;

        then

        reconsider j1 = 1 as Element of ( dom ( carr <*X*>)) by A2, FINSEQ_1: 2, FINSEQ_1:def 3;

        

         A10: (( addop <*X*>) . j1) = the addF of ( <*X*> . j1) by PRVECT_1:def 12;

        

         A11: (( [:( addop <*X*>):] . (Iv,Iw)) . j1) = ((( addop <*X*>) . j1) . ((Iv . j1),(Iw . j1))) by PRVECT_1:def 8

        .= (v + w) by A10, A8, A9, FINSEQ_1: 40;

        consider Ivw be Function such that

         A12: ((I . v) + (I . w)) = Ivw & ( dom Ivw) = ( dom ( carr <*X*>)) & for i be object st i in ( dom ( carr <*X*>)) holds (Ivw . i) in (( carr <*X*>) . i) by CARD_3:def 5;

        

         A13: ( dom Ivw) = ( Seg 1) by A2, A12, FINSEQ_1:def 3;

        then

        reconsider Ivw as FinSequence by FINSEQ_1:def 2;

        ( len Ivw) = 1 by A13, FINSEQ_1:def 3;

        hence thesis by A8, A12, A11, FINSEQ_1: 40;

      end;

      

       A14: for v be Point of X, r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of X, r be Element of REAL ;

        

         A15: (I . v) = <*v*> & (I . (r * v)) = <*(r * v)*> by A1;

        

         A16: ( <*v*> . 1) = v by FINSEQ_1: 40;

        1 in {1} by TARSKI:def 1;

        then

        reconsider j1 = 1 as Element of ( dom ( carr <*X*>)) by A2, FINSEQ_1: 2, FINSEQ_1:def 3;

        

         A17: (( multop <*X*>) . j1) = the Mult of ( <*X*> . j1) by PRVECT_2:def 8;

        reconsider Iv = (I . v) as Element of ( product ( carr <*X*>));

        

         A18: (( [:( multop <*X*>):] . (r,Iv)) . j1) = ((( multop <*X*>) . j1) . (r,(Iv . j1))) by PRVECT_2:def 2

        .= (r * v) by A17, A15, A16, FINSEQ_1: 40;

        consider Ivw be Function such that

         A19: (r * (I . v)) = Ivw & ( dom Ivw) = ( dom ( carr <*X*>)) & for i be object st i in ( dom ( carr <*X*>)) holds (Ivw . i) in (( carr <*X*>) . i) by CARD_3:def 5;

        

         A20: ( dom Ivw) = ( Seg 1) by A2, A19, FINSEQ_1:def 3;

        then

        reconsider Ivw as FinSequence by FINSEQ_1:def 2;

        ( len Ivw) = 1 by A20, FINSEQ_1:def 3;

        hence thesis by A15, A19, A18, FINSEQ_1: 40;

      end;

      (I . ( 0. X)) = (I . (( 0. X) + ( 0. X)))

      .= ((I . ( 0. X)) + (I . ( 0. X))) by A7;

      

      then ((I . ( 0. X)) - (I . ( 0. X))) = ((I . ( 0. X)) + ((I . ( 0. X)) - (I . ( 0. X)))) by RLVECT_1: 28

      .= ((I . ( 0. X)) + ( 0. ( product <*X*>))) by RLVECT_1: 15

      .= (I . ( 0. X));

      then ( 0. ( product <*X*>)) = (I . ( 0. X)) by RLVECT_1: 15;

      hence thesis by A1, A6, A5, A7, A14;

    end;

    registration

      let G,F be non empty RealLinearSpace-yielding FinSequence;

      cluster (G ^ F) -> RealLinearSpace-yielding;

      correctness

      proof

        let S be set;

        assume S in ( rng (G ^ F));

        then

        consider i be object such that

         A1: i in ( dom (G ^ F)) & ((G ^ F) . i) = S by FUNCT_1:def 3;

        reconsider i as Element of NAT by A1;

        per cases by A1, FINSEQ_1: 25;

          suppose

           A2: i in ( dom G);

          then

           A3: ((G ^ F) . i) = (G . i) by FINSEQ_1:def 7;

          (G . i) in ( rng G) by A2, FUNCT_1: 3;

          hence S is RealLinearSpace by A3, A1, PRVECT_2:def 3;

        end;

          suppose ex n be Nat st n in ( dom F) & i = (( len G) + n);

          then

          consider n be Nat such that

           A4: n in ( dom F) & i = (( len G) + n);

          

           A5: ((G ^ F) . i) = (F . n) by A4, FINSEQ_1:def 7;

          (F . n) in ( rng F) by A4, FUNCT_1: 3;

          hence S is RealLinearSpace by A5, A1, PRVECT_2:def 3;

        end;

      end;

    end

    theorem :: PRVECT_3:12

    

     Th12: for X,Y be RealLinearSpace holds ex I be Function of [:X, Y:], ( product <*X, Y*>) st I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*>) & (for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:X, Y:])) = ( 0. ( product <*X, Y*>))

    proof

      let X,Y be RealLinearSpace;

      set CarrX = the carrier of X;

      set CarrY = the carrier of Y;

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

       A1: I is one-to-one & I is onto & for x,y be object st x in CarrX & y in CarrY holds (I . (x,y)) = <*x, y*> by Th5;

      ( len ( carr <*X, Y*>)) = ( len <*X, Y*>) by PRVECT_1:def 11;

      then

       A2: ( len ( carr <*X, Y*>)) = 2 by FINSEQ_1: 44;

      then

       A3: ( dom ( carr <*X, Y*>)) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      ( len <*X, Y*>) = 2 by FINSEQ_1: 44;

      then

       A4: ( dom <*X, Y*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1:def 3;

      

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

      1 in {1, 2} & 2 in {1, 2} by TARSKI:def 2;

      then (( carr <*X, Y*>) . 1) = CarrX & (( carr <*X, Y*>) . 2) = CarrY by A4, A5, PRVECT_1:def 11;

      then

       A6: ( carr <*X, Y*>) = <*CarrX, CarrY*> by A2, FINSEQ_1: 44;

      then

      reconsider I as Function of [:X, Y:], ( product <*X, Y*>);

      

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

      

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

      proof

        let v,w be Point of [:X, Y:];

        consider x1 be Point of X, y1 be Point of Y such that

         A9: v = [x1, y1] by Lm1;

        consider x2 be Point of X, y2 be Point of Y such that

         A10: w = [x2, y2] by Lm1;

        (I . v) = (I . (x1,y1)) & (I . w) = (I . (x2,y2)) by A9, A10;

        then

         A11: (I . v) = <*x1, y1*> & (I . w) = <*x2, y2*> by A1;

        

         A12: (I . (v + w)) = (I . ((x1 + x2),(y1 + y2))) by A9, A10, Def1

        .= <*(x1 + x2), (y1 + y2)*> by A1;

        

         A13: ( <*x1, y1*> . 1) = x1 & ( <*x2, y2*> . 1) = x2 & ( <*x1, y1*> . 2) = y1 & ( <*x2, y2*> . 2) = y2 by FINSEQ_1: 44;

        reconsider Iv = (I . v), Iw = (I . w) as Element of ( product ( carr <*X, Y*>));

        reconsider j1 = 1, j2 = 2 as Element of ( dom ( carr <*X, Y*>)) by A3, TARSKI:def 2;

        

         A14: (( addop <*X, Y*>) . j1) = the addF of ( <*X, Y*> . j1) by PRVECT_1:def 12;

        

         A15: (( [:( addop <*X, Y*>):] . (Iv,Iw)) . j1) = ((( addop <*X, Y*>) . j1) . ((Iv . j1),(Iw . j1))) by PRVECT_1:def 8

        .= (x1 + x2) by A14, A11, A13, FINSEQ_1: 44;

        

         A16: (( addop <*X, Y*>) . j2) = the addF of ( <*X, Y*> . j2) by PRVECT_1:def 12;

        

         A17: (( [:( addop <*X, Y*>):] . (Iv,Iw)) . j2) = ((( addop <*X, Y*>) . j2) . ((Iv . j2),(Iw . j2))) by PRVECT_1:def 8

        .= (y1 + y2) by A16, A11, A13, FINSEQ_1: 44;

        consider Ivw be Function such that

         A18: ((I . v) + (I . w)) = Ivw & ( dom Ivw) = ( dom ( carr <*X, Y*>)) & for i be object st i in ( dom ( carr <*X, Y*>)) holds (Ivw . i) in (( carr <*X, Y*>) . i) by CARD_3:def 5;

        

         A19: ( dom Ivw) = ( Seg 2) by A2, A18, FINSEQ_1:def 3;

        then

        reconsider Ivw as FinSequence by FINSEQ_1:def 2;

        ( len Ivw) = 2 by A19, FINSEQ_1:def 3;

        hence thesis by A12, A18, A15, A17, FINSEQ_1: 44;

      end;

      

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

      proof

        let v be Point of [:X, Y:], r be Real;

        consider x1 be Point of X, y1 be Point of Y such that

         A21: v = [x1, y1] by Lm1;

        

         A22: (I . v) = (I . (x1,y1)) by A21

        .= <*x1, y1*> by A1;

        

         A23: (I . (r * v)) = (I . ((r * x1),(r * y1))) by A21, Def2

        .= <*(r * x1), (r * y1)*> by A1;

        

         A24: ( <*x1, y1*> . 1) = x1 & ( <*x1, y1*> . 2) = y1 by FINSEQ_1: 44;

        reconsider j1 = 1, j2 = 2 as Element of ( dom ( carr <*X, Y*>)) by A3, TARSKI:def 2;

        

         A25: (( multop <*X, Y*>) . j1) = the Mult of ( <*X, Y*> . j1) & (( multop <*X, Y*>) . j2) = the Mult of ( <*X, Y*> . j2) by PRVECT_2:def 8;

        reconsider Iv = (I . v) as Element of ( product ( carr <*X, Y*>));

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

        (( [:( multop <*X, Y*>):] . (rr,Iv)) . j1) = ((( multop <*X, Y*>) . j1) . (r,(Iv . j1))) & (( [:( multop <*X, Y*>):] . (rr,Iv)) . j2) = ((( multop <*X, Y*>) . j2) . (r,(Iv . j2))) by PRVECT_2:def 2;

        then

         A26: (( [:( multop <*X, Y*>):] . (rr,Iv)) . j1) = (r * x1) & (( [:( multop <*X, Y*>):] . (rr,Iv)) . j2) = (r * y1) by A25, A22, A24, FINSEQ_1: 44;

        consider Ivw be Function such that

         A27: (r * (I . v)) = Ivw & ( dom Ivw) = ( dom ( carr <*X, Y*>)) & for i be object st i in ( dom ( carr <*X, Y*>)) holds (Ivw . i) in (( carr <*X, Y*>) . i) by CARD_3:def 5;

        

         A28: ( dom Ivw) = ( Seg 2) by A2, A27, FINSEQ_1:def 3;

        then

        reconsider Ivw as FinSequence by FINSEQ_1:def 2;

        ( len Ivw) = 2 by A28, FINSEQ_1:def 3;

        hence thesis by A23, A27, A26, FINSEQ_1: 44;

      end;

      (I . ( 0. [:X, Y:])) = (I . (( 0. [:X, Y:]) + ( 0. [:X, Y:])))

      .= ((I . ( 0. [:X, Y:])) + (I . ( 0. [:X, Y:]))) by A8;

      

      then ((I . ( 0. [:X, Y:])) - (I . ( 0. [:X, Y:]))) = ((I . ( 0. [:X, Y:])) + ((I . ( 0. [:X, Y:])) - (I . ( 0. [:X, Y:])))) by RLVECT_1: 28

      .= ((I . ( 0. [:X, Y:])) + ( 0. ( product <*X, Y*>))) by RLVECT_1: 15

      .= (I . ( 0. [:X, Y:]));

      then ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) by RLVECT_1: 15;

      hence thesis by A7, A8, A20, A1, A6;

    end;

    

     Lm2: for X be non-empty non empty FinSequence, x be set st x in ( product X) holds x is FinSequence

    proof

      let X be non-empty non empty FinSequence, x be set;

      assume x in ( product X);

      then

      consider g be Function such that

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

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

      hence x is FinSequence by A1, FINSEQ_1:def 2;

    end;

    theorem :: PRVECT_3:13

    

     Th13: for X,Y be non empty RealLinearSpace-Sequence holds ex I be Function of [:( product X), ( product Y):], ( product (X ^ Y)) st I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), ( product Y):] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), ( product Y):], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), ( product Y):])) = ( 0. ( product (X ^ Y)))

    proof

      let X,Y be non empty RealLinearSpace-Sequence;

      reconsider CX = ( carr X), CY = ( carr Y) as non-empty non empty FinSequence;

      

       A1: ( len CX) = ( len X) & ( len CY) = ( len Y) & ( len ( carr (X ^ Y))) = ( len (X ^ Y)) by PRVECT_1:def 11;

      consider I be Function of [:( product CX), ( product CY):], ( product (CX ^ CY)) such that

       A2: I is one-to-one & I is onto & for x,y be FinSequence st x in ( product CX) & y in ( product CY) holds (I . (x,y)) = (x ^ y) by Th6;

      set PX = ( product X);

      set PY = ( product Y);

      ( len ( carr (X ^ Y))) = (( len X) + ( len Y)) & ( len (CX ^ CY)) = (( len X) + ( len Y)) by A1, FINSEQ_1: 22;

      then

       A3: ( dom ( carr (X ^ Y))) = ( dom (CX ^ CY)) by FINSEQ_3: 29;

      

       A4: for k be Nat st k in ( dom ( carr (X ^ Y))) holds (( carr (X ^ Y)) . k) = ((CX ^ CY) . k)

      proof

        let k be Nat;

        assume

         A5: k in ( dom ( carr (X ^ Y)));

        then

        reconsider k1 = k as Element of ( dom (X ^ Y)) by A1, FINSEQ_3: 29;

        

         A6: (( carr (X ^ Y)) . k) = the carrier of ((X ^ Y) . k1) by PRVECT_1:def 11;

        

         A7: k in ( dom (X ^ Y)) by A1, A5, FINSEQ_3: 29;

        per cases by A7, FINSEQ_1: 25;

          suppose

           A8: k in ( dom X);

          then

           A9: k in ( dom CX) by A1, FINSEQ_3: 29;

          reconsider k2 = k1 as Element of ( dom X) by A8;

          

          thus (( carr (X ^ Y)) . k) = the carrier of (X . k2) by A6, FINSEQ_1:def 7

          .= (CX . k) by PRVECT_1:def 11

          .= ((CX ^ CY) . k) by A9, FINSEQ_1:def 7;

        end;

          suppose ex n be Nat st n in ( dom Y) & k = (( len X) + n);

          then

          consider n be Nat such that

           A10: n in ( dom Y) & k = (( len X) + n);

          

           A11: n in ( dom CY) by A1, A10, FINSEQ_3: 29;

          reconsider n1 = n as Element of ( dom Y) by A10;

          

          thus (( carr (X ^ Y)) . k) = the carrier of (Y . n1) by A6, A10, FINSEQ_1:def 7

          .= (CY . n) by PRVECT_1:def 11

          .= ((CX ^ CY) . k) by A11, A10, A1, FINSEQ_1:def 7;

        end;

      end;

      then

       A12: ( carr (X ^ Y)) = (CX ^ CY) by A3, FINSEQ_1: 13;

      reconsider I as Function of [:PX, PY:], ( product (X ^ Y)) by A3, A4, FINSEQ_1: 13;

      

       A13: for x be Point of ( product X), y be Point of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1)

      proof

        let x be Point of PX, y be Point of PY;

        reconsider x1 = x, y1 = y as FinSequence by Lm2;

        (I . (x,y)) = (x1 ^ y1) by A2;

        hence thesis;

      end;

      

       A14: for v,w be Point of [:PX, PY:] holds (I . (v + w)) = ((I . v) + (I . w))

      proof

        let v,w be Point of [:PX, PY:];

        consider x1 be Point of PX, y1 be Point of PY such that

         A15: v = [x1, y1] by Lm1;

        consider x2 be Point of PX, y2 be Point of PY such that

         A16: w = [x2, y2] by Lm1;

        reconsider xx1 = x1, xx2 = x2 as FinSequence by Lm2;

        reconsider yy1 = y1, yy2 = y2 as FinSequence by Lm2;

        reconsider xx12 = (x1 + x2), yy12 = (y1 + y2) as FinSequence by Lm2;

        

         A17: ( dom xx1) = ( dom CX) & ( dom xx2) = ( dom CX) & ( dom xx12) = ( dom CX) & ( dom yy1) = ( dom CY) & ( dom yy2) = ( dom CY) & ( dom yy12) = ( dom CY) by CARD_3: 9;

        (I . v) = (I . (x1,y1)) & (I . w) = (I . (x2,y2)) by A15, A16;

        then

         A18: (I . v) = (xx1 ^ yy1) & (I . w) = (xx2 ^ yy2) by A2;

        (I . (v + w)) = (I . ((x1 + x2),(y1 + y2))) by A15, A16, Def1;

        then

         A19: (I . (v + w)) = (xx12 ^ yy12) by A2;

        then

         A20: ( dom (xx12 ^ yy12)) = ( dom ( carr (X ^ Y))) by CARD_3: 9;

        reconsider Iv = (I . v), Iw = (I . w) as Element of ( product ( carr (X ^ Y)));

        reconsider Ivw = ((I . v) + (I . w)) as FinSequence by Lm2;

        

         A21: ( dom Ivw) = ( dom ( carr (X ^ Y))) by CARD_3: 9;

        for j0 be Nat st j0 in ( dom Ivw) holds (Ivw . j0) = ((xx12 ^ yy12) . j0)

        proof

          let j0 be Nat;

          assume j0 in ( dom Ivw);

          then

          reconsider j = j0 as Element of ( dom ( carr (X ^ Y))) by CARD_3: 9;

          

           A22: (Ivw . j0) = ((( addop (X ^ Y)) . j) . ((Iv . j),(Iw . j))) by PRVECT_1:def 8

          .= (the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j))) by PRVECT_1:def 12;

          per cases by A22, A3, FINSEQ_1: 25;

            suppose

             A23: j0 in ( dom CX);

            then j0 in ( dom X) by A1, FINSEQ_3: 29;

            then

             A24: ((X ^ Y) . j) = (X . j0) by FINSEQ_1:def 7;

            

             A25: (Iv . j) = (xx1 . j) & (Iw . j) = (xx2 . j) by A23, A17, A18, FINSEQ_1:def 7;

            

             A26: ((xx12 ^ yy12) . j0) = (xx12 . j0) by A23, A17, FINSEQ_1:def 7;

            reconsider j1 = j0 as Element of ( dom ( carr X)) by A23;

            (the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j))) = ((( addop X) . j1) . ((xx1 . j1),(xx2 . j1))) by A24, A25, PRVECT_1:def 12

            .= ((xx12 ^ yy12) . j0) by A26, PRVECT_1:def 8;

            hence (Ivw . j0) = ((xx12 ^ yy12) . j0) by A22;

          end;

            suppose ex n be Nat st n in ( dom CY) & j0 = (( len CX) + n);

            then

            consider n be Nat such that

             A27: n in ( dom CY) & j0 = (( len CX) + n);

            

             A28: ( len CX) = ( len xx1) & ( len CX) = ( len xx2) & ( len CX) = ( len xx12) by A17, FINSEQ_3: 29;

            n in ( dom Y) by A1, A27, FINSEQ_3: 29;

            then

             A29: ((X ^ Y) . j) = (Y . n) by A27, A1, FINSEQ_1:def 7;

            

             A30: (Iv . j) = (yy1 . n) & (Iw . j) = (yy2 . n) by A17, A18, A27, A28, FINSEQ_1:def 7;

            

             A31: ((xx12 ^ yy12) . j0) = (yy12 . n) by A27, A28, A17, FINSEQ_1:def 7;

            reconsider j1 = n as Element of ( dom ( carr Y)) by A27;

            (the addF of ((X ^ Y) . j) . ((Iv . j),(Iw . j))) = ((( addop Y) . j1) . ((yy1 . j1),(yy2 . j1))) by A29, A30, PRVECT_1:def 12

            .= ((xx12 ^ yy12) . j0) by A31, PRVECT_1:def 8;

            hence (Ivw . j0) = ((xx12 ^ yy12) . j0) by A22;

          end;

        end;

        hence thesis by A19, A20, A21, FINSEQ_1: 13;

      end;

      

       A32: for v be Point of [:PX, PY:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of [:PX, PY:], r be Element of REAL ;

        consider x1 be Point of PX, y1 be Point of PY such that

         A33: v = [x1, y1] by Lm1;

        reconsider xx1 = x1, yy1 = y1 as FinSequence by Lm2;

        reconsider rxx1 = (r * x1), ryy1 = (r * y1) as FinSequence by Lm2;

        

         A34: ( dom xx1) = ( dom CX) & ( dom yy1) = ( dom CY) & ( dom rxx1) = ( dom CX) & ( dom ryy1) = ( dom CY) by CARD_3: 9;

        

         A35: (I . v) = (I . (x1,y1)) by A33

        .= (xx1 ^ yy1) by A2;

        

         A36: (I . (r * v)) = (I . ((r * x1),(r * y1))) by A33, Def2

        .= (rxx1 ^ ryy1) by A2;

        reconsider Iv = (I . v) as Element of ( product ( carr (X ^ Y)));

        reconsider rIv = (r * (I . v)) as FinSequence by Lm2;

        

         A37: ( dom rIv) = ( dom ( carr (X ^ Y))) by CARD_3: 9;

        

         A38: ( dom (rxx1 ^ ryy1)) = ( dom ( carr (X ^ Y))) by A36, CARD_3: 9;

        for j0 be Nat st j0 in ( dom rIv) holds (rIv . j0) = ((rxx1 ^ ryy1) . j0)

        proof

          let j0 be Nat;

          assume

           A39: j0 in ( dom rIv);

          then

          reconsider j = j0 as Element of ( dom ( carr (X ^ Y))) by CARD_3: 9;

          

           A40: (rIv . j0) = ((( multop (X ^ Y)) . j) . (r,(Iv . j))) by PRVECT_2:def 2

          .= (the Mult of ((X ^ Y) . j) . (r,(Iv . j))) by PRVECT_2:def 8;

          per cases by A3, A39, A37, FINSEQ_1: 25;

            suppose

             A41: j0 in ( dom CX);

            then j0 in ( dom X) by A1, FINSEQ_3: 29;

            then

             A42: ((X ^ Y) . j) = (X . j0) by FINSEQ_1:def 7;

            

             A43: (Iv . j) = (xx1 . j) by A41, A34, A35, FINSEQ_1:def 7;

            

             A44: ((rxx1 ^ ryy1) . j0) = (rxx1 . j0) by A41, A34, FINSEQ_1:def 7;

            reconsider j1 = j0 as Element of ( dom ( carr X)) by A41;

            (the Mult of ((X ^ Y) . j) . (r,(Iv . j))) = ((( multop X) . j1) . (r,(xx1 . j1))) by A42, A43, PRVECT_2:def 8

            .= ((rxx1 ^ ryy1) . j0) by A44, PRVECT_2:def 2;

            hence (rIv . j0) = ((rxx1 ^ ryy1) . j0) by A40;

          end;

            suppose ex n be Nat st n in ( dom CY) & j0 = (( len CX) + n);

            then

            consider n be Nat such that

             A45: n in ( dom CY) & j0 = (( len CX) + n);

            

             A46: ( len CX) = ( len xx1) & ( len CX) = ( len rxx1) by A34, FINSEQ_3: 29;

            n in ( dom Y) by A45, A1, FINSEQ_3: 29;

            then

             A47: ((X ^ Y) . j) = (Y . n) by A45, A1, FINSEQ_1:def 7;

            

             A48: (Iv . j) = (yy1 . n) by A35, A45, A34, A46, FINSEQ_1:def 7;

            

             A49: ((rxx1 ^ ryy1) . j0) = (ryy1 . n) by A45, A46, A34, FINSEQ_1:def 7;

            reconsider j1 = n as Element of ( dom ( carr Y)) by A45;

            (the Mult of ((X ^ Y) . j) . (r,(Iv . j))) = ((( multop Y) . j1) . (r,(yy1 . j1))) by A47, A48, PRVECT_2:def 8

            .= ((rxx1 ^ ryy1) . j0) by A49, PRVECT_2:def 2;

            hence (rIv . j0) = ((rxx1 ^ ryy1) . j0) by A40;

          end;

        end;

        hence thesis by A36, A38, A37, FINSEQ_1: 13;

      end;

      (I . ( 0. [:PX, PY:])) = (I . (( 0. [:PX, PY:]) + ( 0. [:PX, PY:])))

      .= ((I . ( 0. [:PX, PY:])) + (I . ( 0. [:PX, PY:]))) by A14;

      

      then ((I . ( 0. [:PX, PY:])) - (I . ( 0. [:PX, PY:]))) = ((I . ( 0. [:PX, PY:])) + ((I . ( 0. [:PX, PY:])) - (I . ( 0. [:PX, PY:])))) by RLVECT_1: 28

      .= ((I . ( 0. [:PX, PY:])) + ( 0. ( product (X ^ Y)))) by RLVECT_1: 15

      .= (I . ( 0. [:PX, PY:]));

      then ( 0. ( product (X ^ Y))) = (I . ( 0. [:PX, PY:])) by RLVECT_1: 15;

      hence thesis by A13, A14, A32, A2, A12;

    end;

    theorem :: PRVECT_3:14

    for G,F be RealLinearSpace holds (for x be set holds (x is Point of ( product <*G, F*>) iff ex x1 be Point of G, x2 be Point of F st x = <*x1, x2*>)) & (for x,y be Point of ( product <*G, F*>), x1,y1 be Point of G, x2,y2 be Point of F st x = <*x1, x2*> & y = <*y1, y2*> holds (x + y) = <*(x1 + y1), (x2 + y2)*>) & ( 0. ( product <*G, F*>)) = <*( 0. G), ( 0. F)*> & (for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>) & (for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F, a be Real st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>)

    proof

      let G,F be RealLinearSpace;

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

       A1: I is one-to-one & I is onto & (for x be Point of G, y be Point of F holds (I . (x,y)) = <*x, y*>) & (for v,w be Point of [:G, F:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:G, F:], r be Real holds (I . (r * v)) = (r * (I . v))) & ( 0. ( product <*G, F*>)) = (I . ( 0. [:G, F:])) by Th12;

      thus

       A2: for x be set holds (x is Point of ( product <*G, F*>) iff ex x1 be Point of G, x2 be Point of F st x = <*x1, x2*>)

      proof

        let y be set;

        hereby

          assume y is Point of ( product <*G, F*>);

          then y in the carrier of ( product <*G, F*>);

          then y in ( rng I) by A1, FUNCT_2:def 3;

          then

          consider x be Element of the carrier of [:G, F:] such that

           A3: y = (I . x) by FUNCT_2: 113;

          consider x1 be Point of G, x2 be Point of F such that

           A4: x = [x1, x2] by Lm1;

          take x1, x2;

          (I . (x1,x2)) = <*x1, x2*> by A1;

          hence y = <*x1, x2*> by A3, A4;

        end;

        now

          assume ex x1 be Point of G, x2 be Point of F st y = <*x1, x2*>;

          then

          consider x1 be Point of G, x2 be Point of F such that

           A5: y = <*x1, x2*>;

          

           A6: (I . [x1, x2]) in ( rng I) by FUNCT_2: 112;

          (I . (x1,x2)) = <*x1, x2*> by A1;

          hence y is Point of ( product <*G, F*>) by A5, A6;

        end;

        hence thesis;

      end;

      thus

       A7: for x,y be Point of ( product <*G, F*>), x1,y1 be Point of G, x2,y2 be Point of F st x = <*x1, x2*> & y = <*y1, y2*> holds (x + y) = <*(x1 + y1), (x2 + y2)*>

      proof

        let x,y be Point of ( product <*G, F*>);

        let x1,y1 be Point of G, x2,y2 be Point of F;

        assume

         A8: x = <*x1, x2*> & y = <*y1, y2*>;

        reconsider z = [x1, x2], w = [y1, y2] as Point of [:G, F:];

        

         A9: (z + w) = [(x1 + y1), (x2 + y2)] by Def1;

        (I . ((x1 + y1),(x2 + y2))) = <*(x1 + y1), (x2 + y2)*> & (I . (x1,x2)) = <*x1, x2*> & (I . (y1,y2)) = <*y1, y2*> by A1;

        hence <*(x1 + y1), (x2 + y2)*> = (x + y) by A1, A9, A8;

      end;

      thus

       A10: ( 0. ( product <*G, F*>)) = <*( 0. G), ( 0. F)*>

      proof

        (I . (( 0. G),( 0. F))) = <*( 0. G), ( 0. F)*> by A1;

        hence thesis by A1;

      end;

      thus for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>

      proof

        let x be Point of ( product <*G, F*>);

        let x1 be Point of G, x2 be Point of F;

        assume

         A11: x = <*x1, x2*>;

        reconsider y = <*( - x1), ( - x2)*> as Point of ( product <*G, F*>) by A2;

        (x + y) = <*(x1 + ( - x1)), (x2 + ( - x2))*> by A7, A11

        .= <*( 0. G), (x2 + ( - x2))*> by RLVECT_1:def 10

        .= ( 0. ( product <*G, F*>)) by A10, RLVECT_1:def 10;

        hence thesis by RLVECT_1:def 10;

      end;

      thus for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F, a be Real st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>

      proof

        let x be Point of ( product <*G, F*>);

        let x1 be Point of G, x2 be Point of F, a be Real;

        assume

         A12: x = <*x1, x2*>;

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

        reconsider y = [x1, x2] as Point of [:G, F:];

        

         A13: <*x1, x2*> = (I . (x1,x2)) by A1;

        (I . (a * y)) = (I . ((a0 * x1),(a0 * x2))) by Th9

        .= <*(a0 * x1), (a0 * x2)*> by A1;

        hence thesis by A1, A12, A13;

      end;

    end;

    begin

    definition

      let G,F be non empty NORMSTR;

      :: PRVECT_3:def6

      func prod_NORM (G,F) -> Function of [:the carrier of G, the carrier of F:], REAL means

      : Def6: for g be Point of G, f be Point of F holds ex v be Element of ( REAL 2) st v = <* ||.g.||, ||.f.||*> & (it . (g,f)) = |.v.|;

      existence

      proof

        defpred NRM[ object, object, object] means ex g be Point of G, f be Point of F, v be Element of ( REAL 2) st $1 = g & $2 = f & v = <* ||.g.||, ||.f.||*> & $3 = |.v.|;

        

         A1: for x,y be object st x in the carrier of G & y in the carrier of F holds ex z be object st z in REAL & NRM[x, y, z]

        proof

          let x,y be object;

          assume

           A2: x in the carrier of G & y in the carrier of F;

          then

          reconsider g = x as Point of G;

          reconsider f = y as Point of F by A2;

          reconsider v = <* ||.g.||, ||.f.||*> as Element of ( REAL 2) by FINSEQ_2: 101;

           |.v.| in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider NORMGF be Function of [:the carrier of G, the carrier of F:], REAL such that

         A3: for x,y be object st x in the carrier of G & y in the carrier of F holds NRM[x, y, (NORMGF . (x,y))] from BINOP_1:sch 1( A1);

        now

          let g be Point of G, f be Point of F;

          ex gg be Point of G, ff be Point of F, v be Element of ( REAL 2) st g = gg & f = ff & v = <* ||.gg.||, ||.ff.||*> & (NORMGF . (g,f)) = |.v.| by A3;

          hence ex v be Element of ( REAL 2) st v = <* ||.g.||, ||.f.||*> & (NORMGF . (g,f)) = |.v.|;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let H1,H2 be Function of [:the carrier of G, the carrier of F:], REAL ;

        assume

         A4: for g be Point of G, f be Point of F holds ex v be Element of ( REAL 2) st v = <* ||.g.||, ||.f.||*> & (H1 . (g,f)) = |.v.|;

        assume

         A5: for g be Point of G, f be Point of F holds ex v be Element of ( REAL 2) st v = <* ||.g.||, ||.f.||*> & (H2 . (g,f)) = |.v.|;

        now

          let g be Element of the carrier of G, f be Element of the carrier of F;

          

           A6: ex v1 be Element of ( REAL 2) st v1 = <* ||.g.||, ||.f.||*> & (H1 . (g,f)) = |.v1.| by A4;

          ex v2 be Element of ( REAL 2) st v2 = <* ||.g.||, ||.f.||*> & (H2 . (g,f)) = |.v2.| by A5;

          hence (H1 . (g,f)) = (H2 . (g,f)) by A6;

        end;

        hence H1 = H2;

      end;

    end

    definition

      let G,F be non empty NORMSTR;

      :: PRVECT_3:def7

      func [:G,F:] -> strict non empty NORMSTR equals NORMSTR (# [:the carrier of G, the carrier of F:], ( prod_ZERO (G,F)), ( prod_ADD (G,F)), ( prod_MLT (G,F)), ( prod_NORM (G,F)) #);

      correctness ;

    end

    registration

      let G,F be RealNormSpace;

      cluster [:G, F:] -> reflexive discerning RealNormSpace-like;

      correctness

      proof

        now

          let x be Point of [:G, F:];

          consider x1 be Point of G, x2 be Point of F such that

           A1: x = [x1, x2] by Lm1;

          consider v be Element of ( REAL 2) such that

           A2: v = <* ||.x1.||, ||.x2.||*> & (( prod_NORM (G,F)) . (x1,x2)) = |.v.| by Def6;

          assume x = ( 0. [:G, F:]);

          then x1 = ( 0. G) & x2 = ( 0. F) by A1, XTUPLE_0: 1;

          then ||.x1.|| = 0 & ||.x2.|| = 0 ;

          then v = ( 0* 2) by A2, FINSEQ_2: 61;

          hence ||.x.|| = 0 by A2, A1, EUCLID: 7;

        end;

        then ||.( 0. [:G, F:]).|| = 0 ;

        hence [:G, F:] is reflexive;

        now

          let x be Point of [:G, F:];

          consider x1 be Point of G, x2 be Point of F such that

           A3: x = [x1, x2] by Lm1;

          consider v be Element of ( REAL 2) such that

           A4: v = <* ||.x1.||, ||.x2.||*> & (( prod_NORM (G,F)) . (x1,x2)) = |.v.| by Def6;

          assume ||.x.|| = 0 ;

          then v = ( 0* 2) by A4, A3, EUCLID: 8;

          then

           A5: v = <* 0 , 0 *> by FINSEQ_2: 61;

           ||.x1.|| = (v . 1) & ||.x2.|| = (v . 2) by A4, FINSEQ_1: 44;

          then ||.x1.|| = 0 & ||.x2.|| = 0 by A5, FINSEQ_1: 44;

          then x1 = ( 0. G) & x2 = ( 0. F) by NORMSP_0:def 5;

          hence x = ( 0. [:G, F:]) by A3;

        end;

        hence [:G, F:] is discerning;

        now

          let x,y be Point of [:G, F:], a be Real;

          consider x1 be Point of G, x2 be Point of F such that

           A6: x = [x1, x2] by Lm1;

          consider y1 be Point of G, y2 be Point of F such that

           A7: y = [y1, y2] by Lm1;

          consider v be Element of ( REAL 2) such that

           A8: v = <* ||.x1.||, ||.x2.||*> & (( prod_NORM (G,F)) . (x1,x2)) = |.v.| by Def6;

          consider z be Element of ( REAL 2) such that

           A9: z = <* ||.y1.||, ||.y2.||*> & (( prod_NORM (G,F)) . (y1,y2)) = |.z.| by Def6;

          thus ||.(a * x).|| = ( |.a.| * ||.x.||)

          proof

            consider w be Element of ( REAL 2) such that

             A10: w = <* ||.(a * x1).||, ||.(a * x2).||*> & (( prod_NORM (G,F)) . ((a * x1),(a * x2))) = |.w.| by Def6;

            reconsider aa = |.a.|, xx1 = ||.x1.||, xx2 = ||.x2.|| as Real;

             ||.(a * x1).|| = ( |.a.| * ||.x1.||) & ||.(a * x2).|| = ( |.a.| * ||.x2.||) by NORMSP_1:def 1;

            

            then w = (aa * |[xx1, xx2]|) by A10, EUCLID: 58

            .= ( |.a.| * v) by A8, EUCLID: 65;

            

            then |.w.| = ( |. |.a.|.| * |.v.|) by EUCLID: 11

            .= ( |.a.| * |.v.|);

            hence thesis by A8, A10, A6, Def2;

          end;

          thus ||.(x + y).|| <= ( ||.x.|| + ||.y.||)

          proof

            consider w be Element of ( REAL 2) such that

             A11: w = <* ||.(x1 + y1).||, ||.(x2 + y2).||*> & (( prod_NORM (G,F)) . ((x1 + y1),(x2 + y2))) = |.w.| by Def6;

            

             A12: ||.(x + y).|| = |.w.| by A11, A6, A7, Def1;

            

             A13: ||.(x1 + y1).|| <= ( ||.x1.|| + ||.y1.||) & ||.(x2 + y2).|| <= ( ||.x2.|| + ||.y2.||) by NORMSP_1:def 1;

            reconsider t1 = ( ||.x1.|| + ||.y1.||), t2 = ( ||.x2.|| + ||.y2.||) as Element of REAL by XREAL_0:def 1;

            reconsider t = <*t1, t2*> as FinSequence of REAL ;

            

             A14: ( len w) = 2 & ( len t) = 2 by A11, FINSEQ_1: 44;

            now

              let i be Element of NAT ;

              assume i in ( Seg ( len w));

              then

               A15: i in ( Seg 2) by A11, FINSEQ_1: 44;

              per cases by A15, FINSEQ_1: 2, TARSKI:def 2;

                suppose

                 A16: i = 1;

                then (w . i) = ||.(x1 + y1).|| by A11, FINSEQ_1: 44;

                hence 0 <= (w . i) & (w . i) <= (t . i) by A13, A16, FINSEQ_1: 44, NORMSP_1: 4;

              end;

                suppose

                 A17: i = 2;

                then (w . i) = ||.(x2 + y2).|| by A11, FINSEQ_1: 44;

                hence 0 <= (w . i) & (w . i) <= (t . i) by A13, A17, FINSEQ_1: 44, NORMSP_1: 4;

              end;

            end;

            then

             A18: |.w.| <= |.t.| by A14, PRVECT_2: 2;

            t = ( |[ ||.x1.||, ||.x2.||]| + |[ ||.y1.||, ||.y2.||]|) by EUCLID: 56

            .= (v + z) by A8, A9, EUCLID: 64;

            then |.t.| <= ( |.v.| + |.z.|) by EUCLID: 12;

            hence thesis by A12, A6, A8, A7, A9, A18, XXREAL_0: 2;

          end;

        end;

        hence thesis by NORMSP_1:def 1;

      end;

    end

    registration

      let G,F be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR;

      cluster [:G, F:] -> strict reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable;

      correctness

      proof

        reconsider G0 = G, F0 = F as RealLinearSpace;

         the RLSStruct of [:G, F:] = [:G0, F0:];

        hence thesis by RSSPACE3: 2;

      end;

    end

    registration

      let G be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR;

      cluster <*G*> -> RealNormSpace-yielding;

      correctness

      proof

        let S be set;

        assume S in ( rng <*G*>);

        then

        consider i be object such that

         A1: i in ( dom <*G*>) & ( <*G*> . i) = S by FUNCT_1:def 3;

        reconsider i as Element of NAT by A1;

        ( len <*G*>) = 1 by FINSEQ_1: 40;

        then ( dom <*G*>) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

        then i = 1 by A1, TARSKI:def 1;

        hence S is RealNormSpace by A1, FINSEQ_1: 40;

      end;

    end

    registration

      let G,F be reflexive discerning RealNormSpace-like scalar-distributive vector-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed right_complementable non empty NORMSTR;

      cluster <*G, F*> -> RealNormSpace-yielding;

      correctness

      proof

        let S be set;

        assume S in ( rng <*G, F*>);

        then

        consider i be object such that

         A1: i in ( dom <*G, F*>) & ( <*G, F*> . i) = S by FUNCT_1:def 3;

        reconsider i as Element of NAT by A1;

        ( dom <*G, F*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        then i = 1 or i = 2 by A1, TARSKI:def 2;

        hence S is RealNormSpace by A1, FINSEQ_1: 44;

      end;

    end

    theorem :: PRVECT_3:15

    

     Th15: for X,Y be RealNormSpace holds ex I be Function of [:X, Y:], ( product <*X, Y*>) st I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*>) & (for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v))) & ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) & (for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.||)

    proof

      let X,Y be RealNormSpace;

      reconsider X0 = X, Y0 = Y as RealLinearSpace;

      consider I0 be Function of [:X0, Y0:], ( product <*X0, Y0*>) such that

       A1: I0 is one-to-one & I0 is onto & (for x be Point of X, y be Point of Y holds (I0 . (x,y)) = <*x, y*>) & (for v,w be Point of [:X0, Y0:] holds (I0 . (v + w)) = ((I0 . v) + (I0 . w))) & (for v be Point of [:X0, Y0:], r be Real holds (I0 . (r * v)) = (r * (I0 . v))) & ( 0. ( product <*X0, Y0*>)) = (I0 . ( 0. [:X0, Y0:])) by Th12;

      

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

      then

      reconsider I = I0 as Function of [:X, Y:], ( product <*X, Y*>);

      take I;

      thus I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*>) by A1, A2;

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

      proof

        let v,w be Point of [:X, Y:];

        reconsider v0 = v, w0 = w as Point of [:X0, Y0:];

        

        thus (I . (v + w)) = (I0 . (v0 + w0))

        .= ((I0 . v0) + (I0 . w0)) by A1

        .= ((I . v) + (I . w)) by A2;

      end;

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

      proof

        let v be Point of [:X, Y:], r be Real;

        reconsider v0 = v as Point of [:X0, Y0:];

        

        thus (I . (r * v)) = (I0 . (r * v0))

        .= (r * (I0 . v0)) by A1

        .= (r * (I . v)) by A2;

      end;

      thus ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) by A1, A2;

      for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.||

      proof

        let v be Point of [:X, Y:];

        consider x1 be Point of X, y1 be Point of Y such that

         A3: v = [x1, y1] by Lm1;

        consider v1 be Element of ( REAL 2) such that

         A4: v1 = <* ||.x1.||, ||.y1.||*> & (( prod_NORM (X,Y)) . (x1,y1)) = |.v1.| by Def6;

        

         A5: (I . v) = (I . (x1,y1)) by A3

        .= <*x1, y1*> by A1;

        reconsider Iv = (I . v) as Element of ( product ( carr <*X, Y*>)) by A2;

        

         A6: ( <*x1, y1*> . 1) = x1 & ( <*x1, y1*> . 2) = y1 by FINSEQ_1: 44;

        1 in {1, 2} & 2 in {1, 2} by TARSKI:def 2;

        then

        reconsider j1 = 1, j2 = 2 as Element of ( dom <*X, Y*>) by FINSEQ_1: 2, FINSEQ_1: 89;

        

         A7: (( normsequence ( <*X, Y*>,Iv)) . j1) = (the normF of ( <*X, Y*> . j1) . (Iv . j1)) by PRVECT_2:def 11

        .= ||.x1.|| by A5, A6, FINSEQ_1: 44;

        

         A8: (( normsequence ( <*X, Y*>,Iv)) . j2) = (the normF of ( <*X, Y*> . j2) . (Iv . j2)) by PRVECT_2:def 11

        .= ||.y1.|| by A5, A6, FINSEQ_1: 44;

        ( len ( normsequence ( <*X, Y*>,Iv))) = ( len <*X, Y*>) by PRVECT_2:def 11

        .= 2 by FINSEQ_1: 44;

        then ( normsequence ( <*X, Y*>,Iv)) = v1 by A4, A7, A8, FINSEQ_1: 44;

        hence thesis by A4, A3, A2, PRVECT_2:def 12;

      end;

      hence thesis;

    end;

    theorem :: PRVECT_3:16

    

     Th16: for X be RealNormSpace holds ex I be Function of X, ( product <*X*>) st I is one-to-one & I is onto & (for x be Point of X holds (I . x) = <*x*>) & (for v,w be Point of X holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of X, r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & ( 0. ( product <*X*>)) = (I . ( 0. X)) & (for v be Point of X holds ||.(I . v).|| = ||.v.||)

    proof

      let X be RealNormSpace;

      reconsider X0 = X as RealLinearSpace;

      consider I0 be Function of X0, ( product <*X0*>) such that

       A1: I0 is one-to-one & I0 is onto & (for x be Point of X holds (I0 . x) = <*x*>) & (for v,w be Point of X0 holds (I0 . (v + w)) = ((I0 . v) + (I0 . w))) & (for v be Point of X0, r be Element of REAL holds (I0 . (r * v)) = (r * (I0 . v))) & ( 0. ( product <*X0*>)) = (I0 . ( 0. X0)) by Th11;

      

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

      then

      reconsider I = I0 as Function of X, ( product <*X*>);

      take I;

      thus I is one-to-one & I is onto & (for x be Point of X holds (I . x) = <*x*>) by A1, A2;

      thus for v,w be Point of X holds (I . (v + w)) = ((I . v) + (I . w))

      proof

        let v,w be Point of X;

        reconsider v0 = v, w0 = w as Point of X0;

        

        thus (I . (v + w)) = ((I0 . v0) + (I0 . w0)) by A1

        .= ((I . v) + (I . w)) by A2;

      end;

      thus for v be Point of X, r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of X, r be Element of REAL ;

        reconsider v0 = v as Point of X0;

        

        thus (I . (r * v)) = (r * (I0 . v0)) by A1

        .= (r * (I . v)) by A2;

      end;

      thus ( 0. ( product <*X*>)) = (I . ( 0. X)) by A1, A2;

      thus for v be Point of X holds ||.(I . v).|| = ||.v.||

      proof

        let v be Point of X;

        

         A3: ( len <* ||.v.||*>) = 1 by FINSEQ_1: 40;

        reconsider vv = ||.v.|| as Element of REAL ;

        reconsider v1 = <*vv*> as Element of ( REAL 1) by FINSEQ_2: 92, A3;

        reconsider v2 = ( ||.v.|| ^2 ) as Real;

        

         A4: |.v1.| = ( sqrt ( Sum <*v2*>)) by RVSUM_1: 55

        .= ( sqrt ( ||.v.|| ^2 )) by RVSUM_1: 73

        .= ||.v.|| by NORMSP_1: 4, SQUARE_1: 22;

        

         A5: (I . v) = <*v*> by A1;

        reconsider Iv = (I . v) as Element of ( product ( carr <*X*>)) by A2;

        

         A6: ( <*v*> . 1) = v by FINSEQ_1: 40;

        1 in {1} by TARSKI:def 1;

        then

        reconsider j1 = 1 as Element of ( dom <*X*>) by FINSEQ_1: 2, FINSEQ_1:def 8;

        

         A7: (( normsequence ( <*X*>,Iv)) . j1) = (the normF of ( <*X*> . j1) . (Iv . j1)) by PRVECT_2:def 11

        .= ||.v.|| by A5, A6, FINSEQ_1: 40;

        ( len ( normsequence ( <*X*>,Iv))) = ( len <*X*>) by PRVECT_2:def 11

        .= 1 by FINSEQ_1: 40;

        then ( normsequence ( <*X*>,Iv)) = v1 by A7, FINSEQ_1: 40;

        hence thesis by A4, A2, PRVECT_2:def 12;

      end;

    end;

    registration

      let G,F be non empty RealNormSpace-yielding FinSequence;

      cluster (G ^ F) -> non empty RealNormSpace-yielding;

      correctness

      proof

        for S be set st S in ( rng (G ^ F)) holds S is RealNormSpace

        proof

          let S be set;

          assume S in ( rng (G ^ F));

          then

          consider i be object such that

           A1: i in ( dom (G ^ F)) & ((G ^ F) . i) = S by FUNCT_1:def 3;

          reconsider i as Element of NAT by A1;

          per cases by A1, FINSEQ_1: 25;

            suppose

             A2: i in ( dom G);

            then (G . i) in ( rng G) by FUNCT_1: 3;

            then (G . i) is RealNormSpace by PRVECT_2:def 10;

            hence S is RealNormSpace by A1, A2, FINSEQ_1:def 7;

          end;

            suppose ex n be Nat st n in ( dom F) & i = (( len G) + n);

            then

            consider n be Nat such that

             A3: n in ( dom F) & i = (( len G) + n);

            (F . n) in ( rng F) by A3, FUNCT_1: 3;

            then (F . n) is RealNormSpace by PRVECT_2:def 10;

            hence S is RealNormSpace by A1, A3, FINSEQ_1:def 7;

          end;

        end;

        hence thesis;

      end;

    end

    

     Lm3: for F1,F2 be FinSequence of REAL holds ( sqr (F1 ^ F2)) = (( sqr F1) ^ ( sqr F2)) by RVSUM_1: 144;

    theorem :: PRVECT_3:17

    

     Th17: for X,Y be non empty RealNormSpace-Sequence holds ex I be Function of [:( product X), ( product Y):], ( product (X ^ Y)) st I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), ( product Y):] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), ( product Y):], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), ( product Y):])) = ( 0. ( product (X ^ Y))) & (for v be Point of [:( product X), ( product Y):] holds ||.(I . v).|| = ||.v.||)

    proof

      let X,Y be non empty RealNormSpace-Sequence;

      reconsider X0 = X, Y0 = Y as non empty RealLinearSpace-Sequence;

      set PX = ( product X);

      set PY = ( product Y);

      set PX0 = ( product X0);

      set PY0 = ( product Y0);

      reconsider CX = ( carr X), CY = ( carr Y) as non-empty non empty FinSequence;

      reconsider CX0 = ( carr X0), CY0 = ( carr Y0) as non-empty non empty FinSequence;

      

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

      

       A2: for g1,g2 be Point of PX, f1,f2 be Point of PY holds (( prod_ADD (PX0,PY0)) . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)]

      proof

        let g1,g2 be Point of PX, f1,f2 be Point of PY;

        reconsider g10 = g1, g20 = g2 as Point of PX0 by A1;

        reconsider f10 = f1, f20 = f2 as Point of PY0 by A1;

        (g10 + g20) = (g1 + g2) & (f10 + f20) = (f1 + f2) by A1;

        hence (( prod_ADD (PX0,PY0)) . ( [g1, f1], [g2, f2])) = [(g1 + g2), (f1 + f2)] by Def1;

      end;

      

       A3: for r be Real, g be Point of PX, f be Point of PY holds (( prod_MLT (PX0,PY0)) . (r, [g, f])) = [(r * g), (r * f)]

      proof

        let r be Real, g be Point of PX, f be Point of PY;

        reconsider g0 = g as Point of PX0 by A1;

        reconsider f0 = f as Point of PY0 by A1;

        (r * g0) = (r * g) & (r * f0) = (r * f) by A1;

        hence (( prod_MLT (PX0,PY0)) . (r, [g, f])) = [(r * g), (r * f)] by Def2;

      end;

      

       A4: ( len ( carr (X ^ Y))) = ( len (X ^ Y)) & ( len ( carr (X0 ^ Y0))) = ( len (X0 ^ Y0)) & ( len CX) = ( len X) & ( len CY) = ( len Y) & ( len CX0) = ( len X0) & ( len CY0) = ( len Y0) by PRVECT_1:def 11;

      consider I0 be Function of [:PX0, PY0:], ( product (X0 ^ Y0)) such that

       A5: I0 is one-to-one & I0 is onto & (for x be Point of PX0, y be Point of PY0 holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I0 . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:PX0, PY0:] holds (I0 . (v + w)) = ((I0 . v) + (I0 . w))) & (for v be Point of [:PX0, PY0:], r be Element of REAL holds (I0 . (r * v)) = (r * (I0 . v))) & ( 0. ( product (X0 ^ Y0))) = (I0 . ( 0. [:PX0, PY0:])) by Th13;

      

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

      then

      reconsider I = I0 as Function of [:PX, PY:], ( product (X ^ Y)) by A1;

      take I;

      thus I is one-to-one & I is onto by A5, A6;

      thus for x be Point of PX, y be Point of PY holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1) by A1, A5;

      

       A7: for x,y be FinSequence st x in the carrier of ( product X) & y in the carrier of ( product Y) holds (I . (x,y)) = (x ^ y)

      proof

        let x,y be FinSequence;

        assume x in the carrier of ( product X) & y in the carrier of ( product Y);

        then ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1) by A1, A5;

        hence thesis;

      end;

      thus for v,w be Point of [:PX, PY:] holds (I . (v + w)) = ((I . v) + (I . w))

      proof

        let v,w be Point of [:PX, PY:];

        reconsider v0 = v, w0 = w as Point of [:PX0, PY0:] by A1;

        (v + w) = (v0 + w0) by A2, A1, Def1;

        then (I . (v + w)) = ((I0 . v0) + (I0 . w0)) by A5;

        hence (I . (v + w)) = ((I . v) + (I . w)) by A6;

      end;

      thus for v be Point of [:PX, PY:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of [:PX, PY:], r be Element of REAL ;

        reconsider v0 = v as Point of [:PX0, PY0:] by A1;

        (r * v) = (r * v0) by A3, A1, Def2;

        then (I . (r * v)) = (r * (I0 . v0)) by A5;

        hence (I . (r * v)) = (r * (I . v)) by A6;

      end;

      thus ( 0. ( product (X ^ Y))) = (I . ( 0. [:PX, PY:])) by A1, A5, A6;

      for v be Point of [:PX, PY:] holds ||.(I . v).|| = ||.v.||

      proof

        let v be Point of [:PX, PY:];

        consider x1 be Point of PX, y1 be Point of PY such that

         A8: v = [x1, y1] by Lm1;

        consider v1 be Element of ( REAL 2) such that

         A9: v1 = <* ||.x1.||, ||.y1.||*> & (( prod_NORM (PX,PY)) . (x1,y1)) = |.v1.| by Def6;

        reconsider Ix1 = x1, Iy1 = y1 as FinSequence by A1, Lm2;

        

         A10: ( dom Ix1) = ( dom ( carr X)) & ( dom Iy1) = ( dom ( carr Y)) by A1, CARD_3: 9;

        

         A11: (I . v) = (I . (x1,y1)) by A8

        .= (Ix1 ^ Iy1) by A7;

        reconsider Iv = (I . v) as Element of ( product ( carr (X ^ Y))) by A6;

        reconsider Ix = x1 as Element of ( product ( carr X)) by A1;

        reconsider Iy = y1 as Element of ( product ( carr Y)) by A1;

        

         A12: ||.(I . v).|| = |.( normsequence ((X ^ Y),Iv)).| by A6, PRVECT_2:def 12

        .= ( sqrt ( Sum ( sqr ( normsequence ((X ^ Y),Iv)))));

        

         A13: ( len ( normsequence ((X ^ Y),Iv))) = ( len (X ^ Y)) & ( len ( normsequence (X,Ix))) = ( len X) & ( len ( normsequence (Y,Iy))) = ( len Y) by PRVECT_2:def 11;

        reconsider x12 = ( ||.x1.|| ^2 ), y12 = ( ||.y1.|| ^2 ) as Real;

        

         A14: |.v1.| = ( sqrt ( Sum <*x12, y12*>)) by A9, TOPREAL6: 11

        .= ( sqrt (( ||.x1.|| ^2 ) + ( ||.y1.|| ^2 ))) by RVSUM_1: 77;

        

         A15: 0 <= ( Sum ( sqr ( normsequence (X,Ix)))) & 0 <= ( Sum ( sqr ( normsequence (Y,Iy)))) by RVSUM_1: 86;

        ( ||.x1.|| ^2 ) = ( |.( normsequence (X,Ix)).| ^2 ) & ( ||.y1.|| ^2 ) = ( |.( normsequence (Y,Iy)).| ^2 ) by A1, PRVECT_2:def 12;

        then

         A16: ( ||.x1.|| ^2 ) = ( Sum ( sqr ( normsequence (X,Ix)))) & ( ||.y1.|| ^2 ) = ( Sum ( sqr ( normsequence (Y,Iy)))) by A15, SQUARE_1:def 2;

        ( len ( normsequence ((X ^ Y),Iv))) = (( len ( normsequence (X,Ix))) + ( len ( normsequence (Y,Iy)))) by A13, FINSEQ_1: 22

        .= ( len (( normsequence (X,Ix)) ^ ( normsequence (Y,Iy)))) by FINSEQ_1: 22;

        then

         A17: ( dom ( normsequence ((X ^ Y),Iv))) = ( dom (( normsequence (X,Ix)) ^ ( normsequence (Y,Iy)))) by FINSEQ_3: 29;

        for k be Nat st k in ( dom ( normsequence ((X ^ Y),Iv))) holds (( normsequence ((X ^ Y),Iv)) . k) = ((( normsequence (X,Ix)) ^ ( normsequence (Y,Iy))) . k)

        proof

          let k be Nat;

          assume k in ( dom ( normsequence ((X ^ Y),Iv)));

          then

           A18: k in ( Seg ( len ( normsequence ((X ^ Y),Iv)))) by FINSEQ_1:def 3;

          then

           A19: k in ( dom (X ^ Y)) by A13, FINSEQ_1:def 3;

          reconsider k1 = k as Element of ( dom (X ^ Y)) by A18, A13, FINSEQ_1:def 3;

          

           A20: (( normsequence ((X ^ Y),Iv)) . k) = (the normF of ((X ^ Y) . k1) . (Iv . k1)) by PRVECT_2:def 11;

          

           A21: ( dom Ix1) = ( Seg ( len ( carr X))) & ( dom Iy1) = ( Seg ( len ( carr Y))) by A10, FINSEQ_1:def 3;

          then

           A22: ( dom Ix1) = ( dom X) & ( dom Iy1) = ( dom Y) by A4, FINSEQ_1:def 3;

          per cases by A19, FINSEQ_1: 25;

            suppose

             A23: k in ( dom X);

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

            then

             A24: k in ( dom ( normsequence (X,Ix))) by A23, FINSEQ_3: 29;

            reconsider k2 = k1 as Element of ( dom X) by A23;

            

             A25: (Iv . k) = (Ix1 . k) by A23, A22, A11, FINSEQ_1:def 7;

            

            thus (( normsequence ((X ^ Y),Iv)) . k) = (the normF of (X . k2) . (Iv . k2)) by A20, FINSEQ_1:def 7

            .= (( normsequence (X,Ix)) . k2) by A25, PRVECT_2:def 11

            .= ((( normsequence (X,Ix)) ^ ( normsequence (Y,Iy))) . k) by A24, FINSEQ_1:def 7;

          end;

            suppose ex n be Nat st n in ( dom Y) & k = (( len X) + n);

            then

            consider n be Nat such that

             A26: n in ( dom Y) & k = (( len X) + n);

            ( len Y) = ( len ( normsequence (Y,Iy))) by PRVECT_2:def 11;

            then

             A27: n in ( dom ( normsequence (Y,Iy))) by A26, FINSEQ_3: 29;

            reconsider n1 = n as Element of ( dom Y) by A26;

            ( len Ix1) = ( len X) by A21, A4, FINSEQ_1:def 3;

            then

             A28: (Iv . k) = (Iy1 . n) by A11, A26, A22, FINSEQ_1:def 7;

            

            thus (( normsequence ((X ^ Y),Iv)) . k) = (the normF of (Y . n1) . (Iv . k1)) by A20, A26, FINSEQ_1:def 7

            .= (( normsequence (Y,Iy)) . n1) by A28, PRVECT_2:def 11

            .= ((( normsequence (X,Ix)) ^ ( normsequence (Y,Iy))) . k) by A27, A26, A13, FINSEQ_1:def 7;

          end;

        end;

        then ( normsequence ((X ^ Y),Iv)) = (( normsequence (X,Ix)) ^ ( normsequence (Y,Iy))) by A17, FINSEQ_1: 13;

        then ( sqr ( normsequence ((X ^ Y),Iv))) = (( sqr ( normsequence (X,Ix))) ^ ( sqr ( normsequence (Y,Iy)))) by Lm3;

        hence thesis by A14, A12, A16, A9, A8, RVSUM_1: 75;

      end;

      hence thesis;

    end;

    theorem :: PRVECT_3:18

    

     Th18: for G,F be RealNormSpace holds (for x be set holds (x is Point of [:G, F:] iff ex x1 be Point of G, x2 be Point of F st x = [x1, x2])) & (for x,y be Point of [:G, F:], x1,y1 be Point of G, x2,y2 be Point of F st x = [x1, x2] & y = [y1, y2] holds (x + y) = [(x1 + y1), (x2 + y2)]) & ( 0. [:G, F:]) = [( 0. G), ( 0. F)] & (for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ( - x) = [( - x1), ( - x2)]) & (for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F, a be Real st x = [x1, x2] holds (a * x) = [(a * x1), (a * x2)]) & (for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & ||.x.|| = |.w.|)

    proof

      let G,F be RealNormSpace;

      thus for x be set holds (x is Point of [:G, F:] iff ex x1 be Point of G, x2 be Point of F st x = [x1, x2]) by Lm1;

      thus for x,y be Point of [:G, F:], x1,y1 be Point of G, x2,y2 be Point of F st x = [x1, x2] & y = [y1, y2] holds (x + y) = [(x1 + y1), (x2 + y2)] by Def1;

      thus ( 0. [:G, F:]) = [( 0. G), ( 0. F)];

      thus for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ( - x) = [( - x1), ( - x2)]

      proof

        let x be Point of [:G, F:];

        let x1 be Point of G, x2 be Point of F;

        assume

         A1: x = [x1, x2];

        reconsider y = [( - x1), ( - x2)] as Point of [:G, F:];

        (x + y) = [(x1 + ( - x1)), (x2 + ( - x2))] by A1, Def1

        .= [( 0. G), (x2 + ( - x2))] by RLVECT_1:def 10

        .= ( 0. [:G, F:]) by RLVECT_1:def 10;

        hence thesis by RLVECT_1:def 10;

      end;

      thus for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F, a be Real st x = [x1, x2] holds (a * x) = [(a * x1), (a * x2)] by Def2;

      thus for x be Point of [:G, F:], x1 be Point of G, x2 be Point of F st x = [x1, x2] holds ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & ||.x.|| = |.w.|

      proof

        let x be Point of [:G, F:], x1 be Point of G, x2 be Point of F;

        assume

         A2: x = [x1, x2];

        ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & (( prod_NORM (G,F)) . (x1,x2)) = |.w.| by Def6;

        hence thesis by A2;

      end;

    end;

    theorem :: PRVECT_3:19

    

     Th19: for G,F be RealNormSpace holds (for x be set holds (x is Point of ( product <*G, F*>) iff ex x1 be Point of G, x2 be Point of F st x = <*x1, x2*>)) & (for x,y be Point of ( product <*G, F*>), x1,y1 be Point of G, x2,y2 be Point of F st x = <*x1, x2*> & y = <*y1, y2*> holds (x + y) = <*(x1 + y1), (x2 + y2)*>) & ( 0. ( product <*G, F*>)) = <*( 0. G), ( 0. F)*> & (for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>) & (for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F, a be Real st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>) & (for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & ||.x.|| = |.w.|)

    proof

      let G,F be RealNormSpace;

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

       A1: I is one-to-one & I is onto & (for x be Point of G, y be Point of F holds (I . (x,y)) = <*x, y*>) & (for v,w be Point of [:G, F:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:G, F:], r be Real holds (I . (r * v)) = (r * (I . v))) & ( 0. ( product <*G, F*>)) = (I . ( 0. [:G, F:])) & (for v be Point of [:G, F:] holds ||.(I . v).|| = ||.v.||) by Th15;

      thus

       A2: for x be set holds (x is Point of ( product <*G, F*>) iff ex x1 be Point of G, x2 be Point of F st x = <*x1, x2*>)

      proof

        let y be set;

        hereby

          assume y is Point of ( product <*G, F*>);

          then y in the carrier of ( product <*G, F*>);

          then y in ( rng I) by A1, FUNCT_2:def 3;

          then

          consider x be Element of the carrier of [:G, F:] such that

           A3: y = (I . x) by FUNCT_2: 113;

          consider x1 be Point of G, x2 be Point of F such that

           A4: x = [x1, x2] by Lm1;

          take x1, x2;

          (I . (x1,x2)) = <*x1, x2*> by A1;

          hence y = <*x1, x2*> by A3, A4;

        end;

        hereby

          assume ex x1 be Point of G, x2 be Point of F st y = <*x1, x2*>;

          then

          consider x1 be Point of G, x2 be Point of F such that

           A5: y = <*x1, x2*>;

          

           A6: (I . [x1, x2]) in ( rng I) by FUNCT_2: 112;

          (I . (x1,x2)) = <*x1, x2*> by A1;

          hence y is Point of ( product <*G, F*>) by A5, A6;

        end;

      end;

      thus

       A7: for x,y be Point of ( product <*G, F*>), x1,y1 be Point of G, x2,y2 be Point of F st x = <*x1, x2*> & y = <*y1, y2*> holds (x + y) = <*(x1 + y1), (x2 + y2)*>

      proof

        let x,y be Point of ( product <*G, F*>);

        let x1,y1 be Point of G, x2,y2 be Point of F;

        assume

         A8: x = <*x1, x2*> & y = <*y1, y2*>;

        reconsider z = [x1, x2], w = [y1, y2] as Point of [:G, F:];

        

         A9: (z + w) = [(x1 + y1), (x2 + y2)] by Def1;

        

         A10: (I . ((x1 + y1),(x2 + y2))) = <*(x1 + y1), (x2 + y2)*> by A1;

        (I . (x1,x2)) = <*x1, x2*> & (I . (y1,y2)) = <*y1, y2*> by A1;

        hence <*(x1 + y1), (x2 + y2)*> = (x + y) by A1, A9, A10, A8;

      end;

      thus

       A11: ( 0. ( product <*G, F*>)) = <*( 0. G), ( 0. F)*>

      proof

        (I . (( 0. G),( 0. F))) = <*( 0. G), ( 0. F)*> by A1;

        hence thesis by A1;

      end;

      thus for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>

      proof

        let x be Point of ( product <*G, F*>);

        let x1 be Point of G, x2 be Point of F;

        assume

         A12: x = <*x1, x2*>;

        reconsider y = <*( - x1), ( - x2)*> as Point of ( product <*G, F*>) by A2;

        (x + y) = <*(x1 + ( - x1)), (x2 + ( - x2))*> by A7, A12

        .= <*( 0. G), (x2 + ( - x2))*> by RLVECT_1:def 10

        .= ( 0. ( product <*G, F*>)) by A11, RLVECT_1:def 10;

        hence thesis by RLVECT_1:def 10;

      end;

      thus for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F, a be Real st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>

      proof

        let x be Point of ( product <*G, F*>);

        let x1 be Point of G, x2 be Point of F, a be Real;

        assume

         A13: x = <*x1, x2*>;

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

        reconsider y = [x1, x2] as Point of [:G, F:];

        

         A14: <*x1, x2*> = (I . (x1,x2)) by A1;

        (I . (a * y)) = (I . ((a0 * x1),(a0 * x2))) by Th18

        .= <*(a0 * x1), (a0 * x2)*> by A1;

        hence thesis by A13, A14, A1;

      end;

      thus for x be Point of ( product <*G, F*>), x1 be Point of G, x2 be Point of F st x = <*x1, x2*> holds ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & ||.x.|| = |.w.|

      proof

        let x be Point of ( product <*G, F*>);

        let x1 be Point of G, x2 be Point of F;

        assume

         A15: x = <*x1, x2*>;

        reconsider y = [x1, x2] as Point of [:G, F:];

        consider w be Element of ( REAL 2) such that

         A16: w = <* ||.x1.||, ||.x2.||*> & ||.y.|| = |.w.| by Th18;

        take w;

        

         A17: (I . y) = (I . (x1,x2))

        .= x by A1, A15;

        thus w = <* ||.x1.||, ||.x2.||*> by A16;

        thus ||.x.|| = |.w.| by A1, A16, A17;

      end;

    end;

    registration

      let X,Y be complete RealNormSpace;

      cluster [:X, Y:] -> complete;

      coherence

      proof

        

         A1: ( dom <*X, Y*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89;

        now

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

          i = 1 or i = 2 by A1, TARSKI:def 2;

          hence ( <*X, Y*> . i) is complete by FINSEQ_1: 44;

        end;

        then

         A2: ( product <*X, Y*>) is complete by PRVECT_2: 14;

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

         A3: I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = <*x, y*>) & (for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:X, Y:], r be Real holds (I . (r * v)) = (r * (I . v))) & ( 0. ( product <*X, Y*>)) = (I . ( 0. [:X, Y:])) & (for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.||) by Th15;

         A4:

        now

          let v,w be Point of [:X, Y:];

          

          thus (I . (v - w)) = (I . (v + (( - 1) * w))) by RLVECT_1: 16

          .= ((I . v) + (I . (( - 1) * w))) by A3

          .= ((I . v) + (( - 1) * (I . w))) by A3

          .= ((I . v) - (I . w)) by RLVECT_1: 16;

        end;

         A5:

        now

          let v,w be Point of [:X, Y:];

          

          thus ||.((I . v) - (I . w)).|| = ||.(I . (v - w)).|| by A4

          .= ||.(v - w).|| by A3;

        end;

        now

          let seq be sequence of [:X, Y:];

          assume

           A6: seq is Cauchy_sequence_by_Norm;

          reconsider Iseq = (I * seq) as sequence of ( product <*X, Y*>);

          now

            let r be Real;

            assume r > 0 ;

            then

            consider k be Nat such that

             A7: for n,m be Nat st n >= k & m >= k holds ||.((seq . n) - (seq . m)).|| < r by A6, RSSPACE3: 8;

            take k;

            let n,m be Nat;

            

             A8: n in NAT & m in NAT by ORDINAL1:def 12;

            assume n >= k & m >= k;

            then

             A9: ||.((seq . n) - (seq . m)).|| < r by A7;

             NAT = ( dom seq) by FUNCT_2:def 1;

            then (Iseq . n) = (I . (seq . n)) & (Iseq . m) = (I . (seq . m)) by FUNCT_1: 13, A8;

            hence ||.((Iseq . n) - (Iseq . m)).|| < r by A9, A5;

          end;

          then Iseq is Cauchy_sequence_by_Norm by RSSPACE3: 8;

          then

           A10: Iseq is convergent by A2, LOPBAN_1:def 15;

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

          then ( dom (I " )) = the carrier of ( product <*X, Y*>) & ( rng (I " )) = the carrier of [:X, Y:] by A3, FUNCT_2:def 1, FUNCT_2:def 3;

          then

          reconsider Lseq = ((I " ) . ( lim Iseq)) as Point of [:X, Y:] by FUNCT_1: 3;

          ( rng I) = the carrier of ( product <*X, Y*>) by A3, FUNCT_2:def 3;

          then

           A11: (I . Lseq) = ( lim Iseq) by A3, FUNCT_1: 35;

          now

            let r be Real;

            assume 0 < r;

            then

            consider m be Nat such that

             A12: for n be Nat st m <= n holds ||.((Iseq . n) - ( lim Iseq)).|| < r by A10, NORMSP_1:def 7;

            take m;

            let n be Nat;

            

             A13: n in NAT by ORDINAL1:def 12;

            assume m <= n;

            then

             A14: ||.((Iseq . n) - ( lim Iseq)).|| < r by A12;

             NAT = ( dom seq) by FUNCT_2:def 1;

            then (Iseq . n) = (I . (seq . n)) by FUNCT_1: 13, A13;

            hence ||.((seq . n) - Lseq).|| < r by A11, A5, A14;

          end;

          hence seq is convergent by NORMSP_1:def 6;

        end;

        hence thesis by LOPBAN_1:def 15;

      end;

    end

    theorem :: PRVECT_3:20

    for X,Y be non empty RealNormSpace-Sequence holds ex I be Function of ( product <*( product X), ( product Y)*>), ( product (X ^ Y)) st I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . <*x, y*>) = (x1 ^ y1)) & (for v,w be Point of ( product <*( product X), ( product Y)*>) holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of ( product <*( product X), ( product Y)*>), r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. ( product <*( product X), ( product Y)*>))) = ( 0. ( product (X ^ Y))) & (for v be Point of ( product <*( product X), ( product Y)*>) holds ||.(I . v).|| = ||.v.||)

    proof

      let X,Y be non empty RealNormSpace-Sequence;

      set PX = ( product X);

      set PY = ( product Y);

      set PXY = ( product (X ^ Y));

      consider K be Function of [:PX, PY:], PXY such that

       A1: K is one-to-one & K is onto & (for x be Point of PX, y be Point of PY holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (K . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:PX, PY:] holds (K . (v + w)) = ((K . v) + (K . w))) & (for v be Point of [:PX, PY:], r be Element of REAL holds (K . (r * v)) = (r * (K . v))) & (K . ( 0. [:PX, PY:])) = ( 0. PXY) & (for v be Point of [:PX, PY:] holds ||.(K . v).|| = ||.v.||) by Th17;

      consider J be Function of [:PX, PY:], ( product <*PX, PY*>) such that

       A2: J is one-to-one & J is onto & (for x be Point of PX, y be Point of PY holds (J . (x,y)) = <*x, y*>) & (for v,w be Point of [:PX, PY:] holds (J . (v + w)) = ((J . v) + (J . w))) & (for v be Point of [:PX, PY:], r be Real holds (J . (r * v)) = (r * (J . v))) & ( 0. ( product <*PX, PY*>)) = (J . ( 0. [:PX, PY:])) & (for v be Point of [:PX, PY:] holds ||.(J . v).|| = ||.v.||) by Th15;

      

       A3: ( rng J) = the carrier of ( product <*PX, PY*>) by A2, FUNCT_2:def 3;

      then

      reconsider JB = (J " ) as Function of the carrier of ( product <*PX, PY*>), the carrier of [:PX, PY:] by A2, FUNCT_2: 25;

      

       A4: ( dom (J " )) = ( rng J) & ( rng (J " )) = ( dom J) by A2, FUNCT_1: 33;

      then

       A5: ( dom (J " )) = the carrier of ( product <*PX, PY*>) by A2, FUNCT_2:def 3;

      

       A6: ( rng (J " )) = the carrier of [:PX, PY:] by A4, FUNCT_2:def 1;

      reconsider I = (K * JB) as Function of ( product <*PX, PY*>), PXY;

      take I;

      thus I is one-to-one by A1, A2;

      ( rng K) = the carrier of PXY by A1, FUNCT_2:def 3;

      then ( rng I) = the carrier of PXY by A6, FUNCT_2: 14;

      hence I is onto by FUNCT_2:def 3;

      thus for x be Point of PX, y be Point of PY holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . <*x, y*>) = (x1 ^ y1)

      proof

        let x be Point of PX, y be Point of PY;

        consider x1,y1 be FinSequence such that

         A7: x = x1 & y = y1 & (K . (x,y)) = (x1 ^ y1) by A1;

        

         A8: (J . (x,y)) = <*x, y*> by A2;

         [x, y] in the carrier of [:PX, PY:];

        then

         A9: [x, y] in ( dom J) by FUNCT_2:def 1;

         <*x, y*> is Point of ( product <*PX, PY*>) by Th19;

        then (I . <*x, y*>) = (K . (JB . (J . [x, y]))) by A8, A5, FUNCT_1: 13;

        then (I . <*x, y*>) = (x1 ^ y1) by A7, A9, A2, FUNCT_1: 34;

        hence thesis by A7;

      end;

      thus for v,w be Point of ( product <*PX, PY*>) holds (I . (v + w)) = ((I . v) + (I . w))

      proof

        let v,w be Point of ( product <*PX, PY*>);

        consider x be Element of the carrier of [:PX, PY:] such that

         A10: v = (J . x) by A3, FUNCT_2: 113;

        consider y be Element of the carrier of [:PX, PY:] such that

         A11: w = (J . y) by A3, FUNCT_2: 113;

        x in the carrier of [:PX, PY:] & y in the carrier of [:PX, PY:] & (x + y) in the carrier of [:PX, PY:];

        then x in ( dom J) & y in ( dom J) & (x + y) in ( dom J) by FUNCT_2:def 1;

        then

         A12: (JB . v) = x & (JB . w) = y & (JB . (J . (x + y))) = (x + y) by A10, A11, A2, FUNCT_1: 34;

        v in ( rng J) & w in ( rng J) by A3;

        then

         A13: v in ( dom JB) & w in ( dom JB) by A2, FUNCT_1: 33;

        (v + w) = (J . (x + y)) by A10, A11, A2;

        

        then (I . (v + w)) = (K . (x + y)) by A12, A5, FUNCT_1: 13

        .= ((K . x) + (K . y)) by A1

        .= (((K * JB) . v) + (K . (JB . w))) by A12, A13, FUNCT_1: 13;

        hence (I . (v + w)) = ((I . v) + (I . w)) by A13, FUNCT_1: 13;

      end;

      thus for v be Point of ( product <*PX, PY*>), r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of ( product <*PX, PY*>), r be Element of REAL ;

        consider x be Element of the carrier of [:PX, PY:] such that

         A14: v = (J . x) by A3, FUNCT_2: 113;

        x in the carrier of [:PX, PY:];

        then x in ( dom J) by FUNCT_2:def 1;

        then

         A15: (JB . v) = x by A14, A2, FUNCT_1: 34;

        v in ( rng J) by A3;

        then

         A16: v in ( dom JB) by A2, FUNCT_1: 33;

        (r * x) in the carrier of [:PX, PY:];

        then

         A17: (r * x) in ( dom J) by FUNCT_2:def 1;

        (r * v) = (J . (r * x)) by A14, A2;

        then (I . (r * v)) = (K . (JB . (J . (r * x)))) by A5, FUNCT_1: 13;

        

        hence (I . (r * v)) = (K . (r * x)) by A17, A2, FUNCT_1: 34

        .= (r * (K . x)) by A1

        .= (r * (I . v)) by A15, A16, FUNCT_1: 13;

      end;

      thus (I . ( 0. ( product <*PX, PY*>))) = ( 0. ( product (X ^ Y)))

      proof

        ( 0. [:PX, PY:]) in the carrier of [:PX, PY:];

        then

         A18: ( 0. [:PX, PY:]) in ( dom J) by FUNCT_2:def 1;

        ( 0. ( product <*PX, PY*>)) in ( rng J) by A3;

        then ( 0. ( product <*PX, PY*>)) in ( dom JB) by A2, FUNCT_1: 33;

        then (I . ( 0. ( product <*PX, PY*>))) = (K . (JB . (J . ( 0. [:PX, PY:])))) by A2, FUNCT_1: 13;

        hence (I . ( 0. ( product <*PX, PY*>))) = ( 0. PXY) by A1, A18, A2, FUNCT_1: 34;

      end;

      thus for v be Point of ( product <*PX, PY*>) holds ||.(I . v).|| = ||.v.||

      proof

        let v be Point of ( product <*PX, PY*>);

        consider x be Element of the carrier of [:PX, PY:] such that

         A19: v = (J . x) by A3, FUNCT_2: 113;

        x in the carrier of [:PX, PY:];

        then

         A20: x in ( dom J) by FUNCT_2:def 1;

        v in ( rng J) by A3;

        then v in ( dom JB) by A2, FUNCT_1: 33;

        

        then (I . v) = (K . (JB . (J . x))) by A19, FUNCT_1: 13

        .= (K . x) by A20, A2, FUNCT_1: 34;

        then ||.(I . v).|| = ||.x.|| by A1;

        hence ||.(I . v).|| = ||.v.|| by A2, A19;

      end;

    end;

    theorem :: PRVECT_3:21

    

     Th21: for X,Y be non empty RealLinearSpace holds ex I be Function of [:X, Y:], [:X, ( product <*Y*>):] st I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = [x, <*y*>]) & (for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:X, Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:X, Y:])) = ( 0. [:X, ( product <*Y*>):])

    proof

      let X,Y be non empty RealLinearSpace;

      consider J be Function of Y, ( product <*Y*>) such that

       A1: J is one-to-one & J is onto & (for y be Point of Y holds (J . y) = <*y*>) & (for v,w be Point of Y holds (J . (v + w)) = ((J . v) + (J . w))) & (for v be Point of Y, r be Element of REAL holds (J . (r * v)) = (r * (J . v))) & (J . ( 0. Y)) = ( 0. ( product <*Y*>)) by Th11;

      defpred P[ object, object, object] means $3 = [$1, <*$2*>];

      

       A2: for x,y be object st x in the carrier of X & y in the carrier of Y holds ex z be object st z in the carrier of [:X, ( product <*Y*>):] & P[x, y, z]

      proof

        let x,y be object;

        assume

         A3: x in the carrier of X & y in the carrier of Y;

        then

        reconsider y0 = y as Point of Y;

        (J . y0) = <*y0*> by A1;

        then [x, <*y*>] in [:the carrier of X, the carrier of ( product <*Y*>):] by A3, ZFMISC_1: 87;

        hence thesis;

      end;

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

       A4: for x,y be object st x in the carrier of X & y in the carrier of Y holds P[x, y, (I . (x,y))] from BINOP_1:sch 1( A2);

      reconsider I as Function of [:X, Y:], [:X, ( product <*Y*>):];

      take I;

      now

        let z1,z2 be object;

        assume

         A5: z1 in the carrier of [:X, Y:] & z2 in the carrier of [:X, Y:] & (I . z1) = (I . z2);

        consider x1,y1 be object such that

         A6: x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1, y1] by A5, ZFMISC_1:def 2;

        consider x2,y2 be object such that

         A7: x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2, y2] by A5, ZFMISC_1:def 2;

         [x1, <*y1*>] = (I . (x1,y1)) by A4, A6

        .= (I . (x2,y2)) by A5, A6, A7

        .= [x2, <*y2*>] by A4, A7;

        then x1 = x2 & <*y1*> = <*y2*> by XTUPLE_0: 1;

        hence z1 = z2 by A6, A7, FINSEQ_1: 76;

      end;

      hence I is one-to-one by FUNCT_2: 19;

      now

        let w be object;

        assume w in the carrier of [:X, ( product <*Y*>):];

        then

        consider x,y1 be object such that

         A8: x in the carrier of X & y1 in the carrier of ( product <*Y*>) & w = [x, y1] by ZFMISC_1:def 2;

        y1 in ( rng J) by A1, A8, FUNCT_2:def 3;

        then

        consider y be object such that

         A9: y in the carrier of Y & y1 = (J . y) by FUNCT_2: 11;

        reconsider z = [x, y] as Element of [:the carrier of X, the carrier of Y:] by A8, A9, ZFMISC_1: 87;

        (J . y) = <*y*> by A9, A1;

        then w = (I . (x,y)) by A4, A8, A9;

        then w = (I . z);

        hence w in ( rng I) by FUNCT_2: 4;

      end;

      then the carrier of [:X, ( product <*Y*>):] c= ( rng I) by TARSKI:def 3;

      then the carrier of [:X, ( product <*Y*>):] = ( rng I) by XBOOLE_0:def 10;

      hence I is onto by FUNCT_2:def 3;

      thus for x be Point of X, y be Point of Y holds (I . (x,y)) = [x, <*y*>] by A4;

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

      proof

        let v,w be Point of [:X, Y:];

        consider x1 be Point of X, x2 be Point of Y such that

         A10: v = [x1, x2] by Lm1;

        consider y1 be Point of X, y2 be Point of Y such that

         A11: w = [y1, y2] by Lm1;

        

         A12: (I . (v + w)) = (I . ((x1 + y1),(x2 + y2))) by A10, A11, Def1

        .= [(x1 + y1), <*(x2 + y2)*>] by A4;

        (I . v) = (I . (x1,x2)) & (I . w) = (I . (y1,y2)) by A10, A11;

        then

         A13: (I . v) = [x1, <*x2*>] & (I . w) = [y1, <*y2*>] by A4;

        

         A14: (J . x2) = <*x2*> & (J . y2) = <*y2*> by A1;

        then

        reconsider xx2 = <*x2*> as Point of ( product <*Y*>);

        reconsider yy2 = <*y2*> as Point of ( product <*Y*>) by A14;

         <*(x2 + y2)*> = (J . (x2 + y2)) by A1

        .= (xx2 + yy2) by A14, A1;

        hence ((I . v) + (I . w)) = (I . (v + w)) by A12, A13, Def1;

      end;

      thus for v be Point of [:X, Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of [:X, Y:], r be Element of REAL ;

        consider x1 be Point of X, x2 be Point of Y such that

         A15: v = [x1, x2] by Lm1;

        

         A16: (I . (r * v)) = (I . ((r * x1),(r * x2))) by A15, Th9

        .= [(r * x1), <*(r * x2)*>] by A4;

        

         A17: (I . v) = (I . (x1,x2)) by A15

        .= [x1, <*x2*>] by A4;

        

         A18: (J . x2) = <*x2*> by A1;

        then

        reconsider xx2 = <*x2*> as Point of ( product <*Y*>);

         <*(r * x2)*> = (J . (r * x2)) by A1

        .= (r * xx2) by A18, A1;

        hence (r * (I . v)) = (I . (r * v)) by A16, A17, Th9;

      end;

      

       A19: <*( 0. Y)*> = ( 0. ( product <*Y*>)) by A1;

      (I . ( 0. [:X, Y:])) = (I . (( 0. X),( 0. Y)));

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

    end;

    theorem :: PRVECT_3:22

    for X be non empty RealLinearSpace-Sequence, Y be RealLinearSpace holds ex I be Function of [:( product X), Y:], ( product (X ^ <*Y*>)) st I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of Y holds ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & (I . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), Y:])) = ( 0. ( product (X ^ <*Y*>)))

    proof

      let X be non empty RealLinearSpace-Sequence;

      let Y be non empty RealLinearSpace;

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

       A1: I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of Y holds (I . (x,y)) = [x, <*y*>]) & (for v,w be Point of [:( product X), Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), Y:])) = ( 0. [:( product X), ( product <*Y*>):]) by Th21;

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

       A2: J is one-to-one & J is onto & (for x be Point of ( product X), y be Point of ( product <*Y*>) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (J . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), ( product <*Y*>):] holds (J . (v + w)) = ((J . v) + (J . w))) & (for v be Point of [:( product X), ( product <*Y*>):], r be Element of REAL holds (J . (r * v)) = (r * (J . v))) & (J . ( 0. [:( product X), ( product <*Y*>):])) = ( 0. ( product (X ^ <*Y*>))) by Th13;

      set K = (J * I);

      reconsider K as Function of [:( product X), Y:], ( product (X ^ <*Y*>));

      take K;

      thus K is one-to-one by A1, A2;

      

       A3: ( rng J) = the carrier of ( product (X ^ <*Y*>)) by A2, FUNCT_2:def 3;

      ( rng I) = the carrier of [:( product X), ( product <*Y*>):] by A1, FUNCT_2:def 3;

      

      then ( rng (J * I)) = (J .: the carrier of [:( product X), ( product <*Y*>):]) by RELAT_1: 127

      .= the carrier of ( product (X ^ <*Y*>)) by A3, RELSET_1: 22;

      hence K is onto by FUNCT_2:def 3;

      thus for x be Point of ( product X), y be Point of Y holds ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & (K . (x,y)) = (x1 ^ y1)

      proof

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

        

         A4: (I . (x,y)) = [x, <*y*>] by A1;

         [x, y] in the carrier of [:( product X), Y:];

        then [x, <*y*>] in the carrier of [:( product X), ( product <*Y*>):] by A4, FUNCT_2: 5;

        then

        reconsider yy = <*y*> as Point of ( product <*Y*>) by ZFMISC_1: 87;

        consider x1,y1 be FinSequence such that

         A5: x = x1 & yy = y1 & (J . (x,yy)) = (x1 ^ y1) by A2;

        (J . (x,yy)) = (J . (I . [x, y])) by A4

        .= (K . (x,y)) by FUNCT_2: 15;

        hence thesis by A5;

      end;

      thus for v,w be Point of [:( product X), Y:] holds (K . (v + w)) = ((K . v) + (K . w))

      proof

        let v,w be Point of [:( product X), Y:];

        

        thus (K . (v + w)) = (J . (I . (v + w))) by FUNCT_2: 15

        .= (J . ((I . v) + (I . w))) by A1

        .= ((J . (I . v)) + (J . (I . w))) by A2

        .= ((K . v) + (J . (I . w))) by FUNCT_2: 15

        .= ((K . v) + (K . w)) by FUNCT_2: 15;

      end;

      thus for v be Point of [:( product X), Y:], r be Element of REAL holds (K . (r * v)) = (r * (K . v))

      proof

        let v be Point of [:( product X), Y:], r be Element of REAL ;

        

        thus (K . (r * v)) = (J . (I . (r * v))) by FUNCT_2: 15

        .= (J . (r * (I . v))) by A1

        .= (r * (J . (I . v))) by A2

        .= (r * (K . v)) by FUNCT_2: 15;

      end;

      thus (K . ( 0. [:( product X), Y:])) = ( 0. ( product (X ^ <*Y*>))) by A1, A2, FUNCT_2: 15;

    end;

    theorem :: PRVECT_3:23

    

     Th23: for X,Y be non empty RealNormSpace holds ex I be Function of [:X, Y:], [:X, ( product <*Y*>):] st I is one-to-one & I is onto & (for x be Point of X, y be Point of Y holds (I . (x,y)) = [x, <*y*>]) & (for v,w be Point of [:X, Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:X, Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:X, Y:])) = ( 0. [:X, ( product <*Y*>):]) & (for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.||)

    proof

      let X,Y be non empty RealNormSpace;

      consider J be Function of Y, ( product <*Y*>) such that

       A1: J is one-to-one & J is onto & (for y be Point of Y holds (J . y) = <*y*>) & (for v,w be Point of Y holds (J . (v + w)) = ((J . v) + (J . w))) & (for v be Point of Y, r be Element of REAL holds (J . (r * v)) = (r * (J . v))) & (J . ( 0. Y)) = ( 0. ( product <*Y*>)) & (for v be Point of Y holds ||.(J . v).|| = ||.v.||) by Th16;

      defpred P[ object, object, object] means $3 = [$1, <*$2*>];

      

       A2: for x,y be object st x in the carrier of X & y in the carrier of Y holds ex z be object st z in the carrier of [:X, ( product <*Y*>):] & P[x, y, z]

      proof

        let x,y be object;

        assume

         A3: x in the carrier of X & y in the carrier of Y;

        then

        reconsider y0 = y as Point of Y;

        (J . y0) = <*y0*> by A1;

        then [x, <*y*>] in [:the carrier of X, the carrier of ( product <*Y*>):] by A3, ZFMISC_1: 87;

        hence thesis;

      end;

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

       A4: for x,y be object st x in the carrier of X & y in the carrier of Y holds P[x, y, (I . (x,y))] from BINOP_1:sch 1( A2);

      reconsider I as Function of [:X, Y:], [:X, ( product <*Y*>):];

      take I;

      thus I is one-to-one

      proof

        now

          let z1,z2 be object;

          assume

           A5: z1 in the carrier of [:X, Y:] & z2 in the carrier of [:X, Y:] & (I . z1) = (I . z2);

          then

          consider x1,y1 be object such that

           A6: x1 in the carrier of X & y1 in the carrier of Y & z1 = [x1, y1] by ZFMISC_1:def 2;

          consider x2,y2 be object such that

           A7: x2 in the carrier of X & y2 in the carrier of Y & z2 = [x2, y2] by A5, ZFMISC_1:def 2;

          

           A8: [x1, <*y1*>] = (I . (x1,y1)) by A4, A6

          .= (I . (x2,y2)) by A5, A6, A7

          .= [x2, <*y2*>] by A4, A7;

          then <*y1*> = <*y2*> by XTUPLE_0: 1;

          then y1 = y2 by FINSEQ_1: 76;

          hence z1 = z2 by A6, A7, A8, XTUPLE_0: 1;

        end;

        hence thesis by FUNCT_2: 19;

      end;

      thus I is onto

      proof

        now

          let w be object;

          assume w in the carrier of [:X, ( product <*Y*>):];

          then

          consider x,y1 be object such that

           A9: x in the carrier of X & y1 in the carrier of ( product <*Y*>) & w = [x, y1] by ZFMISC_1:def 2;

          y1 in ( rng J) by A1, A9, FUNCT_2:def 3;

          then

          consider y be object such that

           A10: y in the carrier of Y & y1 = (J . y) by FUNCT_2: 11;

          

           A11: (J . y) = <*y*> by A10, A1;

          reconsider z = [x, y] as Element of [:the carrier of X, the carrier of Y:] by A9, A10, ZFMISC_1: 87;

          w = (I . (x,y)) by A4, A9, A10, A11

          .= (I . z);

          hence w in ( rng I) by FUNCT_2: 4;

        end;

        then the carrier of [:X, ( product <*Y*>):] c= ( rng I) by TARSKI:def 3;

        then the carrier of [:X, ( product <*Y*>):] = ( rng I) by XBOOLE_0:def 10;

        hence thesis by FUNCT_2:def 3;

      end;

      thus for x be Point of X, y be Point of Y holds (I . (x,y)) = [x, <*y*>] by A4;

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

      proof

        let v,w be Point of [:X, Y:];

        consider x1 be Point of X, x2 be Point of Y such that

         A12: v = [x1, x2] by Lm1;

        consider y1 be Point of X, y2 be Point of Y such that

         A13: w = [y1, y2] by Lm1;

        

         A14: (I . (v + w)) = (I . ((x1 + y1),(x2 + y2))) by A12, A13, Def1

        .= [(x1 + y1), <*(x2 + y2)*>] by A4;

        (I . v) = (I . (x1,x2)) & (I . w) = (I . (y1,y2)) by A12, A13;

        then

         A15: (I . v) = [x1, <*x2*>] & (I . w) = [y1, <*y2*>] by A4;

        

         A16: (J . x2) = <*x2*> & (J . y2) = <*y2*> by A1;

        then

        reconsider xx2 = <*x2*> as Point of ( product <*Y*>);

        reconsider yy2 = <*y2*> as Point of ( product <*Y*>) by A16;

         <*(x2 + y2)*> = (J . (x2 + y2)) by A1

        .= (xx2 + yy2) by A16, A1;

        hence ((I . v) + (I . w)) = (I . (v + w)) by A14, A15, Def1;

      end;

      thus for v be Point of [:X, Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Point of [:X, Y:], r be Element of REAL ;

        consider x1 be Point of X, x2 be Point of Y such that

         A17: v = [x1, x2] by Lm1;

        

         A18: (I . (r * v)) = (I . ((r * x1),(r * x2))) by A17, Th18

        .= [(r * x1), <*(r * x2)*>] by A4;

        

         A19: (I . v) = (I . (x1,x2)) by A17

        .= [x1, <*x2*>] by A4;

        

         A20: (J . x2) = <*x2*> by A1;

        then

        reconsider xx2 = <*x2*> as Point of ( product <*Y*>);

         <*(r * x2)*> = (J . (r * x2)) by A1

        .= (r * xx2) by A20, A1;

        hence (r * (I . v)) = (I . (r * v)) by A18, A19, Th18;

      end;

      

       A21: <*( 0. Y)*> = ( 0. ( product <*Y*>)) by A1;

      (I . ( 0. [:X, Y:])) = (I . (( 0. X),( 0. Y)));

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

      thus for v be Point of [:X, Y:] holds ||.(I . v).|| = ||.v.||

      proof

        let v be Point of [:X, Y:];

        consider x1 be Point of X, x2 be Point of Y such that

         A22: v = [x1, x2] by Lm1;

        

         A23: (J . x2) = <*x2*> by A1;

        then

        reconsider xx2 = <*x2*> as Point of ( product <*Y*>);

        

         A24: ex w be Element of ( REAL 2) st w = <* ||.x1.||, ||.x2.||*> & ||.v.|| = |.w.| by A22, Th18;

        (I . v) = (I . (x1,x2)) by A22

        .= [x1, <*x2*>] by A4;

        then ex s be Element of ( REAL 2) st s = <* ||.x1.||, ||.xx2.||*> & ||.(I . v).|| = |.s.| by Th18;

        hence ||.(I . v).|| = ||.v.|| by A23, A1, A24;

      end;

    end;

    theorem :: PRVECT_3:24

    for X be non empty RealNormSpace-Sequence, Y be RealNormSpace holds ex I be Function of [:( product X), Y:], ( product (X ^ <*Y*>)) st I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of Y holds ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & (I . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), Y:])) = ( 0. ( product (X ^ <*Y*>))) & (for v be Point of [:( product X), Y:] holds ||.(I . v).|| = ||.v.||)

    proof

      let X be non empty RealNormSpace-Sequence, Y be RealNormSpace;

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

       A1: I is one-to-one & I is onto & (for x be Point of ( product X), y be Point of Y holds (I . (x,y)) = [x, <*y*>]) & (for v,w be Point of [:( product X), Y:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Point of [:( product X), Y:], r be Element of REAL holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), Y:])) = ( 0. [:( product X), ( product <*Y*>):]) & (for v be Point of [:( product X), Y:] holds ||.(I . v).|| = ||.v.||) by Th23;

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

       A2: J is one-to-one & J is onto & (for x be Point of ( product X), y be Point of ( product <*Y*>) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (J . (x,y)) = (x1 ^ y1)) & (for v,w be Point of [:( product X), ( product <*Y*>):] holds (J . (v + w)) = ((J . v) + (J . w))) & (for v be Point of [:( product X), ( product <*Y*>):], r be Element of REAL holds (J . (r * v)) = (r * (J . v))) & (J . ( 0. [:( product X), ( product <*Y*>):])) = ( 0. ( product (X ^ <*Y*>))) & (for v be Point of [:( product X), ( product <*Y*>):] holds ||.(J . v).|| = ||.v.||) by Th17;

      set K = (J * I);

      reconsider K as Function of [:( product X), Y:], ( product (X ^ <*Y*>));

      take K;

      thus K is one-to-one by A1, A2;

      

       A3: ( rng J) = the carrier of ( product (X ^ <*Y*>)) by A2, FUNCT_2:def 3;

      ( rng I) = the carrier of [:( product X), ( product <*Y*>):] by A1, FUNCT_2:def 3;

      

      then ( rng (J * I)) = (J .: the carrier of [:( product X), ( product <*Y*>):]) by RELAT_1: 127

      .= the carrier of ( product (X ^ <*Y*>)) by A3, RELSET_1: 22;

      hence K is onto by FUNCT_2:def 3;

      thus for x be Point of ( product X), y be Point of Y holds ex x1,y1 be FinSequence st x = x1 & <*y*> = y1 & (K . (x,y)) = (x1 ^ y1)

      proof

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

        

         A4: (I . (x,y)) = [x, <*y*>] by A1;

         [x, y] in the carrier of [:( product X), Y:];

        then [x, <*y*>] in the carrier of [:( product X), ( product <*Y*>):] by A4, FUNCT_2: 5;

        then

        reconsider yy = <*y*> as Point of ( product <*Y*>) by ZFMISC_1: 87;

        consider x1,y1 be FinSequence such that

         A5: x = x1 & yy = y1 & (J . (x,yy)) = (x1 ^ y1) by A2;

        (J . (x,yy)) = (J . (I . [x, y])) by A4

        .= (K . (x,y)) by FUNCT_2: 15;

        hence thesis by A5;

      end;

      thus for v,w be Point of [:( product X), Y:] holds (K . (v + w)) = ((K . v) + (K . w))

      proof

        let v,w be Point of [:( product X), Y:];

        

        thus (K . (v + w)) = (J . (I . (v + w))) by FUNCT_2: 15

        .= (J . ((I . v) + (I . w))) by A1

        .= ((J . (I . v)) + (J . (I . w))) by A2

        .= ((K . v) + (J . (I . w))) by FUNCT_2: 15

        .= ((K . v) + (K . w)) by FUNCT_2: 15;

      end;

      thus for v be Point of [:( product X), Y:], r be Element of REAL holds (K . (r * v)) = (r * (K . v))

      proof

        let v be Point of [:( product X), Y:], r be Element of REAL ;

        

        thus (K . (r * v)) = (J . (I . (r * v))) by FUNCT_2: 15

        .= (J . (r * (I . v))) by A1

        .= (r * (J . (I . v))) by A2

        .= (r * (K . v)) by FUNCT_2: 15;

      end;

      thus (K . ( 0. [:( product X), Y:])) = ( 0. ( product (X ^ <*Y*>))) by A1, A2, FUNCT_2: 15;

      thus for v be Point of [:( product X), Y:] holds ||.(K . v).|| = ||.v.||

      proof

        let v be Point of [:( product X), Y:];

        

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

        .= ||.(I . v).|| by A2

        .= ||.v.|| by A1;

      end;

    end;