vectsp12.miz



    begin

    reserve K,F for Ring;

    reserve V,W for VectSp of K;

    reserve l for Linear_Combination of V;

    reserve T for linear-transformation of V, W;

    theorem :: VECTSP12:1

    for K be Field, V,W be finite-dimensional VectSp of K, A be Subset of V, B be Basis of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A) st A is Basis of ( ker T) & A c= B holds (T . ( Sum l)) = ( Sum (T @* l))

    proof

      let K be Field, V,W be finite-dimensional VectSp of K, A be Subset of V, B be Basis of V, T be linear-transformation of V, W, l be Linear_Combination of (B \ A);

      assume A is Basis of ( ker T) & A c= B;

      then

       A1: (T | (B \ A)) is one-to-one by RANKNULL: 22;

      

       A2: ((T | (B \ A)) | ( Carrier l)) = (T | ( Carrier l)) by RELAT_1: 74, VECTSP_6:def 4;

      then

       A3: (T | ( Carrier l)) is one-to-one by A1, FUNCT_1: 52;

      consider G be FinSequence of V such that

       A4: G is one-to-one and

       A5: ( rng G) = ( Carrier l) and

       A6: ( Sum l) = ( Sum (l (#) G)) by VECTSP_6:def 6;

      set H = (T * G);

      

       A7: ( rng H) = (T .: ( Carrier l)) by A5, RELAT_1: 127

      .= ( Carrier (T @* l)) by A3, ZMODUL05: 56;

      ( dom T) = ( [#] V) by RANKNULL: 7;

      then H is one-to-one by A1, A2, A4, A5, FUNCT_1: 52, RANKNULL: 1;

      then

       A8: ( Sum (T @* l)) = ( Sum ((T @* l) (#) H)) by A7, VECTSP_6:def 6;

      (T * (l (#) G)) = ((T @* l) (#) H) by A3, A5, ZMODUL05: 55;

      hence thesis by A6, A8, MATRLIN: 16;

    end;

    

     HM11: for F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y, A be Subset of X st T is bijective holds A is Basis of X implies (T .: A) is Basis of Y

    proof

      let F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y, A be Subset of X;

      assume

       AS1: T is bijective;

      assume A is Basis of X;

      then

       P1: A is linearly-independent & ( Lin A) = the ModuleStr of X by VECTSP_7:def 3;

      

       D1: ( dom T) = the carrier of X by FUNCT_2:def 1;

      

       R1: ( rng T) = the carrier of Y by FUNCT_2:def 3, AS1;

      

       P2: (T .: A) is linearly-independent by ZMODUL06: 45, AS1, P1;

      

       P6: ( Lin (T .: A)) is strict Subspace of ( (Omega). Y) by ZMODUL06: 47;

      the carrier of ( Lin (T .: A)) = (T .: the carrier of the ModuleStr of X) by P1, AS1, ZMODUL06: 46

      .= the carrier of ( (Omega). Y) by D1, R1, RELAT_1: 113;

      hence thesis by P2, VECTSP_7:def 3, P6, VECTSP_4: 31;

    end;

    theorem :: VECTSP12:2

    

     HM12: for F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y, A be Subset of X st T is bijective holds A is Basis of X iff (T .: A) is Basis of Y

    proof

      let F be Field, X,Y be VectSp of F, L be linear-transformation of X, Y, A be Subset of X;

      assume

       AS1: L is bijective;

      

       D1: ( dom L) = the carrier of X by FUNCT_2:def 1;

      consider K be linear-transformation of Y, X such that

       AS3: K = (L " ) & K is bijective by ZMODUL06: 42, AS1;

      thus A is Basis of X implies (L .: A) is Basis of Y by AS1, HM11;

      assume (L .: A) is Basis of Y;

      then (K .: (L .: A)) is Basis of X by AS3, HM11;

      hence thesis by D1, AS1, AS3, FUNCT_1: 107;

    end;

    

     HM13: for F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y st T is bijective holds X is finite-dimensional implies Y is finite-dimensional

    proof

      let F be Field, X,Y be VectSp of F, L be linear-transformation of X, Y;

      assume

       AS1: L is bijective;

      assume X is finite-dimensional;

      then

      consider A be finite Subset of X such that

       P1: A is Basis of X;

      (L .: A) is Basis of Y by P1, HM12, AS1;

      hence thesis;

    end;

    theorem :: VECTSP12:3

    

     HM151: for F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y st T is bijective holds X is finite-dimensional iff Y is finite-dimensional

    proof

      let F be Field, X,Y be VectSp of F, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      consider K be linear-transformation of Y, X such that

       AS3: K = (T " ) & K is bijective by ZMODUL06: 42, AS1;

      thus thesis by HM13, AS1, AS3;

    end;

    theorem :: VECTSP12:4

    

     HM15: for F be Field, X be finite-dimensional VectSp of F, Y be VectSp of F, T be linear-transformation of X, Y st T is bijective holds Y is finite-dimensional & ( dim X) = ( dim Y)

    proof

      let F be Field, X be finite-dimensional VectSp of F, Y be VectSp of F, T be linear-transformation of X, Y;

      assume

       AS1: T is bijective;

      hence

       X1: Y is finite-dimensional by HM151;

      for I be Basis of X holds ( dim Y) = ( card I)

      proof

        let I be Basis of X;

        ( dom T) = the carrier of X by FUNCT_2:def 1;

        then

         X12: ( card I) = ( card (T .: I)) by CARD_1: 5, AS1, CARD_1: 33;

        (T .: I) is Basis of Y by AS1, HM12;

        hence ( dim Y) = ( card I) by X1, X12, VECTSP_9:def 1;

      end;

      hence thesis by VECTSP_9:def 1;

    end;

    theorem :: VECTSP12:5

    for F be Field, X,Y be VectSp of F, l be Linear_Combination of X, T be linear-transformation of X, Y st T is one-to-one holds (T @ l) = (T @* l)

    proof

      let F be Field, X,Y be VectSp of F, l be Linear_Combination of X, T be linear-transformation of X, Y;

      assume

       AS: T is one-to-one;

      

       A1: ( Carrier (T @ l)) c= (T .: ( Carrier l)) by RANKNULL: 30;

      for y be Element of Y holds ((T @ l) . y) = ( Sum ( lCFST (l,T,y)))

      proof

        let y be Element of Y;

        ( rng ( lCFST (l,T,y))) c= the carrier of F;

        then

        reconsider Z = ( lCFST (l,T,y)) as FinSequence of F by FINSEQ_1:def 4;

        

         C0: ((T @ l) . y) = ( Sum (l .: (T " {y}))) by RANKNULL:def 5;

        per cases ;

          suppose

           C1: (T " {y}) = {} ;

          then ( lCFST (l,T,y)) = ( <*> the carrier of F);

          then

           C2: ( Sum ( lCFST (l,T,y))) = ( 0. F) by RLVECT_1: 43;

          (l .: (T " {y})) = ( {} F) by C1;

          hence ((T @ l) . y) = ( Sum ( lCFST (l,T,y))) by C0, C2, RLVECT_2: 8;

        end;

          suppose (T " {y}) <> {} ;

          then

          consider x be object such that

           X1: x in (T " {y}) by XBOOLE_0:def 1;

          

           X2: x in ( dom T) & (T . x) in {y} by X1, FUNCT_1:def 7;

          reconsider x as Element of X by X1;

          

           C2: (T . x) = y by X2, TARSKI:def 1;

          y in ( rng T) by X2, C2, FUNCT_1:def 3;

          then

           C3: ex x0 be object st (T " {y}) = {x0} by AS, FUNCT_1: 74;

          then

           C31: (T " {y}) = {x} by X1, TARSKI:def 1;

          

           C81: ( dom l) = the carrier of X by FUNCT_2:def 1;

          

           C9: (l .: (T " {y})) = ( Im (l,x)) by C3, X1, TARSKI:def 1

          .= {(l . x)} by C81, FUNCT_1: 59;

          per cases ;

            suppose

             C61: x in ( Carrier l);

            then

             C6: ((T " {y}) /\ ( Carrier l)) = {x} by C31, XBOOLE_1: 28, ZFMISC_1: 31;

            ( dom l) = the carrier of X by FUNCT_2:def 1;

            then ( rng ( canFS ((T " {y}) /\ ( Carrier l)))) c= ( dom l) by XBOOLE_1: 1;

            

            then

             C81: ( dom Z) = ( dom ( canFS ((T " {y}) /\ ( Carrier l)))) by RELAT_1: 27

            .= ( dom ( canFS {x})) by C31, C61, XBOOLE_1: 28, ZFMISC_1: 31

            .= ( dom <*x*>) by FINSEQ_1: 94

            .= ( Seg 1) by FINSEQ_1: 38;

            then

             C82: ( len Z) = 1 by FINSEQ_1:def 3;

            1 in ( dom Z) by C81;

            

            then (Z . 1) = (l . (( canFS {x}) . 1)) by C6, FUNCT_1: 12

            .= (l . ( <*x*> . 1)) by FINSEQ_1: 94

            .= (l . x) by FINSEQ_1: 40;

            then

             C83: Z = <*(l . x)*> by FINSEQ_1: 40, C82;

            then

             C8: Z = ( canFS {(l . x)}) by FINSEQ_1: 94;

            ( rng Z) = (l .: (T " {y})) by C9, C83, FINSEQ_1: 38;

            hence ((T @ l) . y) = ( Sum ( lCFST (l,T,y))) by C0, C8, RLVECT_2:def 2;

          end;

            suppose

             C5: not x in ( Carrier l);

            ((T " {y}) /\ ( Carrier l)) = {}

            proof

              assume ((T " {y}) /\ ( Carrier l)) <> {} ;

              then

              consider x0 be object such that

               C60: x0 in ((T " {y}) /\ ( Carrier l)) by XBOOLE_0:def 1;

              x0 in (T " {y}) & x0 in ( Carrier l) by C60, XBOOLE_0:def 4;

              hence contradiction by C5, C31, TARSKI:def 1;

            end;

            then Z = ( <*> the carrier of F);

            then

             C8: ( Sum ( lCFST (l,T,y))) = ( 0. F) by RLVECT_1: 43;

            (l .: (T " {y})) = {( 0. F)} by C5, C9;

            hence ((T @ l) . y) = ( Sum ( lCFST (l,T,y))) by C0, C8, RLVECT_2: 9;

          end;

        end;

      end;

      hence thesis by A1, ZMODUL05:def 8;

    end;

    begin

    theorem :: VECTSP12:6

    

     FRds1: for K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2 st V is_the_direct_sum_of (W1,W2) holds (I1 /\ I2) = {}

    proof

      let K be Field;

      let V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2 such that

       A1: V is_the_direct_sum_of (W1,W2);

      assume (I1 /\ I2) <> {} ;

      then

      consider v be object such that

       A2: v in (I1 /\ I2) by XBOOLE_0: 7;

      

       A3: v in I1 by A2, XBOOLE_0:def 4;

       not ( 0. W1) in I1 by VECTSP_7: 2, VECTSP_7:def 3;

      then

       A4: v <> ( 0. V) by A3, VECTSP_4: 11;

      

       A5: v in W1 by A3;

      v in W2 by A2;

      then v in (W1 /\ W2) by A5, VECTSP_5: 3;

      then v in ( (0). V) by A1, VECTSP_5:def 4;

      hence contradiction by A4, VECTSP_4: 35;

    end;

    theorem :: VECTSP12:7

    

     FRds2: for K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V st V is_the_direct_sum_of (W1,W2) & I = (I1 \/ I2) holds ( Lin I) = the ModuleStr of V

    proof

      let K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V such that

       A1: V is_the_direct_sum_of (W1,W2) and

       A2: I = (I1 \/ I2);

      the carrier of W1 c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider II1 = I1 as Subset of V by XBOOLE_1: 1;

      the carrier of W2 c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider II2 = I2 as Subset of V by XBOOLE_1: 1;

      

       A5: the ModuleStr of W1 = ( Lin I1) by VECTSP_7:def 3

      .= ( Lin II1) by VECTSP_9: 17;

      

       A6: the ModuleStr of W2 = ( Lin I2) by VECTSP_7:def 3

      .= ( Lin II2) by VECTSP_9: 17;

      for x be Vector of V holds x in (W1 + W2) iff x in (( Lin II1) + ( Lin II2))

      proof

        let x be Vector of V;

        hereby

          assume x in (W1 + W2);

          then

          consider x1,x2 be Vector of V such that

           B1: x1 in W1 & x2 in W2 & x = (x1 + x2) by VECTSP_5: 1;

          

           B2: x1 in ( Lin II1) by A5, B1;

          x2 in ( Lin II2) by A6, B1;

          hence x in (( Lin II1) + ( Lin II2)) by B1, B2, VECTSP_5: 1;

        end;

        assume x in (( Lin II1) + ( Lin II2));

        then

        consider x1,x2 be Vector of V such that

         B1: x1 in ( Lin II1) & x2 in ( Lin II2) & x = (x1 + x2) by VECTSP_5: 1;

        

         B2: x1 in W1 by A5, B1;

        x2 in W2 by A6, B1;

        hence x in (W1 + W2) by B1, B2, VECTSP_5: 1;

      end;

      then

       A7: (W1 + W2) = (( Lin II1) + ( Lin II2)) by VECTSP_4: 30;

      

      thus the ModuleStr of V = (W1 + W2) by A1, VECTSP_5:def 4

      .= ( Lin I) by A2, A7, VECTSP_7: 15;

    end;

    theorem :: VECTSP12:8

    

     FRds3: for K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V st V is_the_direct_sum_of (W1,W2) & I = (I1 \/ I2) holds I is linearly-independent

    proof

      let K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2, I be Subset of V such that

       A1: V is_the_direct_sum_of (W1,W2) and

       A2: I = (I1 \/ I2);

      assume I is linearly-dependent;

      then

      consider l be Linear_Combination of I such that

       A3: ( Sum l) = ( 0. V) and

       A4: ( Carrier l) <> {} ;

      

       A5A: (I1 /\ I2) = {} by A1, FRds1;

      

       A5B: I1 misses I2 by A1, FRds1;

      the carrier of W1 c= the carrier of V & the carrier of W2 c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider II1 = I1, II2 = I2 as Subset of V by XBOOLE_1: 1;

      consider l1 be Linear_Combination of II1, l2 be Linear_Combination of II2 such that

       A6: l = (l1 + l2) by A2, A5A, ZMODUL04: 26;

      reconsider ll1 = l1 as Linear_Combination of I by A2, XBOOLE_1: 7, VECTSP_6: 4;

      reconsider ll2 = l2 as Linear_Combination of I by A2, XBOOLE_1: 7, VECTSP_6: 4;

      

       A7: ( Sum l) = (( Sum ll1) + ( Sum ll2)) by A6, VECTSP_6: 44;

      set v1 = ( Sum ll1);

      set v2 = ( Sum ll2);

      ( Carrier ll1) c= I1 & ( Carrier ll2) c= I2 by VECTSP_6:def 4;

      then

       A8: (( Carrier ll1) /\ ( Carrier ll2)) = {} by A5B, XBOOLE_0:def 7, XBOOLE_1: 64;

      

       A10: v1 <> ( 0. V)

      proof

        assume

         B1: v1 = ( 0. V);

        II1 is linearly-independent by VECTSP_7:def 3, VECTSP_9: 11;

        then

         B3: ( Carrier l1) = {} by B1;

        II2 is linearly-independent by VECTSP_7:def 3, VECTSP_9: 11;

        then (( Carrier ll1) \/ ( Carrier ll2)) = {} by A3, A7, B1, B3;

        hence contradiction by A4, A6, A8, ZMODUL04: 25;

      end;

      

       A13: v1 = ( - v2) by A3, A7, RLVECT_1: 6;

      v1 in ( Lin II1) by VECTSP_7: 7;

      then v1 in ( Lin I1) by VECTSP_9: 17;

      then v1 in the ModuleStr of W1 by VECTSP_7:def 3;

      then

       A14: v1 in W1;

      v2 in ( Lin II2) by VECTSP_7: 7;

      then v2 in ( Lin I2) by VECTSP_9: 17;

      then v2 in the ModuleStr of W2 by VECTSP_7:def 3;

      then v2 in W2;

      then

       A15: v1 in W2 by A13, VECTSP_4: 22;

      (W1 /\ W2) = ( (0). V) by A1, VECTSP_5:def 4;

      hence contradiction by A10, A14, A15, VECTSP_5: 3, VECTSP_4: 35;

    end;

    theorem :: VECTSP12:9

    for K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2 st (W1 /\ W2) = ( (0). V) holds (I1 \/ I2) is Basis of (W1 + W2)

    proof

      let K be Field, V be VectSp of K, W1,W2 be Subspace of V, I1 be Basis of W1, I2 be Basis of W2 such that

       P1: (W1 /\ W2) = ( (0). V);

      set I = (I1 \/ I2);

      reconsider W = (W1 + W2) as strict Subspace of V;

      reconsider WW1 = W1, WW2 = W2 as Subspace of W by VECTSP_5: 7;

      the carrier of WW1 c= the carrier of W & the carrier of WW2 c= the carrier of W by VECTSP_4:def 2;

      then I1 c= the carrier of W & I2 c= the carrier of W;

      then

      reconsider I0 = I as Subset of W by XBOOLE_1: 8;

      reconsider I10 = I1 as Basis of WW1;

      reconsider I20 = I2 as Basis of WW2;

      

       A2: (WW1 /\ WW2) is Subspace of V by VECTSP_4: 26;

      

       A3: (WW1 + WW2) is Subspace of V by VECTSP_4: 26;

      for x be object holds x in (WW1 /\ WW2) iff x in ( (0). V)

      proof

        let x be object;

        hereby

          assume x in (WW1 /\ WW2);

          then x in WW1 & x in WW2 by VECTSP_5: 3;

          hence x in ( (0). V) by P1, VECTSP_5: 3;

        end;

        assume x in ( (0). V);

        then x in W1 & x in W2 by P1, VECTSP_5: 3;

        hence x in (WW1 /\ WW2) by VECTSP_5: 3;

      end;

      then for x be Vector of V holds x in (WW1 /\ WW2) iff x in ( (0). V);

      

      then

       A4: (WW1 /\ WW2) = ( (0). V) by A2, VECTSP_4: 30

      .= ( (0). W) by VECTSP_4: 36;

      for x be object holds x in W iff x in (WW1 + WW2)

      proof

        let x be object;

        hereby

          assume x in W;

          then

          consider x1,x2 be Vector of V such that

           B2: x1 in W1 & x2 in W2 & x = (x1 + x2) by VECTSP_5: 1;

          x1 in (W1 + W2) by B2, VECTSP_5: 2;

          then

          reconsider xx1 = x1 as Vector of W;

          x2 in (W1 + W2) by B2, VECTSP_5: 2;

          then

          reconsider xx2 = x2 as Vector of W;

          x = (xx1 + xx2) by B2, VECTSP_4: 13;

          hence x in (WW1 + WW2) by B2, VECTSP_5: 1;

        end;

        assume x in (WW1 + WW2);

        then

        consider x1,x2 be Vector of W such that

         B2: x1 in WW1 & x2 in WW2 & x = (x1 + x2) by VECTSP_5: 1;

        thus x in W by B2;

      end;

      then for x be Vector of V holds x in W iff x in (WW1 + WW2);

      then W = (WW1 + WW2) by A3, VECTSP_4: 30;

      then I0 is base by A4, FRds2, FRds3, VECTSP_5:def 4;

      hence thesis;

    end;

    begin

    theorem :: VECTSP12:10

    

     Th38A: for K be Field holds for V be finite-dimensional VectSp of K, W be Subspace of V holds ex S be Linear_Compl of W, T be linear-transformation of S, ( VectQuot (V,W)) st T is bijective & for v be Vector of V st v in S holds (T . v) = (v + W)

    proof

      let K be Field;

      let V be finite-dimensional VectSp of K, W be Subspace of V;

      set S = the Linear_Compl of W;

      set aC = ( addCoset (V,W));

      set C = ( CosetSet (V,W));

      set Vq = ( VectQuot (V,W));

      defpred P[ Vector of V, Vector of Vq] means $2 = ($1 + W);

       A2:

      now

        let v be Vector of V;

        reconsider y = (v + W) as Vector of Vq by VECTSP10: 23;

        take y;

        thus P[v, y];

      end;

      consider ff be Function of the carrier of V, the carrier of Vq such that

       A7: for v be Vector of V holds P[v, (ff . v)] from FUNCT_2:sch 3( A2);

      set T = (ff | the carrier of S);

      

       S1: the carrier of S c= the carrier of V by VECTSP_4:def 2;

      then

      reconsider T as Function of the carrier of S, the carrier of Vq by FUNCT_2: 32;

      

       P1: for v be Vector of V st v in S holds (T . v) = (v + W)

      proof

        let v be Vector of V;

        assume v in S;

        

        hence (T . v) = (ff . v) by FUNCT_1: 49

        .= (v + W) by A7;

      end;

      now

        let a,b be Vector of S;

        reconsider a1 = a, b1 = b as Vector of V by S1;

        

         A91: a1 in S & b1 in S;

        (a1 + b1) = (a + b) by VECTSP_4: 13;

        then

         A94: (a1 + b1) in S;

        

         A95: (T . a) = (a1 + W) by P1, A91;

        

         A96: (T . b) = (b1 + W) by P1, A91;

        

        thus (T . (a + b)) = (T . (a1 + b1)) by VECTSP_4: 13

        .= ((a1 + b1) + W) by A94, P1

        .= ((T . a) + (T . b)) by A95, A96, VECTSP10: 26;

      end;

      then

       AD: T is additive;

      now

        let a be Vector of S;

        let r be Element of K;

        reconsider a1 = a as Vector of V by S1;

        

         A91: a1 in S;

        (r * a) = (r * a1) by VECTSP_4: 14;

        then

         A94: (r * a1) in S;

        

         A95: (T . a) = (a1 + W) by P1, A91;

        

        thus (T . (r * a)) = (T . (r * a1)) by VECTSP_4: 14

        .= ((r * a1) + W) by A94, P1

        .= (r * (T . a)) by A95, VECTSP10: 25;

      end;

      then T is homogeneous;

      then

      reconsider T as linear-transformation of S, Vq by AD;

      

       A100: V is_the_direct_sum_of (S,W) by VECTSP_5:def 5;

      the carrier of Vq c= ( rng T)

      proof

        let y be object;

        assume y in the carrier of Vq;

        then

        consider a be Vector of V such that

         A10: y = (a + W) by VECTSP10: 22;

         the ModuleStr of V = (S + W) by A100, VECTSP_5:def 4;

        then a in (S + W);

        then

        consider s,w be Element of V such that

         A12: s in S & w in W & a = (s + w) by VECTSP_5: 1;

        reconsider s0 = s as Vector of S by A12;

        reconsider B = (s + W) as Vector of Vq by VECTSP10: 23;

        reconsider A = (a + W), Z = (w + W) as Vector of Vq by VECTSP10: 23;

        Z = ( zeroCoset (V,W)) by A12, VECTSP_4: 49

        .= ( 0. Vq) by VECTSP10:def 6;

        

        then

         A13: B = (B + Z)

        .= A by A12, VECTSP10: 26;

        (T . s0) = y by A10, A12, A13, P1;

        hence y in ( rng T) by FUNCT_2: 4;

      end;

      then ( rng T) = the carrier of Vq;

      then

       A14: T is onto;

      

       X1: for x1,x2 be object st x1 in the carrier of S & x2 in the carrier of S & (T . x1) = (T . x2) holds x1 = x2

      proof

        let x1,x2 be object;

        assume

         A15: x1 in the carrier of S & x2 in the carrier of S & (T . x1) = (T . x2);

        then

        reconsider a1 = x1, a2 = x2 as Vector of V by S1;

        

         A16: a1 in S & a2 in S by A15;

        

         A17: (T . x1) = (a1 + W) by P1, A16;

        (T . x2) = (a2 + W) by P1, A16;

        then

        consider w be Element of V such that

         A19: w in W & a2 = (a1 + w) by A15, A17, VECTSP_4: 42, VECTSP_4: 55;

        

         A20: (a2 - a1) = (w + (a1 - a1)) by A19, RLVECT_1: 28

        .= (w + ( 0. V)) by VECTSP_1: 19

        .= w;

        (a2 - a1) in S by A16, VECTSP_4: 23;

        then (a2 - a1) in (S /\ W) by A19, A20, VECTSP_5: 3;

        then (a2 - a1) in ( (0). V) by A100, VECTSP_5:def 4;

        then (a2 - a1) = ( 0. V) by VECTSP_4: 35;

        hence x1 = x2 by RLVECT_1: 21;

      end;

      take S, T;

      thus thesis by A14, P1, X1, FUNCT_2: 19;

    end;

    theorem :: VECTSP12:11

    for K be Field holds for V be finite-dimensional VectSp of K, W be Subspace of V holds ( VectQuot (V,W)) is finite-dimensional & (( dim ( VectQuot (V,W))) + ( dim W)) = ( dim V)

    proof

      let K be Field;

      let V be finite-dimensional VectSp of K, W be Subspace of V;

      set Vq = ( VectQuot (V,W));

      consider S be Linear_Compl of W, T be linear-transformation of S, Vq such that

       X1: T is bijective and for v be Vector of V st v in S holds (T . v) = (v + W) by Th38A;

      Vq is finite-dimensional & ( dim S) = ( dim Vq) by HM15, X1;

      hence thesis by VECTSP_5:def 5, VECTSP_9: 34;

    end;

    definition

      let K be Ring;

      let V,U be VectSp of K;

      let W be Subspace of V;

      let f be linear-transformation of V, U;

      assume

       A1: the carrier of W c= the carrier of ( ker f);

      :: VECTSP12:def1

      func QFunctional (f,W) -> linear-transformation of ( VectQuot (V,W)), U means

      : Def12: for A be Vector of ( VectQuot (V,W)), a be Vector of V st A = (a + W) holds (it . A) = (f . a);

      existence

      proof

        defpred P[ set, set] means for a be Vector of V st $1 = (a + W) holds $2 = (f . a);

        set aC = ( addCoset (V,W));

        set C = ( CosetSet (V,W));

        set vq = ( VectQuot (V,W));

         A2:

        now

          let A be Vector of vq;

          consider a be Vector of V such that

           A3: A = (a + W) by VECTSP10: 22;

          take y = (f . a);

          thus P[A, y]

          proof

            let a1 be Vector of V;

            assume A = (a1 + W);

            then

            consider w be Vector of V such that

             A4: w in W and

             A5: a = (a1 + w) by A3, VECTSP_4: 42, VECTSP_4: 44;

            w in ( ker f) by A1, A4;

            then

             A6: (f . w) = ( 0. U) by RANKNULL: 10;

            

            thus y = ((f . a1) + (f . w)) by A5, VECTSP_1:def 20

            .= (f . a1) by A6;

          end;

        end;

        consider ff be Function of the carrier of vq, the carrier of U such that

         A7: for A be Vector of vq holds P[A, (ff . A)] from FUNCT_2:sch 3( A2);

        reconsider ff as Function of vq, U;

        

         A8: C = the carrier of vq by VECTSP10:def 6;

        now

          

           A9: the addF of vq = ( addCoset (V,W)) by VECTSP10:def 6;

          let A,B be Vector of vq;

          consider a be Vector of V such that

           A10: A = (a + W) by VECTSP10: 22;

          consider b be Vector of V such that

           A11: B = (b + W) by VECTSP10: 22;

          (aC . (A,B)) = ((a + b) + W) by A8, A10, A11, VECTSP10:def 3;

          

          hence (ff . (A + B)) = (f . (a + b)) by A7, A9

          .= ((f . a) + (f . b)) by VECTSP_1:def 20

          .= ((ff . A) + (f . b)) by A7, A10

          .= ((ff . A) + (ff . B)) by A7, A11;

        end;

        then

         AD: ff is additive;

        now

          let A be Vector of vq;

          let r be Element of K;

          

           A2: C = the carrier of vq by VECTSP10:def 6;

          then A in C;

          then

          consider aa be Coset of W such that

           A3: A = aa;

          consider a be Vector of V such that

           A4: aa = (a + W) by VECTSP_4:def 6;

          (r * A) = (( lmultCoset (V,W)) . (r,A)) by VECTSP10:def 6

          .= ((r * a) + W) by A2, A3, A4, VECTSP10:def 5;

          

          hence (ff . (r * A)) = (f . (r * a)) by A7

          .= (r * (f . a)) by MOD_2:def 2

          .= (r * (ff . A)) by A3, A4, A7;

        end;

        then ff is homogeneous;

        then

        reconsider ff as linear-transformation of vq, U by AD;

        take ff;

        thus thesis by A7;

      end;

      uniqueness

      proof

        set vq = ( VectQuot (V,W));

        let f1,f2 be linear-transformation of vq, U such that

         A12: for A be Vector of ( VectQuot (V,W)), a be Vector of V st A = (a + W) holds (f1 . A) = (f . a) and

         A13: for A be Vector of ( VectQuot (V,W)), a be Vector of V st A = (a + W) holds (f2 . A) = (f . a);

        now

          let A be Vector of vq;

          consider a be Vector of V such that

           A14: A = (a + W) by VECTSP10: 22;

          

          thus (f1 . A) = (f . a) by A12, A14

          .= (f2 . A) by A13, A14;

        end;

        hence thesis;

      end;

    end

    definition

      let K be Ring;

      let V,U be VectSp of K;

      let f be linear-transformation of V, U;

      :: VECTSP12:def2

      func CQFunctional (f) -> linear-transformation of ( VectQuot (V,( ker f))), U equals ( QFunctional (f,( ker f)));

      coherence ;

    end

    registration

      let K be Ring;

      let V,U be VectSp of K, f be linear-transformation of V, U;

      cluster ( CQFunctional f) -> one-to-one;

      coherence

      proof

        set T = ( CQFunctional f);

        set Vq = ( VectQuot (V,( ker f)));

        for x1,x2 be object st x1 in the carrier of Vq & x2 in the carrier of Vq & (T . x1) = (T . x2) holds x1 = x2

        proof

          let xx1,xx2 be object;

          assume

           AS: xx1 in the carrier of Vq & xx2 in the carrier of Vq & (T . xx1) = (T . xx2);

          then

          reconsider x1 = xx1, x2 = xx2 as Vector of Vq;

          consider a1 be Vector of V such that

           A14: x1 = (a1 + ( ker f)) by VECTSP10: 22;

          consider a2 be Vector of V such that

           A15: x2 = (a2 + ( ker f)) by VECTSP10: 22;

          (f . a1) = (T . x1) by A14, Def12

          .= (f . a2) by AS, A15, Def12;

          then

           A16: (a1 - a2) in ( ker f) by RANKNULL: 17;

          a1 = (a1 - ( 0. V))

          .= (a1 - (a2 - a2)) by VECTSP_1: 19

          .= (a2 + (a1 - a2)) by RLVECT_1: 29;

          then a1 in x1 & a1 in x2 by A14, A15, A16, VECTSP_4: 44;

          hence xx1 = xx2 by VECTSP_4: 56, A14, A15;

        end;

        hence thesis by FUNCT_2: 19;

      end;

    end

    theorem :: VECTSP12:12

    for K be Ring, V,U be VectSp of K, f be linear-transformation of V, U holds ex T be linear-transformation of ( VectQuot (V,( ker f))), ( im f) st T = ( CQFunctional f) & T is bijective

    proof

      let K be Ring, V,U be VectSp of K, f be linear-transformation of V, U;

      set T = ( CQFunctional f);

      set Vq = ( VectQuot (V,( ker f)));

      

       Q0: the carrier of ( im f) = ( [#] ( im f))

      .= (f .: ( [#] V)) by RANKNULL:def 2

      .= (f .: ( dom f)) by FUNCT_2:def 1

      .= ( rng f) by RELAT_1: 113;

      

       Q1: for x be object holds x in ( rng T) iff x in ( rng f)

      proof

        let x be object;

        hereby

          assume x in ( rng T);

          then

          consider z be object such that

           Q12: z in ( dom T) & x = (T . z) by FUNCT_1:def 3;

          reconsider z as Vector of Vq by Q12;

          consider a be Vector of V such that

           A14: z = (a + ( ker f)) by VECTSP10: 22;

          (T . z) = (f . a) by A14, Def12;

          hence x in ( rng f) by Q12, FUNCT_2: 4;

        end;

        assume x in ( rng f);

        then

        consider a be object such that

         Q12: a in ( dom f) & x = (f . a) by FUNCT_1:def 3;

        reconsider a as Vector of V by Q12;

        reconsider z = (a + ( ker f)) as Vector of Vq by VECTSP10: 23;

        (T . z) = (f . a) by Def12;

        hence x in ( rng T) by Q12, FUNCT_2: 4;

      end;

      then

       P1: ( rng T) = the carrier of ( im f) by Q0, TARSKI: 2;

      the carrier of ( VectQuot (V,( ker f))) = ( dom T) by FUNCT_2:def 1;

      then

      reconsider T as Function of the carrier of ( VectQuot (V,( ker f))), the carrier of ( im f) by FUNCT_2: 2, P1;

      

       A1: T is onto by Q0, Q1, TARSKI: 2;

      set Tq = ( CQFunctional f);

      now

        let A,B be Vector of Vq;

        

        thus (T . (A + B)) = ((Tq . A) + (Tq . B)) by VECTSP_1:def 20

        .= ((T . A) + (T . B)) by VECTSP_4: 13;

      end;

      then

       AD: T is additive;

      now

        let A be Vector of Vq;

        let r be Element of K;

        

        thus (T . (r * A)) = (r * (Tq . A)) by MOD_2:def 2

        .= (r * (T . A)) by VECTSP_4: 14;

      end;

      then T is homogeneous;

      then

      reconsider T as linear-transformation of Vq, ( im f) by AD;

      take T;

      thus thesis by A1;

    end;

    definition

      let K be Ring, V,U,W be VectSp of K, f be linear-transformation of V, U, g be linear-transformation of U, W;

      :: original: *

      redefine

      func g * f -> linear-transformation of V, W ;

      correctness

      proof

        (g * f) is linear-transformation of V, W;

        hence thesis;

      end;

    end

    begin

    definition

      let K be Ring;

      :: VECTSP12:def3

      mode VectorSpace-Sequence of K -> non empty FinSequence means

      : Def3: for S be set st S in ( rng it ) holds S is VectSp of K;

      existence

      proof

        set S = the VectSp of K;

        take <*S*>;

        let x be set;

        assume that

         A1: x in ( rng <*S*>) and

         A2: not x is VectSp of K;

        x in {S} by A1, FINSEQ_1: 38;

        hence contradiction by A2, TARSKI:def 1;

      end;

    end

    registration

      let K be Ring;

      cluster -> AbGroup-yielding for VectorSpace-Sequence of K;

      coherence

      proof

        let F be VectorSpace-Sequence of K;

        for x be set st x in ( rng F) holds x is AbGroup by Def3;

        hence thesis by PRVECT_1:def 10;

      end;

    end

    definition

      let K be Ring;

      let G be VectorSpace-Sequence of K;

      let j be Element of ( dom G);

      :: original: .

      redefine

      func G . j -> VectSp of K ;

      coherence

      proof

        (G . j) in ( rng G) by FUNCT_1:def 3;

        hence thesis by Def3;

      end;

    end

    definition

      let K be Ring, G be VectorSpace-Sequence of K, j be Element of ( dom ( carr G));

      :: original: .

      redefine

      func G . j -> VectSp of K ;

      coherence

      proof

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

        then

        reconsider j9 = j as Element of ( dom G) by PRVECT_1:def 11;

        (G . j9) is VectSp of K;

        hence thesis;

      end;

    end

    definition

      let K be Ring, G be VectorSpace-Sequence of K;

      :: VECTSP12:def4

      func multop G -> MultOps of the carrier of K, ( carr G) means

      : Def8: ( len it ) = ( len ( carr G)) & for j be Element of ( dom ( carr G)) holds (it . j) = the lmult of (G . j);

      existence

      proof

        deffunc F( Element of ( dom ( carr G))) = the lmult of (G . $1);

        consider p be non empty FinSequence such that

         A20: ( len p) = ( len ( carr G)) & for j be Element of ( dom ( carr G)) holds (p . j) = F(j) from PRVECT_1:sch 1;

        now

          let ai be set;

          assume ai in ( dom ( carr G));

          then

          reconsider i = ai as Element of ( dom ( carr G));

          ( len G) = ( len ( carr G)) by PRVECT_1:def 11;

          then

          reconsider j = i as Element of ( dom G) by FINSEQ_3: 29;

          (p . i) = the lmult of (G . i) & the carrier of (G . j) = (( carr G) . j) by A20, PRVECT_1:def 11;

          hence (p . ai) is Function of [:the carrier of K, (( carr G) . ai):], (( carr G) . ai);

        end;

        then

        reconsider p9 = p as MultOps of the carrier of K, ( carr G) by A20, PRVECT_2: 4;

        take p9;

        thus thesis by A20;

      end;

      uniqueness

      proof

        let f,h be MultOps of the carrier of K, ( carr G);

        assume that

         A21: ( len f) = ( len ( carr G)) and

         A22: for j be Element of ( dom ( carr G)) holds (f . j) = the lmult of (G . j) and

         A23: ( len h) = ( len ( carr G)) and

         A24: for j be Element of ( dom ( carr G)) holds (h . j) = the lmult of (G . j);

        reconsider f9 = f, h9 = h as FinSequence;

         A25:

        now

          let i be Nat;

          assume i in ( dom f9);

          then

          reconsider i9 = i as Element of ( dom ( carr G)) by A21, FINSEQ_3: 29;

          (f9 . i) = the lmult of (G . i9) by A22;

          hence (f9 . i) = (h9 . i) by A24;

        end;

        ( dom f9) = ( Seg ( len f9)) & ( dom h9) = ( Seg ( len h9)) by FINSEQ_1:def 3;

        hence thesis by A21, A23, A25, FINSEQ_1: 13;

      end;

    end

    definition

      let K be Ring, G be VectorSpace-Sequence of K;

      :: VECTSP12:def5

      func product G -> strict non empty ModuleStr over K equals ModuleStr (# ( product ( carr G)), [:( addop G):], ( zeros G), [:( multop G):] #);

      coherence ;

    end

    

     Lm3: for K be Ring, G be VectorSpace-Sequence of K holds for v1,w1 be Element of ( product ( carr G)), i be Element of ( dom ( carr G)) holds (( [:( addop G):] . (v1,w1)) . i) = (the addF of (G . i) . ((v1 . i),(w1 . i))) & for vi,wi be Vector of (G . i) st vi = (v1 . i) & wi = (w1 . i) holds (( [:( addop G):] . (v1,w1)) . i) = (vi + wi)

    proof

      let K be Ring, G be VectorSpace-Sequence of K;

      let v1,w1 be Element of ( product ( carr G));

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

      (( [:( addop G):] . (v1,w1)) . i) = ((( addop G) . i) . ((v1 . i),(w1 . i))) by PRVECT_1:def 8;

      hence thesis by PRVECT_1:def 12;

    end;

    

     Lm4: for K be Ring, G be VectorSpace-Sequence of K, r be Element of K, v be Element of ( product ( carr G)), i be Element of ( dom ( carr G)) holds (( [:( multop G):] . (r,v)) . i) = (the lmult of (G . i) . (r,(v . i))) & for vi be Vector of (G . i) st vi = (v . i) holds (( [:( multop G):] . (r,v)) . i) = (r * vi)

    proof

      let K be Ring, G be VectorSpace-Sequence of K;

      let r be Element of K, v be Element of ( product ( carr G));

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

      (( [:( multop G):] . (r,v)) . i) = ((( multop G) . i) . (r,(v . i))) by PRVECT_2:def 2;

      hence thesis by Def8;

    end;

    

     Lm5: for K be Ring, G be VectorSpace-Sequence of K holds ( product G) is vector-distributive scalar-distributive scalar-associative scalar-unital

    proof

      let K be Ring, G be VectorSpace-Sequence of K;

      deffunc ad( addLoopStr) = the addF of $1;

      reconsider GS = ModuleStr (# ( product ( carr G)), [:( addop G):], ( zeros G), [:( multop G):] #) as non empty ModuleStr over K;

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

      then ( dom G) = ( Seg ( len ( carr G))) by PRVECT_1:def 11;

      then

       A1: ( dom G) = ( dom ( carr G)) by FINSEQ_1:def 3;

      now

        let a,b be Element of K;

        let v,w be Vector of GS;

        reconsider v1 = v, w1 = w as Element of ( product ( carr G));

         A2:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

          reconsider i = x as Element of ( dom ( carr G));

          reconsider vi = (v1 . i) as Vector of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . (( 1. K),v1)) . x) = (( 1. K) * vi) by Lm4;

          hence (( [:( multop G):] . (( 1. K),v1)) . x) = (v1 . x) by VECTSP_1:def 17;

        end;

         A3:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

          reconsider i = x as Element of ( dom ( carr G));

          reconsider vi = (v1 . i) as Vector of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . ((a + b),v1)) . i) = ((a + b) * vi) by Lm4

          .= ((a * vi) + (b * vi)) by VECTSP_1:def 15

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(b * vi))) by Lm4

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(( [:( multop G):] . (b,v1)) . i))) by Lm4;

          hence (( [:( multop G):] . ((a + b),v1)) . x) = (( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (b,v1)))) . x) by Lm3;

        end;

         A4:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

          reconsider i = x as Element of ( dom ( carr G));

          reconsider vi = (v1 . i), wi = (w1 . i) as Vector of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . (a,( [:( addop G):] . (v1,w1)))) . i) = (the lmult of (G . i) . (a,(( [:( addop G):] . (v1,w1)) . i))) by Lm4

          .= (a * (vi + wi)) by Lm3

          .= ((a * vi) + (a * wi)) by VECTSP_1:def 14

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(a * wi))) by Lm4

          .= ( ad(.) . ((( [:( multop G):] . (a,v1)) . i),(( [:( multop G):] . (a,w1)) . i))) by Lm4;

          hence (( [:( multop G):] . (a,( [:( addop G):] . (v1,w1)))) . x) = (( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (a,w1)))) . x) by Lm3;

        end;

        ( dom ( [:( multop G):] . (a,( [:( addop G):] . (v1,w1))))) = ( dom ( carr G)) & ( dom ( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (a,w1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence (a * (v + w)) = ((a * v) + (a * w)) by A4, FUNCT_1: 2;

         A5:

        now

          let x be object;

          assume x in ( dom ( carr G));

          then

          reconsider i = x as Element of ( dom ( carr G));

          reconsider vi = (v1 . i) as Vector of (G . i) by A1, PRVECT_1:def 11;

          (( [:( multop G):] . ((a * b),v1)) . i) = ((a * b) * vi) by Lm4

          .= (a * (b * vi)) by VECTSP_1:def 16

          .= (the lmult of (G . i) . (a,(( [:( multop G):] . (b,v1)) . i))) by Lm4;

          hence (( [:( multop G):] . ((a * b),v1)) . x) = (( [:( multop G):] . (a,( [:( multop G):] . (b,v1)))) . x) by Lm4;

        end;

        ( dom ( [:( multop G):] . ((a + b),v1))) = ( dom ( carr G)) & ( dom ( [:( addop G):] . (( [:( multop G):] . (a,v1)),( [:( multop G):] . (b,v1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence ((a + b) * v) = ((a * v) + (b * v)) by A3, FUNCT_1: 2;

        ( dom ( [:( multop G):] . ((a * b),v1))) = ( dom ( carr G)) & ( dom ( [:( multop G):] . (a,( [:( multop G):] . (b,v1))))) = ( dom ( carr G)) by CARD_3: 9;

        hence ((a * b) * v) = (a * (b * v)) by A5, FUNCT_1: 2;

        ( dom ( [:( multop G):] . (( 1. K),v1))) = ( dom ( carr G)) & ( dom v1) = ( dom ( carr G)) by CARD_3: 9;

        hence (( 1. K) * v) = v by A2, FUNCT_1: 2;

      end;

      hence thesis;

    end;

    registration

      let K be Ring, G be VectorSpace-Sequence of K;

      cluster ( product G) -> Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital;

      coherence

      proof

        deffunc zr( addLoopStr) = the ZeroF of $1;

        reconsider GS = ModuleStr (# ( product ( carr G)), [:( addop G):], ( zeros G), [:( multop G):] #) as non empty ModuleStr over K;

        deffunc car( 1-sorted) = the carrier of $1;

        deffunc ad( addLoopStr) = the addF of $1;

         A1:

        now

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

          ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3

          .= ( Seg ( len ( carr G))) by PRVECT_1:def 11

          .= ( dom ( carr G)) by FINSEQ_1:def 3;

          hence (( carr G) . i) = car(.) by PRVECT_1:def 11;

        end;

        now

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

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( addop G) . i) is associative by FVSUM_1: 2;

        end;

        then

         A2: [:( addop G):] is associative by PRVECT_1: 18;

        now

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

          

           A3: (( zeros G) . i) = ( 0. (G . i)) by PRVECT_1:def 14;

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( zeros G) . i) is_a_unity_wrt (( addop G) . i) by A3, PRVECT_1: 1;

        end;

        then

         A4: ( zeros G) is_a_unity_wrt [:( addop G):] by PRVECT_1: 19;

        

         A5: GS is right_complementable

        proof

          let x be Element of GS;

          reconsider y = (( Frege ( complop G)) . x) as Element of GS by FUNCT_2: 5;

          take y;

          now

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

            

             A6: ( 0. (G . i)) = zr(.);

            

             A7: (( complop G) . i) = ( comp (G . i)) by PRVECT_1:def 13;

            (( carr G) . i) = car(.) & (( addop G) . i) = ad(.) by A1, PRVECT_1:def 12;

            hence (( complop G) . i) is_an_inverseOp_wrt (( addop G) . i) & (( addop G) . i) is having_a_unity by A6, A7, PRVECT_1: 1, PRVECT_1: 2, SETWISEO:def 2;

          end;

          then ( Frege ( complop G)) is_an_inverseOp_wrt [:( addop G):] by PRVECT_1: 20;

          then ( [:( addop G):] . (x,y)) = ( the_unity_wrt [:( addop G):]) by FINSEQOP:def 1;

          hence thesis by A4, BINOP_1:def 8;

        end;

        now

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

          (( addop G) . i) = ad(.) & (( carr G) . i) = car(.) by A1, PRVECT_1:def 12;

          hence (( addop G) . i) is commutative by FVSUM_1: 1;

        end;

        then [:( addop G):] is commutative by PRVECT_1: 17;

        hence thesis by A2, A4, A5, Lm5, BINOP_1: 3;

      end;

    end

    begin

    reserve K for Ring;

    definition

      let K be Ring, G,F be non empty ModuleStr over K;

      :: VECTSP12:def6

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

      : YDef2: for r be Element of K, g be Vector of G, f be Vector of F holds (it . (r, [g, f])) = [(r * g), (r * f)];

      existence

      proof

        defpred MLT[ object, object, object] means ex r be Element of the carrier of K, g be Vector of G, f be Vector 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 the carrier of K & 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 the carrier of K & y in [:CarrG, CarrF:];

          then

          reconsider r = x as Element of the carrier of K;

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

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

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

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

          hence thesis;

        end;

        consider MLTGF be Function of [:the carrier of K, [:CarrG, CarrF:]:], [:CarrG, CarrF:] such that

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

        now

          let r be Element of K, g be Vector of G, f be Vector of F;

           MLT[r, [g, f], (MLTGF . (r, [g, f]))] by A4, ZFMISC_1: 87;

          then

          consider rr be Element of the carrier of K, gg be Vector of G, ff be Vector 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 [:the carrier of K, [:the carrier of G, the carrier of F:]:], [:the carrier of G, the carrier of F:];

        assume

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

        assume

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

        now

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

           [:the carrier of G, the carrier of F:] <> {} by ZFMISC_1: 90;

          then

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

           A8: x = [x1, x2] by SUBSET_1: 43;

          

          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 K be Ring;

      let G,F be non empty ModuleStr over K;

      :: VECTSP12:def7

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

      correctness

      proof

         [:the carrier of G, the carrier of F:] <> {} by ZFMISC_1: 90;

        hence thesis;

      end;

    end

    registration

      let K be Ring;

      let G,F be Abelian non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

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

         A2: y = [y1, y2] by SUBSET_1: 43;

        (x + y) = [(x1 + y1), (x2 + y2)] by A1, A2, PRVECT_3:def 1;

        hence (x + y) = (y + x) by A1, A2, PRVECT_3:def 1;

      end;

    end

    registration

      let K be Ring;

      let G,F be add-associative non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

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

         A2: y = [y1, y2] by SUBSET_1: 43;

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

         A3: z = [z1, z2] by SUBSET_1: 43;

        

         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, PRVECT_3:def 1

        .= [(x1 + (y1 + z1)), (x2 + (y2 + z2))] by A4, PRVECT_3:def 1

        .= (( prod_ADD (G,F)) . ( [x1, x2], [(y1 + z1), (y2 + z2)])) by PRVECT_3:def 1

        .= (x + (y + z)) by A1, A2, A3, PRVECT_3:def 1;

      end;

    end

    registration

      let K be Ring;

      let G,F be right_zeroed non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

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

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

      end;

    end

    registration

      let K be Ring;

      let G,F be right_complementable non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

        consider y1 be Vector of G such that

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

        consider y2 be Vector of F such that

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

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

        take y;

        thus thesis by A1, A2, A3, PRVECT_3:def 1;

      end;

    end

    theorem :: VECTSP12:13

    for G,F be non empty ModuleStr over K holds (for x be set holds (x is Vector of [:G, F:] iff ex x1 be Vector of G, x2 be Vector of F st x = [x1, x2])) & (for x,y be Vector of [:G, F:], x1,y1 be Vector of G, x2,y2 be Vector 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 Vector of [:G, F:], x1 be Vector of G, x2 be Vector of F, a be Element of K st x = [x1, x2] holds (a * x) = [(a * x1), (a * x2)]) by YDef2, PRVECT_3:def 1, SUBSET_1: 43, ZFMISC_1: 87;

    theorem :: VECTSP12:14

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

    proof

      let G,F be add-associative right_zeroed right_complementable non empty ModuleStr over K;

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

      assume

       A1: x = [x1, x2];

      reconsider y = [( - x1), ( - x2)] as Vector of [:G, F:] by ZFMISC_1: 87;

      (x + y) = [(x1 + ( - x1)), (x2 + ( - x2))] by A1, PRVECT_3:def 1

      .= [( 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 K be Ring;

      let G,F be vector-distributive non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

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

         A2: y = [y1, y2] by SUBSET_1: 43;

        

         A3: (a * (x1 + y1)) = ((a * x1) + (a * y1)) & (a * (x2 + y2)) = ((a * x2) + (a * y2)) by VECTSP_1:def 14;

        

        thus (a * (x + y)) = (( prod_MLT (G,F)) . (a, [(x1 + y1), (x2 + y2)])) by A1, A2, PRVECT_3:def 1

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

        .= (( prod_ADD (G,F)) . ( [(a * x1), (a * x2)], [(a * y1), (a * y2)])) by A3, PRVECT_3:def 1

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

        .= ((a * x) + (a * y)) by A1, A2, YDef2;

      end;

    end

    registration

      let K be Ring;

      let G,F be scalar-distributive non empty ModuleStr over K;

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

      correctness

      proof

        let a,b be Element of K, x be Vector of [:G, F:];

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

         A1: x = [x1, x2] by SUBSET_1: 43;

        

         A2: ((a + b) * x1) = ((a * x1) + (b * x1)) & ((a + b) * x2) = ((a * x2) + (b * x2)) by VECTSP_1:def 15;

        

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

        .= (( prod_ADD (G,F)) . ( [(a * x1), (a * x2)], [(b * x1), (b * x2)])) by A2, PRVECT_3:def 1

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

        .= ((a * x) + (b * x)) by A1, YDef2;

      end;

    end

    registration

      let K be Ring;

      let G,F be scalar-associative non empty ModuleStr over K;

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

      correctness

      proof

        let a,b be Element of K, x be Vector of [:G, F:];

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

         A1: x = [x1, x2] by SUBSET_1: 43;

        

         A2: ((a * b) * x1) = (a * (b * x1)) & ((a * b) * x2) = (a * (b * x2)) by VECTSP_1:def 16;

        

        thus ((a * b) * x) = [((a * b) * x1), ((a * b) * x2)] by A1, YDef2

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

        .= (a * (b * x)) by A1, YDef2;

      end;

    end

    registration

      let K be Ring;

      let G,F be scalar-unital non empty ModuleStr over K;

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

      correctness

      proof

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

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

         A1: x = [x1, x2] by SUBSET_1: 43;

        (( 1. K) * x1) = x1 & (( 1. K) * x2) = x2 by VECTSP_1:def 17;

        hence (( 1. K) * x) = x by A1, YDef2;

      end;

    end

    definition

      let K be Ring;

      let G be VectSp of K;

      :: original: <*

      redefine

      func <*G*> -> VectorSpace-Sequence of K ;

      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 VectSp of K by A1, FINSEQ_1: 40;

      end;

    end

    definition

      let K be Ring;

      let G,F be VectSp of K;

      :: original: <*

      redefine

      func <*G,F*> -> VectorSpace-Sequence of K ;

      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 VectSp of K by A1, FINSEQ_1: 44;

      end;

    end

    theorem :: VECTSP12:15

    for X be VectSp of K holds ex I be Function of X, ( product <*X*>) st I is one-to-one onto & (for x be Vector of X holds (I . x) = <*x*>) & (for v,w be Vector of X holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Vector of X, r be Element of the carrier of K holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. X)) = ( 0. ( product <*X*>))

    proof

      let X be VectSp of K;

      set CarrX = the carrier of X;

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

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

      ( 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 Vector of X holds (I . x) = <*x*> by A1;

      

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

      proof

        let v,w be Vector 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 Vector of X, r be Element of the carrier of K holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Vector of X, r be Element of the carrier of K;

        

         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 lmult of ( <*X*> . j1) by Def8;

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

      hence thesis by A1, A6, A5, A7, A14, RLVECT_1: 15;

    end;

    definition

      let K be Ring;

      let G,F be VectorSpace-Sequence of K;

      :: original: ^

      redefine

      func G ^ F -> VectorSpace-Sequence of K ;

      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 VectSp of K by A3, A1, Def3;

        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 VectSp of K by A5, A1, Def3;

        end;

      end;

    end

    theorem :: VECTSP12:16

    

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

    proof

      let X,Y be VectSp of K;

      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 onto & for x,y be object st x in CarrX & y in CarrY holds (I . (x,y)) = <*x, y*> by PRVECT_3: 5;

      ( 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 Vector of X, y be Vector of Y holds (I . (x,y)) = <*x, y*> by A1;

      

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

      proof

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

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

         A9: v = [x1, y1] by SUBSET_1: 43;

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

         A10: w = [x2, y2] by SUBSET_1: 43;

        (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, PRVECT_3:def 1

        .= <*(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 Vector of [:X, Y:], r be Element of K holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Vector of [:X, Y:], r be Element of K;

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

         A21: v = [x1, y1] by SUBSET_1: 43;

        

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

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

        

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

        .= <*(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 lmult of ( <*X, Y*> . j1) & (( multop <*X, Y*>) . j2) = the lmult of ( <*X, Y*> . j2) by Def8;

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

        reconsider rr = r as Element of the carrier of K;

        (( [:( 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:]));

      hence thesis by A7, A8, A20, A1, A6, RLVECT_1: 15;

    end;

    theorem :: VECTSP12:17

    for X,Y be VectorSpace-Sequence of K holds ex I be Function of [:( product X), ( product Y):], ( product (X ^ Y)) st I is one-to-one onto & (for x be Vector of ( product X), y be Vector of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1)) & (for v,w be Vector of [:( product X), ( product Y):] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Vector of [:( product X), ( product Y):], r be Element of the carrier of K holds (I . (r * v)) = (r * (I . v))) & (I . ( 0. [:( product X), ( product Y):])) = ( 0. ( product (X ^ Y)))

    proof

      let X,Y be VectorSpace-Sequence of K;

      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 onto & for x,y be FinSequence st x in ( product CX) & y in ( product CY) holds (I . (x,y)) = (x ^ y) by PRVECT_3: 6;

      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 Vector of ( product X), y be Vector of ( product Y) holds ex x1,y1 be FinSequence st x = x1 & y = y1 & (I . (x,y)) = (x1 ^ y1)

      proof

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

        reconsider x1 = x, y1 = y as FinSequence by NDIFF_5: 9;

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

        hence thesis;

      end;

      

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

      proof

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

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

         A15: v = [x1, y1] by SUBSET_1: 43;

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

         A16: w = [x2, y2] by SUBSET_1: 43;

        reconsider xx1 = x1, xx2 = x2 as FinSequence by NDIFF_5: 9;

        reconsider yy1 = y1, yy2 = y2 as FinSequence by NDIFF_5: 9;

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

        

         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, PRVECT_3:def 1;

        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 NDIFF_5: 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, CARD_3: 9, FINSEQ_1: 13;

      end;

      

       A32: for v be Vector of [:PX, PY:], r be Element of the carrier of K holds (I . (r * v)) = (r * (I . v))

      proof

        let v be Vector of [:PX, PY:], r be Element of the carrier of K;

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

         A33: v = [x1, y1] by SUBSET_1: 43;

        reconsider xx1 = x1, yy1 = y1 as FinSequence by NDIFF_5: 9;

        reconsider rxx1 = (r * x1), ryy1 = (r * y1) as FinSequence by NDIFF_5: 9;

        

         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, YDef2

        .= (rxx1 ^ ryy1) by A2;

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

        reconsider rIv = (r * (I . v)) as FinSequence by NDIFF_5: 9;

        

         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 lmult of ((X ^ Y) . j) . (r,(Iv . j))) by Def8;

          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 lmult of ((X ^ Y) . j) . (r,(Iv . j))) = ((( multop X) . j1) . (r,(xx1 . j1))) by A42, A43, Def8

            .= ((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 lmult of ((X ^ Y) . j) . (r,(Iv . j))) = ((( multop Y) . j1) . (r,(yy1 . j1))) by A47, A48, Def8

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

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

          end;

        end;

        hence thesis by A36, A38, CARD_3: 9, 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:]));

      hence thesis by A13, A14, A32, A2, A12, RLVECT_1: 15;

    end;

    theorem :: VECTSP12:18

    for G,F be VectSp of K holds (for x be set holds (x is Vector of ( product <*G, F*>) iff ex x1 be Vector of G, x2 be Vector of F st x = <*x1, x2*>)) & (for x,y be Vector of ( product <*G, F*>), x1,y1 be Vector of G, x2,y2 be Vector 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 Vector of ( product <*G, F*>), x1 be Vector of G, x2 be Vector of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>) & (for x be Vector of ( product <*G, F*>), x1 be Vector of G, x2 be Vector of F, a be Element of K st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>)

    proof

      let G,F be VectSp of K;

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

       A1: I is one-to-one onto & (for x be Vector of G, y be Vector of F holds (I . (x,y)) = <*x, y*>) & (for v,w be Vector of [:G, F:] holds (I . (v + w)) = ((I . v) + (I . w))) & (for v be Vector of [:G, F:], r be Element of K 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 Vector of ( product <*G, F*>) iff ex x1 be Vector of G, x2 be Vector of F st x = <*x1, x2*>)

      proof

        let y be set;

        hereby

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

          then

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

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

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

           A4: x = [x1, x2] by SUBSET_1: 43;

          take x1, x2;

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

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

        end;

        now

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

          then

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

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

           [x1, x2] in the carrier of [:G, F:] by ZFMISC_1: 87;

          then

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

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

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

        end;

        hence thesis;

      end;

      thus

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

      proof

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

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

        assume

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

        reconsider z = [x1, x2], w = [y1, y2] as Vector of [:G, F:] by ZFMISC_1: 87;

        

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

        (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 Vector of ( product <*G, F*>), x1 be Vector of G, x2 be Vector of F st x = <*x1, x2*> holds ( - x) = <*( - x1), ( - x2)*>

      proof

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

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

        assume

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

        reconsider y = <*( - x1), ( - x2)*> as Vector 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 Vector of ( product <*G, F*>), x1 be Vector of G, x2 be Vector of F, a be Element of K st x = <*x1, x2*> holds (a * x) = <*(a * x1), (a * x2)*>

      proof

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

        let x1 be Vector of G, x2 be Vector of F, a be Element of K;

        assume

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

        reconsider y = [x1, x2] as Vector of [:G, F:] by ZFMISC_1: 87;

        

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

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

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

        hence thesis by A1, A12, A13;

      end;

    end;