matrlin2.miz



    begin

    reserve i,j,m,n,k for Nat,

x,y for set,

K for Field,

a,a1 for Element of K;

    theorem :: MATRLIN2:1

    

     Th1: for V be VectSp of K holds for W1,W2,W12 be Subspace of V holds for U1,U2 be Subspace of W12 st U1 = W1 & U2 = W2 holds (W1 /\ W2) = (U1 /\ U2) & (W1 + W2) = (U1 + U2)

    proof

      let V be VectSp of K;

      let W1,W2,W12 be Subspace of V;

      let U1,U2 be Subspace of W12 such that

       A1: U1 = W1 and

       A2: U2 = W2;

      reconsider U12 = (U1 /\ U2) as Subspace of V by VECTSP_4: 26;

      

       A3: the carrier of U12 c= the carrier of (W1 /\ W2)

      proof

        let x be object;

        assume x in the carrier of U12;

        then x in (U1 /\ U2);

        then x in U1 & x in U2 by VECTSP_5: 3;

        then x in (W1 /\ W2) by A1, A2, VECTSP_5: 3;

        hence thesis;

      end;

      the carrier of (W1 /\ W2) c= the carrier of U12

      proof

        let x be object;

        assume x in the carrier of (W1 /\ W2);

        then x in (W1 /\ W2);

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

        then x in U12 by A1, A2, VECTSP_5: 3;

        hence thesis;

      end;

      then the carrier of (W1 /\ W2) = the carrier of U12 by A3, XBOOLE_0:def 10;

      hence (W1 /\ W2) = (U1 /\ U2) by VECTSP_4: 29;

      reconsider U12 = (U1 + U2) as Subspace of V by VECTSP_4: 26;

      

       A4: the carrier of (W1 + W2) c= the carrier of U12

      proof

        let x be object;

        assume x in the carrier of (W1 + W2);

        then x in (W1 + W2);

        then

        consider v1,v2 be Vector of V such that

         A5: v1 in W1 and

         A6: v2 in W2 and

         A7: (v1 + v2) = x by VECTSP_5: 1;

        U2 is Subspace of U12 by VECTSP_5: 7;

        then

         A8: v2 in U12 by A2, A6, VECTSP_4: 8;

        U1 is Subspace of U12 by VECTSP_5: 7;

        then v1 in U12 by A1, A5, VECTSP_4: 8;

        then

        reconsider w1 = v1, w2 = v2 as Vector of U12 by A8;

        (v1 + v2) = (w1 + w2) by VECTSP_4: 13;

        hence thesis by A7;

      end;

      the carrier of U12 c= the carrier of (W1 + W2)

      proof

        let x be object;

        assume x in the carrier of U12;

        then x in (U1 + U2);

        then

        consider v1,v2 be Vector of W12 such that

         A9: v1 in U1 & v2 in U2 & (v1 + v2) = x by VECTSP_5: 1;

        reconsider w1 = v1, w2 = v2 as Vector of V by VECTSP_4: 10;

        (v1 + v2) = (w1 + w2) by VECTSP_4: 13;

        then x in (W1 + W2) by A1, A2, A9, VECTSP_5: 1;

        hence thesis;

      end;

      then the carrier of (W1 + W2) = the carrier of U12 by A4, XBOOLE_0:def 10;

      hence thesis by VECTSP_4: 29;

    end;

    theorem :: MATRLIN2:2

    

     Th2: for V be VectSp of K holds for W1,W2 be Subspace of V st (W1 /\ W2) = ( (0). V) holds for B1 be linearly-independent Subset of W1, B2 be linearly-independent Subset of W2 holds (B1 \/ B2) is linearly-independent Subset of (W1 + W2)

    proof

      let V be VectSp of K;

      let W1,W2 be Subspace of V such that

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

      reconsider W19 = W1, W29 = W2 as Subspace of (W1 + W2) by VECTSP_5: 7;

      let B1 be linearly-independent Subset of W1;

      let B2 be linearly-independent Subset of W2;

      

       A2: W2 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then the carrier of W2 c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then

       A3: B2 c= the carrier of (W1 + W2);

      

       A4: W1 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then the carrier of W1 c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then B1 c= the carrier of (W1 + W2);

      then

      reconsider B12 = (B1 \/ B2), B19 = B1, B29 = B2 as Subset of (W1 + W2) by A3, XBOOLE_1: 8;

      B12 is linearly-independent

      proof

        let L be Linear_Combination of B12;

        assume ( Sum L) = ( 0. (W1 + W2));

        then

         A5: ( Sum L) = (( 0. (W1 + W2)) + ( 0. (W1 + W2))) by RLVECT_1:def 4;

        set C = (( Carrier L) /\ B1);

        defpred P[ object] means $1 in C;

        C c= ( Carrier L) by XBOOLE_1: 17;

        then

        reconsider C as finite Subset of (W1 + W2) by XBOOLE_1: 1;

        set D = (( Carrier L) \ B1);

        deffunc G( object) = (L . $1);

        defpred C[ object] means $1 in D;

        reconsider D as finite Subset of (W1 + W2);

        

         A6: D c= B29

        proof

          let x be object;

          assume x in D;

          then

           A7: x in ( Carrier L) & not x in B19 by XBOOLE_0:def 5;

          ( Carrier L) c= B12 by VECTSP_6:def 4;

          hence thesis by A7, XBOOLE_0:def 3;

        end;

        ( (0). V) = ( (0). (W1 + W2)) by VECTSP_4: 36;

        then

         A8: (W19 /\ W29) = ( (0). (W1 + W2)) by A1, Th1;

        (W19 + W29) = (W1 + W2) by Th1;

        then

         A9: (W1 + W2) is_the_direct_sum_of (W19,W29) by A8, VECTSP_5:def 4;

        

         A10: B29 is linearly-independent by A2, VECTSP_9: 11;

        

         A11: B19 is linearly-independent by A4, VECTSP_9: 11;

        deffunc F( object) = ( 0. K);

        

         A12: ( 0. W1) in W19 & ( 0. W2) in W29;

         A13:

        now

          let x be object;

          assume x in the carrier of (W1 + W2);

          then

          reconsider v = x as Vector of (W1 + W2);

          (L . v) in the carrier of K;

          hence P[x] implies G(x) in the carrier of K;

          assume not P[x];

          thus F(x) in the carrier of K;

        end;

        consider f be Function of the carrier of (W1 + W2), the carrier of K such that

         A14: for x be object st x in the carrier of (W1 + W2) holds ( P[x] implies (f . x) = G(x)) & ( not P[x] implies (f . x) = F(x)) from FUNCT_2:sch 5( A13);

        deffunc G( object) = (L . $1);

         A15:

        now

          let x be object;

          assume x in the carrier of (W1 + W2);

          then

          reconsider v = x as Vector of (W1 + W2);

          (L . v) in the carrier of K;

          hence C[x] implies G(x) in the carrier of K;

          assume not C[x];

          thus F(x) in the carrier of K;

        end;

        consider g be Function of the carrier of (W1 + W2), the carrier of K such that

         A16: for x be object st x in the carrier of (W1 + W2) holds ( C[x] implies (g . x) = G(x)) & ( not C[x] implies (g . x) = F(x)) from FUNCT_2:sch 5( A15);

        reconsider g as Element of ( Funcs (the carrier of (W1 + W2),the carrier of K)) by FUNCT_2: 8;

        for u be Vector of (W1 + W2) holds not u in D implies (g . u) = ( 0. K) by A16;

        then

        reconsider g as Linear_Combination of (W1 + W2) by VECTSP_6:def 1;

        

         A17: ( Carrier g) c= D

        proof

          let x be object;

          assume x in ( Carrier g);

          then

           A18: ex u be Vector of (W1 + W2) st x = u & (g . u) <> ( 0. K);

          assume not x in D;

          hence thesis by A16, A18;

        end;

        then ( Carrier g) c= B29 by A6;

        then

        reconsider g as Linear_Combination of B29 by VECTSP_6:def 4;

        reconsider f as Element of ( Funcs (the carrier of (W1 + W2),the carrier of K)) by FUNCT_2: 8;

        for u be Vector of (W1 + W2) holds not u in C implies (f . u) = ( 0. K) by A14;

        then

        reconsider f as Linear_Combination of (W1 + W2) by VECTSP_6:def 1;

        

         A19: ( Carrier f) c= B19

        proof

          let x be object;

          assume x in ( Carrier f);

          then

           A20: ex u be Vector of (W1 + W2) st x = u & (f . u) <> ( 0. K);

          assume not x in B19;

          then not x in C by XBOOLE_0:def 4;

          hence thesis by A14, A20;

        end;

        then

        reconsider f as Linear_Combination of B19 by VECTSP_6:def 4;

        ex f1 be Linear_Combination of W19 st ( Carrier f1) = ( Carrier f) & ( Sum f) = ( Sum f1) by A19, VECTSP_9: 9, XBOOLE_1: 1;

        then

         A21: ( Sum f) in W19;

        

         A22: L = (f + g)

        proof

          let v be Vector of (W1 + W2);

          now

            per cases ;

              suppose

               A23: v in C;

               A24:

              now

                assume v in D;

                then not v in B19 by XBOOLE_0:def 5;

                hence contradiction by A23, XBOOLE_0:def 4;

              end;

              

              thus ((f + g) . v) = ((f . v) + (g . v)) by VECTSP_6: 22

              .= ((L . v) + (g . v)) by A14, A23

              .= ((L . v) + ( 0. K)) by A16, A24

              .= (L . v) by RLVECT_1: 4;

            end;

              suppose

               A25: not v in C;

              now

                per cases ;

                  suppose

                   A26: v in ( Carrier L);

                   A27:

                  now

                    assume not v in D;

                    then not v in ( Carrier L) or v in B19 by XBOOLE_0:def 5;

                    hence contradiction by A25, A26, XBOOLE_0:def 4;

                  end;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by VECTSP_6: 22

                  .= ((g . v) + ( 0. K)) by A14, A25

                  .= (g . v) by RLVECT_1: 4

                  .= (L . v) by A16, A27;

                end;

                  suppose

                   A28: not v in ( Carrier L);

                  then

                   A29: not v in D by XBOOLE_0:def 5;

                  

                   A30: not v in C by A28, XBOOLE_0:def 4;

                  

                  thus ((f + g) . v) = ((f . v) + (g . v)) by VECTSP_6: 22

                  .= (( 0. K) + (g . v)) by A14, A30

                  .= (( 0. K) + ( 0. K)) by A16, A29

                  .= ( 0. K) by RLVECT_1: 4

                  .= (L . v) by A28;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        then

         A31: ( Sum L) = (( Sum f) + ( Sum g)) by VECTSP_6: 44;

        ( Carrier g) c= B2 by A17, A6;

        then ex g1 be Linear_Combination of W29 st ( Carrier g1) = ( Carrier g) & ( Sum g) = ( Sum g1) by VECTSP_9: 9, XBOOLE_1: 1;

        then

         A32: ( Sum g) in W29;

        

         A33: ( 0. (W1 + W2)) = ( 0. W19) & ( 0. (W1 + W2)) = ( 0. W29) by VECTSP_4: 11;

        then ( Sum f) = ( 0. (W1 + W2)) by A31, A21, A32, A9, A12, A5, VECTSP_5: 48;

        then

         A34: ( Carrier f) = {} by A11;

        ( Sum g) = ( 0. (W1 + W2)) by A31, A21, A32, A9, A33, A12, A5, VECTSP_5: 48;

        then

         A35: ( Carrier g) = {} by A10;

        ( {} \/ {} ) = {} ;

        hence thesis by A22, A34, A35, VECTSP_6: 23, XBOOLE_1: 3;

      end;

      hence thesis;

    end;

    theorem :: MATRLIN2:3

    

     Th3: for V be VectSp of K holds for W1,W2 be Subspace of V st (W1 /\ W2) = ( (0). V) holds for B1 be Basis of W1, B2 be Basis of W2 holds (B1 \/ B2) is Basis of (W1 + W2)

    proof

      let V be VectSp of K;

      let W1,W2 be Subspace of V such that

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

      let B1 be Basis of W1, B2 be Basis of W2;

      

       A2: W2 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then the carrier of W2 c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then

       A3: B2 c= the carrier of (W1 + W2);

      

       A4: W1 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then the carrier of W1 c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then B1 c= the carrier of (W1 + W2);

      then

      reconsider B12 = (B1 \/ B2), B19 = B1, B29 = B2 as Subset of (W1 + W2) by A3, XBOOLE_1: 8;

      

       A5: ( (Omega). W2) = ( Lin B2) by VECTSP_7:def 3

      .= ( Lin B29) by A2, VECTSP_9: 17;

      

       A6: ( Lin B12) = (( Lin B19) + ( Lin B29)) by VECTSP_7: 15;

      

       A7: ( (Omega). W1) = ( Lin B1) by VECTSP_7:def 3

      .= ( Lin B19) by A4, VECTSP_9: 17;

      

       A8: the carrier of (W1 + W2) c= the carrier of ( Lin B12)

      proof

        let x be object such that

         A9: x in the carrier of (W1 + W2);

        reconsider x as Vector of (W1 + W2) by A9;

        x in (W1 + W2);

        then

        consider v1,v2 be Vector of V such that

         A10: v1 in W1 and

         A11: v2 in W2 and

         A12: x = (v1 + v2) by VECTSP_5: 1;

        v1 is Vector of W1 & v2 is Vector of W2 by A10, A11;

        then

        reconsider w1 = v1, w2 = v2 as Vector of (W1 + W2) by A4, A2, VECTSP_4: 10;

        

         A13: (v1 + v2) = (w1 + w2) by VECTSP_4: 13;

        v2 in the carrier of ( Lin B29) by A5, A11;

        then

         A14: v2 in ( Lin B29);

        v1 in the carrier of ( Lin B19) by A7, A10;

        then v1 in ( Lin B19);

        then (w1 + w2) in ( Lin B12) by A6, A14, VECTSP_5: 1;

        hence thesis by A12, A13;

      end;

      the carrier of ( Lin B12) c= the carrier of (W1 + W2) by VECTSP_4:def 2;

      then the carrier of ( Lin B12) = the carrier of (W1 + W2) by A8, XBOOLE_0:def 10;

      then

       A15: ( Lin B12) = the ModuleStr of (W1 + W2) by VECTSP_4: 31;

      B2 is linearly-independent & B1 is linearly-independent by VECTSP_7:def 3;

      then (B1 \/ B2) is linearly-independent Subset of (W1 + W2) by A1, Th2;

      hence thesis by A15, VECTSP_7:def 3;

    end;

    theorem :: MATRLIN2:4

    for V be finite-dimensional VectSp of K, B be OrdBasis of ( (Omega). V) holds B is OrdBasis of V

    proof

      let V be finite-dimensional VectSp of K, B be OrdBasis of ( (Omega). V);

      reconsider r = ( rng B) as Basis of ( (Omega). V) by MATRLIN:def 2;

      r is linearly-independent by VECTSP_7:def 3;

      then

      reconsider R = r as linearly-independent Subset of V by VECTSP_9: 11;

      ( Lin R) = ( Lin r) by VECTSP_9: 17

      .= the ModuleStr of V by VECTSP_7:def 3;

      then

       A1: R is Basis of V by VECTSP_7:def 3;

      B is one-to-one by MATRLIN:def 2;

      hence thesis by A1, MATRLIN:def 2;

    end;

    theorem :: MATRLIN2:5

    for V1 be VectSp of K holds for A be finite Subset of V1 st ( dim ( Lin A)) = ( card A) holds A is linearly-independent

    proof

      let V1 be VectSp of K;

      let A be finite Subset of V1 such that

       A1: ( dim ( Lin A)) = ( card A);

      set L = ( Lin A);

      A c= the carrier of L

      proof

        let x be object;

        assume x in A;

        then x in L by VECTSP_7: 8;

        hence thesis;

      end;

      then

      reconsider A9 = A as Subset of L;

      ( Lin A9) = L by VECTSP_9: 17;

      then

      consider B be Subset of L such that

       A2: B c= A9 and

       A3: B is linearly-independent and

       A4: ( Lin B) = L by VECTSP_7: 18;

      reconsider B as finite Subset of L by A2;

      B is Basis of L by A3, A4, VECTSP_7:def 3;

      then

      reconsider L as finite-dimensional VectSp of K by MATRLIN:def 1;

      ( card A) = ( dim L) by A1

      .= ( card B) by A3, A4, VECTSP_9: 26;

      then A = B by A2, CARD_2: 102;

      hence thesis by A3, VECTSP_9: 11;

    end;

    theorem :: MATRLIN2:6

    for V be VectSp of K holds for A be finite Subset of V holds ( dim ( Lin A)) <= ( card A)

    proof

      let V be VectSp of K;

      let A be finite Subset of V;

      set L = ( Lin A);

      A c= the carrier of L

      proof

        let x be object;

        assume x in A;

        then x in L by VECTSP_7: 8;

        hence thesis;

      end;

      then

      reconsider A9 = A as Subset of L;

      ( Lin A9) = L by VECTSP_9: 17;

      then

      consider B be Subset of L such that

       A1: B c= A9 and

       A2: B is linearly-independent & ( Lin B) = L by VECTSP_7: 18;

      reconsider B as finite Subset of L by A1;

      B is Basis of L by A2, VECTSP_7:def 3;

      then

      reconsider L as finite-dimensional VectSp of K by MATRLIN:def 1;

      ( card B) = ( dim L) & ( Segm ( card B)) c= ( Segm ( card A)) by A1, A2, CARD_1: 11, VECTSP_9: 26;

      hence thesis by NAT_1: 39;

    end;

    begin

    reserve V1,V2,V3 for finite-dimensional VectSp of K,

f for Function of V1, V2,

b1,b19 for OrdBasis of V1,

B1 for FinSequence of V1,

b2 for OrdBasis of V2,

B2 for FinSequence of V2,

B3 for FinSequence of V3,

v1,w1 for Element of V1,

R,R1,R2 for FinSequence of V1,

p,p1,p2 for FinSequence of K;

    

     Lm1: ( dom ( lmlt (p,R))) = (( dom p) /\ ( dom R))

    proof

      ( rng p) c= the carrier of K & ( rng R) c= the carrier of V1 by FINSEQ_1:def 4;

      then [:( rng p), ( rng R):] c= [:the carrier of K, the carrier of V1:] by ZFMISC_1: 96;

      then [:( rng p), ( rng R):] c= ( dom the lmult of V1) by FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 69;

    end;

    

     Lm2: ( dom (p1 + p2)) = (( dom p1) /\ ( dom p2))

    proof

      ( rng p1) c= the carrier of K & ( rng p2) c= the carrier of K by FINSEQ_1:def 4;

      then [:( rng p1), ( rng p2):] c= [:the carrier of K, the carrier of K:] by ZFMISC_1: 96;

      then [:( rng p1), ( rng p2):] c= ( dom the addF of K) by FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 69;

    end;

    

     Lm3: ( dom (R1 + R2)) = (( dom R1) /\ ( dom R2))

    proof

      ( rng R1) c= the carrier of V1 & ( rng R2) c= the carrier of V1 by FINSEQ_1:def 4;

      then [:( rng R1), ( rng R2):] c= [:the carrier of V1, the carrier of V1:] by ZFMISC_1: 96;

      then [:( rng R1), ( rng R2):] c= ( dom the addF of V1) by FUNCT_2:def 1;

      hence thesis by FUNCOP_1: 69;

    end;

    theorem :: MATRLIN2:7

    

     Th7: ( lmlt ((p1 + p2),R)) = (( lmlt (p1,R)) + ( lmlt (p2,R)))

    proof

      set L12 = ( lmlt ((p1 + p2),R));

      set L1 = ( lmlt (p1,R));

      set L2 = ( lmlt (p2,R));

      

       A1: ( dom (L1 + L2)) = (( dom L1) /\ ( dom L2)) by Lm3;

      

       A2: ( dom L12) = (( dom (p1 + p2)) /\ ( dom R)) by Lm1;

      

       A3: ( dom L1) = (( dom p1) /\ ( dom R)) by Lm1;

      

       A4: ( dom L2) = (( dom p2) /\ ( dom R)) by Lm1;

      

      then

       A5: ( dom (L1 + L2)) = (((( dom p1) /\ ( dom R)) /\ ( dom p2)) /\ ( dom R)) by A1, A3, XBOOLE_1: 16

      .= (((( dom p1) /\ ( dom p2)) /\ ( dom R)) /\ ( dom R)) by XBOOLE_1: 16

      .= ((( dom p1) /\ ( dom p2)) /\ (( dom R) /\ ( dom R))) by XBOOLE_1: 16

      .= ( dom L12) by A2, Lm2;

      now

        let x be object such that

         A6: x in ( dom (L1 + L2));

        

         A7: x in ( dom L2) by A1, A6, XBOOLE_0:def 4;

        then

         A8: (L2 /. x) = (L2 . x) by PARTFUN1:def 6;

        x in ( dom p2) by A4, A7, XBOOLE_0:def 4;

        then

         A9: (p2 /. x) = (p2 . x) by PARTFUN1:def 6;

        

         A10: x in ( dom (p1 + p2)) by A2, A5, A6, XBOOLE_0:def 4;

        then

         A11: ((p1 + p2) . x) = ((p1 + p2) /. x) by PARTFUN1:def 6;

        

         A12: x in ( dom L1) by A1, A6, XBOOLE_0:def 4;

        then x in ( dom p1) by A3, XBOOLE_0:def 4;

        then

         A13: (p1 /. x) = (p1 . x) by PARTFUN1:def 6;

        x in ( dom R) by A3, A12, XBOOLE_0:def 4;

        then

         A14: (R /. x) = (R . x) by PARTFUN1:def 6;

        

         A15: (L1 /. x) = (L1 . x) by A12, PARTFUN1:def 6;

        

        hence ((L1 + L2) . x) = ((L1 /. x) + (L2 /. x)) by A6, A8, FVSUM_1: 17

        .= ((the lmult of V1 . ((p1 /. x),(R /. x))) + (L2 /. x)) by A12, A15, A13, A14, FUNCOP_1: 22

        .= (((p1 /. x) * (R /. x)) + ((p2 /. x) * (R /. x))) by A7, A8, A9, A14, FUNCOP_1: 22

        .= (((p1 /. x) + (p2 /. x)) * (R /. x)) by VECTSP_1:def 15

        .= (((p1 + p2) /. x) * (R /. x)) by A10, A13, A9, A11, FVSUM_1: 17

        .= (L12 . x) by A5, A6, A14, A11, FUNCOP_1: 22;

      end;

      hence thesis by A5;

    end;

    theorem :: MATRLIN2:8

    ( lmlt (p,(R1 + R2))) = (( lmlt (p,R1)) + ( lmlt (p,R2)))

    proof

      set L12 = ( lmlt (p,(R1 + R2)));

      set L1 = ( lmlt (p,R1));

      set L2 = ( lmlt (p,R2));

      

       A1: ( dom (L1 + L2)) = (( dom L1) /\ ( dom L2)) by Lm3;

      

       A2: ( dom L12) = (( dom p) /\ ( dom (R1 + R2))) by Lm1;

      

       A3: ( dom (R1 + R2)) = (( dom R1) /\ ( dom R2)) by Lm3;

      

       A4: ( dom L1) = (( dom p) /\ ( dom R1)) by Lm1;

      

       A5: ( dom L2) = (( dom p) /\ ( dom R2)) by Lm1;

      

      then

       A6: ( dom (L1 + L2)) = (((( dom p) /\ ( dom R1)) /\ ( dom p)) /\ ( dom R2)) by A1, A4, XBOOLE_1: 16

      .= (((( dom p) /\ ( dom p)) /\ ( dom R1)) /\ ( dom R2)) by XBOOLE_1: 16

      .= ( dom L12) by A3, A2, XBOOLE_1: 16;

      now

        let x be object such that

         A7: x in ( dom (L1 + L2));

        

         A8: x in ( dom L2) by A1, A7, XBOOLE_0:def 4;

        then

         A9: (L2 /. x) = (L2 . x) by PARTFUN1:def 6;

        x in ( dom R2) by A5, A8, XBOOLE_0:def 4;

        then

         A10: (R2 /. x) = (R2 . x) by PARTFUN1:def 6;

        

         A11: x in ( dom (R1 + R2)) by A2, A6, A7, XBOOLE_0:def 4;

        then

         A12: ((R1 + R2) . x) = ((R1 + R2) /. x) by PARTFUN1:def 6;

        

         A13: x in ( dom L1) by A1, A7, XBOOLE_0:def 4;

        then x in ( dom p) by A4, XBOOLE_0:def 4;

        then

         A14: (p /. x) = (p . x) by PARTFUN1:def 6;

        x in ( dom R1) by A4, A13, XBOOLE_0:def 4;

        then

         A15: (R1 /. x) = (R1 . x) by PARTFUN1:def 6;

        

         A16: (L1 /. x) = (L1 . x) by A13, PARTFUN1:def 6;

        

        hence ((L1 + L2) . x) = ((L1 /. x) + (L2 /. x)) by A7, A9, FVSUM_1: 17

        .= ((the lmult of V1 . ((p /. x),(R1 /. x))) + (L2 /. x)) by A13, A16, A14, A15, FUNCOP_1: 22

        .= (((p /. x) * (R1 /. x)) + ((p /. x) * (R2 /. x))) by A8, A9, A14, A10, FUNCOP_1: 22

        .= ((p /. x) * ((R1 /. x) + (R2 /. x))) by VECTSP_1:def 14

        .= ((p /. x) * ((R1 + R2) /. x)) by A11, A15, A10, A12, FVSUM_1: 17

        .= (L12 . x) by A6, A7, A14, A12, FUNCOP_1: 22;

      end;

      hence thesis by A6;

    end;

    theorem :: MATRLIN2:9

    

     Th9: ( len p1) = ( len R1) & ( len p2) = ( len R2) implies ( lmlt ((p1 ^ p2),(R1 ^ R2))) = (( lmlt (p1,R1)) ^ ( lmlt (p2,R2)))

    proof

      assume that

       A1: ( len p1) = ( len R1) and

       A2: ( len p2) = ( len R2);

      reconsider r2 = R2 as Element of (( len p2) -tuples_on the carrier of V1) by A2, FINSEQ_2: 92;

      reconsider r1 = R1 as Element of (( len p1) -tuples_on the carrier of V1) by A1, FINSEQ_2: 92;

      reconsider P1 = p1 as Element of (( len p1) -tuples_on the carrier of K) by FINSEQ_2: 92;

      reconsider P2 = p2 as Element of (( len p2) -tuples_on the carrier of K) by FINSEQ_2: 92;

      

      thus ( lmlt ((p1 ^ p2),(R1 ^ R2))) = ((the lmult of V1 .: (P1,r1)) ^ (the lmult of V1 .: (P2,r2))) by FINSEQOP: 11

      .= (( lmlt (p1,R1)) ^ ( lmlt (p2,R2)));

    end;

    theorem :: MATRLIN2:10

    ( len R1) = ( len R2) implies ( Sum (R1 + R2)) = (( Sum R1) + ( Sum R2))

    proof

      assume ( len R1) = ( len R2);

      then

      reconsider r1 = R1, r2 = R2 as Element of (( len R1) -tuples_on the carrier of V1) by FINSEQ_2: 92;

      

      thus ( Sum (R1 + R2)) = ( Sum (r1 + r2))

      .= (( Sum R1) + ( Sum R2)) by FVSUM_1: 76;

    end;

    theorem :: MATRLIN2:11

    ( Sum ( lmlt ((( len R) |-> a),R))) = (a * ( Sum R))

    proof

      defpred P[ Nat] means for R, a st ( len R) = $1 holds ( Sum ( lmlt ((( len R) |-> a),R))) = (a * ( Sum R));

      

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

      proof

        let n such that

         A2: P[n];

        set n1 = (n + 1);

        let R, a such that

         A3: ( len R) = n1;

        

         A4: ( len (R | n)) = n by A3, FINSEQ_1: 59, NAT_1: 11;

        then

         A5: ( dom (R | n)) = ( Seg n) by FINSEQ_1:def 3;

        1 <= n1 by NAT_1: 11;

        then n1 in ( dom R) by A3, FINSEQ_3: 25;

        then

         A6: (R /. n1) = (R . n1) by PARTFUN1:def 6;

        

         A7: ( lmlt ( <*a*>, <*(R /. n1)*>)) = <*(a * (R /. n1))*> by FINSEQ_2: 74;

        

         A8: ( len <*a*>) = 1 & ( len <*(R . n1)*>) = 1 by FINSEQ_1: 39;

        

         A9: (n1 |-> a) = ((n |-> a) ^ <*a*>) & ( len (n |-> a)) = n by CARD_1:def 7, FINSEQ_2: 60;

        R = ((R | n) ^ <*(R . n1)*>) by A3, FINSEQ_3: 55;

        

        hence ( Sum ( lmlt ((( len R) |-> a),R))) = ( Sum (( lmlt ((n |-> a),(R | n))) ^ ( lmlt ( <*a*>, <*(R /. n1)*>)))) by A3, A6, A4, A9, A8, Th9

        .= (( Sum ( lmlt ((n |-> a),(R | n)))) + ( Sum ( lmlt ( <*a*>, <*(R /. n1)*>)))) by RLVECT_1: 41

        .= ((a * ( Sum (R | n))) + ( Sum <*(a * (R /. n1))*>)) by A2, A4, A7

        .= ((a * ( Sum (R | n))) + (a * (R /. n1))) by RLVECT_1: 44

        .= (a * (( Sum (R | n)) + (R /. n1))) by VECTSP_1:def 14

        .= (a * ( Sum R)) by A3, A6, A4, A5, RLVECT_1: 38;

      end;

      

       A10: P[ 0 ]

      proof

        let R, a such that

         A11: ( len R) = 0 ;

        set L = (( len R) |-> a);

        set M = ( lmlt (L,R));

        ( len L) = ( len R) by CARD_1:def 7;

        then ( dom L) = ( dom R) by FINSEQ_3: 29;

        then ( dom M) = ( dom R) by MATRLIN: 12;

        then ( len R) = ( len M) by FINSEQ_3: 29;

        then M = ( <*> the carrier of V1) by A11;

        then

         A12: ( Sum M) = ( 0. V1) by RLVECT_1: 43;

        R = ( <*> the carrier of V1) by A11;

        then ( Sum R) = ( 0. V1) by RLVECT_1: 43;

        hence thesis by A12, VECTSP_1: 14;

      end;

      for n holds P[n] from NAT_1:sch 2( A10, A1);

      hence thesis;

    end;

    theorem :: MATRLIN2:12

    ( Sum ( lmlt (p,(( len p) |-> v1)))) = (( Sum p) * v1)

    proof

      set L = (( len p) |-> v1);

      set M = ( lmlt (p,L));

      ( len L) = ( len p) by CARD_1:def 7;

      then ( dom L) = ( dom p) by FINSEQ_3: 29;

      then

       A1: ( dom M) = ( dom p) by MATRLIN: 12;

       A2:

      now

        let k, a1 such that

         A3: k in ( dom M) and

         A4: a1 = (p . k);

        k in ( Seg ( len p)) by A1, A3, FINSEQ_1:def 3;

        then (L . k) = v1 by FINSEQ_2: 57;

        hence (M . k) = (a1 * v1) by A3, A4, FUNCOP_1: 22;

      end;

      ( len p) = ( len M) by A1, FINSEQ_3: 29;

      hence thesis by A2, MATRLIN: 9;

    end;

    theorem :: MATRLIN2:13

    ( Sum ( lmlt ((a * p),R))) = (a * ( Sum ( lmlt (p,R))))

    proof

      set Ma = ( lmlt ((a * p),R));

      set M = ( lmlt (p,R));

      ( len (a * p)) = ( len p) by MATRIXR1: 16;

      then

       A1: ( dom (a * p)) = ( dom p) by FINSEQ_3: 29;

      

       A2: ( dom Ma) = (( dom (a * p)) /\ ( dom R)) by Lm1;

      

       A3: ( dom M) = (( dom p) /\ ( dom R)) by Lm1;

      

       A4: for k be Nat holds for v1 st k in ( dom Ma) & v1 = (M . k) holds (Ma . k) = (a * v1)

      proof

        let k be Nat;

        let v1 such that

         A5: k in ( dom Ma) and

         A6: v1 = (M . k);

        k in ( dom R) by A2, A5, XBOOLE_0:def 4;

        then

         A7: (R /. k) = (R . k) by PARTFUN1:def 6;

        k in ( dom p) by A1, A2, A5, XBOOLE_0:def 4;

        then

         A8: (p /. k) = (p . k) by PARTFUN1:def 6;

        k in ( dom (a * p)) by A2, A5, XBOOLE_0:def 4;

        then ((a * p) . k) = (a * (p /. k)) by A8, FVSUM_1: 50;

        

        hence (Ma . k) = ((a * (p /. k)) * (R /. k)) by A5, A7, FUNCOP_1: 22

        .= (a * ((p /. k) * (R /. k))) by VECTSP_1:def 16

        .= (a * v1) by A1, A3, A2, A5, A6, A8, A7, FUNCOP_1: 22;

      end;

      ( len M) = ( len Ma) by A1, A3, A2, FINSEQ_3: 29;

      hence thesis by A4, RLVECT_2: 66;

    end;

    theorem :: MATRLIN2:14

    for B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 st B1 = B2 holds ( lmlt (p,B1)) = ( lmlt (p,B2))

    proof

      let B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 such that

       A1: B1 = B2;

      set M2 = ( lmlt (p,B2));

      set M1 = ( lmlt (p,B1));

      

       A2: ( dom M1) = (( dom p) /\ ( dom B1)) by Lm1;

      

       A3: ( dom M2) = (( dom p) /\ ( dom B2)) by Lm1;

      now

        let i such that

         A4: i in ( dom M1);

        i in ( dom p) by A2, A4, XBOOLE_0:def 4;

        then

         A5: (p . i) = (p /. i) by PARTFUN1:def 6;

        

         A6: i in ( dom B1) by A2, A4, XBOOLE_0:def 4;

        then

         A7: (B2 . i) = (B2 /. i) by A1, PARTFUN1:def 6;

        

         A8: (B1 . i) = (B1 /. i) by A6, PARTFUN1:def 6;

        

        hence (M1 . i) = ((p /. i) * (B1 /. i)) by A4, A5, FUNCOP_1: 22

        .= ((p /. i) * (B2 /. i)) by A1, A6, A8, PARTFUN1:def 6, VECTSP_4: 14

        .= (M2 . i) by A1, A2, A3, A4, A5, A7, FUNCOP_1: 22;

      end;

      hence thesis by A1, A3, Lm1;

    end;

    theorem :: MATRLIN2:15

    for B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 st B1 = B2 holds ( Sum B1) = ( Sum B2)

    proof

      let B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 such that

       A1: B1 = B2;

      defpred P[ Nat] means for B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 st B1 = B2 & ( len B1) = $1 holds ( Sum B1) = ( Sum B2);

      

       A2: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A3: P[n];

        set n1 = (n + 1);

        let B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1 such that

         A4: B1 = B2 and

         A5: ( len B1) = n1;

        

         A6: ( len (B1 | n)) = n by A5, FINSEQ_1: 59, NAT_1: 11;

        then

         A7: ( Sum (B1 | n)) = ( Sum (B2 | n)) by A3, A4;

        1 <= n1 by NAT_1: 11;

        then

         A8: n1 in ( dom B1) by A5, FINSEQ_3: 25;

        then

         A9: (B2 . n1) = (B2 /. n1) by A4, PARTFUN1:def 6;

        

         A10: (B1 . n1) = (B1 /. n1) by A8, PARTFUN1:def 6;

        

         A11: ( dom (B1 | n)) = ( Seg n) by A6, FINSEQ_1:def 3;

        

        hence ( Sum B1) = (( Sum (B1 | n)) + (B1 /. n1)) by A5, A10, A6, RLVECT_1: 38

        .= (( Sum (B2 | n)) + (B2 /. n1)) by A4, A10, A9, A7, VECTSP_4: 13

        .= ( Sum B2) by A4, A5, A9, A6, A11, RLVECT_1: 38;

      end;

      

       A12: P[ 0 ]

      proof

        let B1 be FinSequence of V1, W1 be Subspace of V1, B2 be FinSequence of W1;

        assume B1 = B2 & ( len B1) = 0 ;

        then ( Sum B1) = ( 0. V1) & ( Sum B2) = ( 0. W1) by RLVECT_1: 75;

        hence thesis by VECTSP_4: 11;

      end;

      for n holds P[n] from NAT_1:sch 2( A12, A2);

      then P[( len B1)];

      hence thesis by A1;

    end;

    theorem :: MATRLIN2:16

    i in ( dom R) implies ( Sum ( lmlt (( Line (( 1. (K,( len R))),i)),R))) = (R /. i)

    proof

      set ONE = ( 1. (K,( len R)));

      set L = ( Line (ONE,i));

      set M = ( lmlt (L,R));

      

       A1: ( width ONE) = ( len R) by MATRIX_0: 24;

      ( len L) = ( width ONE) by CARD_1:def 7;

      then ( dom L) = ( dom R) by A1, FINSEQ_3: 29;

      then

       A2: ( dom M) = ( dom R) by MATRLIN: 12;

      then

       A3: ( len M) = ( len R) by FINSEQ_3: 29;

      consider f be sequence of the carrier of V1 such that

       A4: ( Sum M) = (f . ( len M)) and

       A5: (f . 0 ) = ( 0. V1) and

       A6: for j be Nat, v1 st j < ( len M) & v1 = (M . (j + 1)) holds (f . (j + 1)) = ((f . j) + v1) by RLVECT_1:def 12;

      defpred Q[ Nat] means $1 <= ( len M) implies (f . $1) = (R /. i);

      defpred P[ Nat] means $1 < i implies (f . $1) = ( 0. V1);

      assume

       A7: i in ( dom R);

      then

       A8: 1 <= i by FINSEQ_3: 25;

      ( len ONE) = ( len R) by MATRIX_0: 24;

      then

       A9: ( dom R) = ( dom ONE) by FINSEQ_3: 29;

      

       A10: for n st i <= n holds Q[n] implies Q[(n + 1)]

      proof

        let n such that

         A11: i <= n;

        set n1 = (n + 1);

        

         A12: i < n1 by A11, NAT_1: 13;

        reconsider N = n as Element of NAT by ORDINAL1:def 12;

        assume

         A13: Q[n];

        assume

         A14: n1 <= ( len M);

        then

         A15: n < ( len M) by NAT_1: 13;

        

         A16: 1 <= n1 by NAT_1: 11;

        then n1 in ( Seg ( len R)) by A3, A14;

        then (L . n1) = (ONE * (i,n1)) & [i, n1] in ( Indices ONE) by A7, A1, A9, MATRIX_0:def 7, ZFMISC_1: 87;

        then

         A17: (L . n1) = ( 0. K) by A12, MATRIX_1:def 3;

        

         A18: n1 in ( dom R) by A2, A14, A16, FINSEQ_3: 25;

        then (R . n1) = (R /. n1) by PARTFUN1:def 6;

        

        then (M . n1) = (( 0. K) * (R /. n1)) by A2, A18, A17, FUNCOP_1: 22

        .= ( 0. V1) by VECTSP_1: 14;

        

        hence (f . n1) = ((f . N) + ( 0. V1)) by A6, A15

        .= (R /. i) by A13, A14, NAT_1: 13, RLVECT_1:def 4;

      end;

      

       A19: i <= ( len M) by A7, A2, FINSEQ_3: 25;

      

       A20: for n st P[n] holds P[(n + 1)]

      proof

        let n such that

         A21: P[n];

        reconsider N = n as Element of NAT by ORDINAL1:def 12;

        set n1 = (n + 1);

        assume

         A22: n1 < i;

        then n1 < ( len M) by A19, XXREAL_0: 2;

        then

         A23: n < ( len M) by NAT_1: 13;

        

         A24: 1 <= n1 & n1 <= ( len R) by A19, A3, A22, NAT_1: 11, XXREAL_0: 2;

        then n1 in ( Seg ( len R));

        then (L . n1) = (ONE * (i,n1)) & [i, n1] in ( Indices ONE) by A7, A1, A9, MATRIX_0:def 7, ZFMISC_1: 87;

        then

         A25: (L . n1) = ( 0. K) by A22, MATRIX_1:def 3;

        

         A26: n1 in ( dom R) by A24, FINSEQ_3: 25;

        then (R . n1) = (R /. n1) by PARTFUN1:def 6;

        

        then (M . n1) = (( 0. K) * (R /. n1)) by A2, A26, A25, FUNCOP_1: 22

        .= ( 0. V1) by VECTSP_1: 14;

        

        hence (f . n1) = ((f . N) + ( 0. V1)) by A6, A23

        .= ( 0. V1) by A21, A22, NAT_1: 13, RLVECT_1:def 4;

      end;

      

       A27: P[ 0 ] by A5;

      

       A28: for n holds P[n] from NAT_1:sch 2( A27, A20);

      

       A29: Q[i]

      proof

        i in ( Seg ( len R)) by A8, A19, A3;

        then (L . i) = (ONE * (i,i)) & [i, i] in ( Indices ONE) by A7, A1, A9, MATRIX_0:def 7, ZFMISC_1: 87;

        then

         A30: (L . i) = ( 1_ K) by MATRIX_1:def 3;

        reconsider i1 = (i - 1) as Element of NAT by A8, NAT_1: 21;

        

         A31: (i1 + 1) = i;

        then i1 < i by NAT_1: 13;

        then

         A32: (f . i1) = ( 0. V1) by A28;

        assume i <= ( len M);

        then

         A33: i1 < ( len M) by A31, NAT_1: 13;

        (R . i) = (R /. i) by A7, PARTFUN1:def 6;

        

        then (M . i) = (( 1_ K) * (R /. i)) by A7, A2, A30, FUNCOP_1: 22

        .= (R /. i) by VECTSP_1:def 17;

        then (f . (i1 + 1)) = ((f . i1) + (R /. i)) by A6, A33;

        hence thesis by A32, RLVECT_1:def 4;

      end;

      for n st i <= n holds Q[n] from NAT_1:sch 8( A29, A10);

      hence thesis by A19, A4;

    end;

    begin

    theorem :: MATRLIN2:17

    

     Th17: ((v1 + w1) |-- b1) = ((v1 |-- b1) + (w1 |-- b1))

    proof

      set vb = (v1 |-- b1);

      set wb = (w1 |-- b1);

      set vwb = ((v1 + w1) |-- b1);

      consider L1 be Linear_Combination of V1 such that

       A1: v1 = ( Sum L1) & ( Carrier L1) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len vb) holds (vb /. k) = (L1 . (b1 /. k)) by MATRLIN:def 7;

      consider L3 be Linear_Combination of V1 such that

       A3: (v1 + w1) = ( Sum L3) & ( Carrier L3) c= ( rng b1) and

       A4: for k st 1 <= k & k <= ( len vwb) holds (vwb /. k) = (L3 . (b1 /. k)) by MATRLIN:def 7;

      

       A5: ( len wb) = ( len b1) by MATRLIN:def 7;

      reconsider rb1 = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      consider L2 be Linear_Combination of V1 such that

       A6: w1 = ( Sum L2) & ( Carrier L2) c= ( rng b1) and

       A7: for k st 1 <= k & k <= ( len wb) holds (wb /. k) = (L2 . (b1 /. k)) by MATRLIN:def 7;

      

       A8: ( len vb) = ( len b1) by MATRLIN:def 7;

      

       A9: ( len vwb) = ( len b1) by MATRLIN:def 7;

      then

      reconsider vb, wb, vwb as Element of (( len b1) -tuples_on the carrier of K) by A8, A5, FINSEQ_2: 92;

      rb1 is linearly-independent by VECTSP_7:def 3;

      then

       A10: L3 = (L1 + L2) by A1, A6, A3, MATRLIN: 6;

      now

        

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

        let i such that

         A12: i in ( Seg ( len b1));

        

         A13: 1 <= i & i <= ( len b1) by A12, FINSEQ_1: 1;

        ( dom wb) = ( dom b1) by A5, FINSEQ_3: 29;

        then

         A14: (wb . i) = (wb /. i) by A12, A11, PARTFUN1:def 6;

        ( dom vb) = ( dom b1) by A8, FINSEQ_3: 29;

        then

         A15: (vb . i) = (vb /. i) by A12, A11, PARTFUN1:def 6;

        ( dom vwb) = ( dom b1) by A9, FINSEQ_3: 29;

        then (vwb . i) = (vwb /. i) by A12, A11, PARTFUN1:def 6;

        

        hence (vwb . i) = ((L1 + L2) . (b1 /. i)) by A4, A9, A10, A13

        .= ((L1 . (b1 /. i)) + (L2 . (b1 /. i))) by VECTSP_6: 22

        .= ((vb /. i) + (L2 . (b1 /. i))) by A2, A8, A13

        .= ((vb /. i) + (wb /. i)) by A7, A5, A13

        .= ((vb + wb) . i) by A12, A15, A14, FVSUM_1: 18;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: MATRLIN2:18

    

     Th18: ((a * v1) |-- b1) = (a * (v1 |-- b1))

    proof

      set vb = (v1 |-- b1);

      set avb = ((a * v1) |-- b1);

      consider L1 be Linear_Combination of V1 such that

       A1: v1 = ( Sum L1) & ( Carrier L1) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len vb) holds (vb /. k) = (L1 . (b1 /. k)) by MATRLIN:def 7;

      

       A3: ( len vb) = ( len b1) by MATRLIN:def 7;

      reconsider rb1 = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      consider L2 be Linear_Combination of V1 such that

       A4: (a * v1) = ( Sum L2) and

       A5: ( Carrier L2) c= ( rng b1) and

       A6: for k st 1 <= k & k <= ( len avb) holds (avb /. k) = (L2 . (b1 /. k)) by MATRLIN:def 7;

      

       A7: ( len avb) = ( len b1) by MATRLIN:def 7;

      ( len (a * vb)) = ( len vb) by MATRIXR1: 16;

      then

      reconsider vb9 = vb, avb, Avb = (a * vb) as Element of (( len b1) -tuples_on the carrier of K) by A3, A7, FINSEQ_2: 92;

      

       A8: rb1 is linearly-independent by VECTSP_7:def 3;

      now

        let i such that

         A9: i in ( Seg ( len b1));

        

         A10: 1 <= i & i <= ( len b1) by A9, FINSEQ_1: 1;

         A11:

        now

          per cases ;

            suppose a <> ( 0. K);

            then (a * L1) = L2 by A1, A4, A5, A8, MATRLIN: 7;

            

            hence (L2 . (b1 /. i)) = (a * (L1 . (b1 /. i))) by VECTSP_6:def 9

            .= (a * (vb9 /. i)) by A2, A3, A10;

          end;

            suppose

             A12: a = ( 0. K);

            then

             A13: (a * v1) = ( 0. V1) by VECTSP_1: 14;

            L2 is Linear_Combination of ( Carrier L2) & ( Carrier L2) is linearly-independent by A5, A8, VECTSP_6: 7, VECTSP_7: 1;

            then not (b1 /. i) in ( Carrier L2) by A4, A13;

            

            hence (L2 . (b1 /. i)) = ( 0. K)

            .= (a * (vb9 /. i)) by A12;

          end;

        end;

        

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

        ( dom vb) = ( dom b1) by A3, FINSEQ_3: 29;

        then

         A15: (vb . i) = (vb /. i) by A9, A14, PARTFUN1:def 6;

        ( dom avb) = ( dom b1) by A7, FINSEQ_3: 29;

        then (avb . i) = (avb /. i) by A9, A14, PARTFUN1:def 6;

        

        hence (avb . i) = (L2 . (b1 /. i)) by A6, A7, A10

        .= (Avb . i) by A9, A15, A11, FVSUM_1: 51;

      end;

      hence thesis by FINSEQ_2: 119;

    end;

    theorem :: MATRLIN2:19

    

     Th19: i in ( dom b1) implies ((b1 /. i) |-- b1) = ( Line (( 1. (K,( len b1))),i))

    proof

      set ONE = ( 1. (K,( len b1)));

      set bb = ((b1 /. i) |-- b1);

      consider KL be Linear_Combination of V1 such that

       A1: (b1 /. i) = ( Sum KL) & ( Carrier KL) c= ( rng b1) and

       A2: for k st 1 <= k & k <= ( len bb) holds (bb /. k) = (KL . (b1 /. k)) by MATRLIN:def 7;

      reconsider rb1 = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      

       A3: rb1 is linearly-independent by VECTSP_7:def 3;

      (b1 /. i) in {(b1 /. i)} by TARSKI:def 1;

      then (b1 /. i) in ( Lin {(b1 /. i)}) by VECTSP_7: 8;

      then

      consider Lb be Linear_Combination of {(b1 /. i)} such that

       A4: (b1 /. i) = ( Sum Lb) by VECTSP_7: 7;

      assume

       A5: i in ( dom b1);

      then

       A6: (b1 . i) = (b1 /. i) by PARTFUN1:def 6;

      then

       A7: ( Carrier Lb) c= {(b1 . i)} by VECTSP_6:def 4;

      

       A8: (b1 . i) in rb1 by A5, FUNCT_1:def 3;

      then {(b1 . i)} c= rb1 by ZFMISC_1: 31;

      then ( Carrier Lb) c= rb1 by A7;

      then

       A9: Lb = KL by A4, A1, A3, MATRLIN: 5;

      

       A10: ( width ONE) = ( len b1) by MATRIX_0: 24;

      

       A11: ( Indices ONE) = [:( Seg ( len b1)), ( Seg ( len b1)):] by MATRIX_0: 24;

      

       A12: ( len b1) = ( len bb) by MATRLIN:def 7;

      

       A13: (b1 /. i) <> ( 0. V1) by A6, A3, A8, VECTSP_7: 2;

       A14:

      now

        let j such that

         A15: 1 <= j & j <= ( len bb);

        

         A16: j in ( Seg ( len b1)) by A12, A15;

        i in ( Seg ( len b1)) by A5, FINSEQ_1:def 3;

        then

         A17: [i, j] in ( Indices ONE) by A11, A16, ZFMISC_1: 87;

        

         A18: j in ( dom b1) by A12, A15, FINSEQ_3: 25;

        

         A19: ( dom bb) = ( dom b1) by A12, FINSEQ_3: 29;

        now

          per cases ;

            suppose

             A20: i = j;

            ((Lb . (b1 /. i)) * (b1 /. i)) = (b1 /. i) by A4, VECTSP_6: 17

            .= (( 1_ K) * (b1 /. i)) by VECTSP_1:def 17;

            

            then

             A21: ( 1_ K) = (KL . (b1 /. i)) by A13, A9, VECTSP10: 4

            .= (bb /. j) by A2, A15, A20;

            ( 1_ K) = (ONE * (i,j)) by A17, A20, MATRIX_1:def 3

            .= (( Line (ONE,i)) . j) by A10, A16, MATRIX_0:def 7;

            hence (( Line (ONE,i)) . j) = (bb . j) by A18, A19, A21, PARTFUN1:def 6;

          end;

            suppose

             A22: i <> j;

            b1 is one-to-one by MATRLIN:def 2;

            then (b1 . i) <> (b1 . j) by A5, A18, A22;

            then

             A23: not (b1 . j) in ( Carrier Lb) by A7, TARSKI:def 1;

            

             A24: ( 0. K) = (ONE * (i,j)) by A17, A22, MATRIX_1:def 3

            .= (( Line (ONE,i)) . j) by A10, A16, MATRIX_0:def 7;

            (b1 . j) = (b1 /. j) by A18, PARTFUN1:def 6;

            

            then ( 0. K) = (KL . (b1 /. j)) by A9, A23

            .= (bb /. j) by A2, A15;

            hence (( Line (ONE,i)) . j) = (bb . j) by A18, A19, A24, PARTFUN1:def 6;

          end;

        end;

        hence (( Line (ONE,i)) . j) = (bb . j);

      end;

      ( len ( Line (ONE,i))) = ( len b1) by A10, CARD_1:def 7;

      hence thesis by A12, A14;

    end;

    theorem :: MATRLIN2:20

    

     Th20: (( 0. V1) |-- b1) = (( len b1) |-> ( 0. K))

    proof

      per cases ;

        suppose

         A1: ( dom b1) = {} ;

        then

         A2: ( len b1) = 0 by CARD_1: 27, RELAT_1: 41;

        ( len (( 0. V1) |-- b1)) = ( len b1) by MATRLIN:def 7;

        

        hence (( 0. V1) |-- b1) = {} by A1, CARD_1: 27, RELAT_1: 41

        .= (( len b1) |-> ( 0. K)) by A2;

      end;

        suppose ( dom b1) <> {} ;

        then

        consider x be object such that

         A3: x in ( dom b1) by XBOOLE_0:def 1;

        

         A4: ( width ( 1. (K,( len b1)))) = ( len b1) by MATRIX_0: 24;

        reconsider x as Nat by A3;

        ( 0. V1) = ((b1 /. x) - (b1 /. x)) by VECTSP_1: 16

        .= ((b1 /. x) + (( - ( 1_ K)) * (b1 /. x))) by VECTSP_1: 14;

        

        hence (( 0. V1) |-- b1) = (((b1 /. x) |-- b1) + ((( - ( 1_ K)) * (b1 /. x)) |-- b1)) by Th17

        .= (((b1 /. x) |-- b1) + (( - ( 1_ K)) * ((b1 /. x) |-- b1))) by Th18

        .= (( Line (( 1. (K,( len b1))),x)) + (( - ( 1_ K)) * ((b1 /. x) |-- b1))) by A3, Th19

        .= (( Line (( 1. (K,( len b1))),x)) + (( - ( 1_ K)) * ( Line (( 1. (K,( len b1))),x)))) by A3, Th19

        .= (( Line (( 1. (K,( len b1))),x)) + ( - ( Line (( 1. (K,( len b1))),x)))) by FVSUM_1: 59

        .= (( len b1) |-> ( 0. K)) by A4, FVSUM_1: 26;

      end;

    end;

    theorem :: MATRLIN2:21

    

     Th21: ( len b1) = ( dim V1)

    proof

      reconsider R = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      

       A1: b1 is one-to-one by MATRLIN:def 2;

      

      thus ( len b1) = ( card ( Seg ( len b1))) by FINSEQ_1: 57

      .= ( card ( dom b1)) by FINSEQ_1:def 3

      .= ( card R) by A1, CARD_1: 70

      .= ( dim V1) by VECTSP_9:def 1;

    end;

    

     Lm4: for V be VectSp of K holds for W1 be Subspace of V holds for L1 be Linear_Combination of W1 holds ex K1 be Linear_Combination of V st ( Carrier K1) = ( Carrier L1) & ( Sum K1) = ( Sum L1) & (K1 | the carrier of W1) = L1

    proof

      let V be VectSp of K;

      let W1 be Subspace of V;

      let L1 be Linear_Combination of W1;

      defpred P[ object, object] means ($1 in W1 & $2 = (L1 . $1)) or ( not $1 in W1 & $2 = ( 0. K));

      reconsider L9 = L1 as Function of W1, K;

      

       A1: for x be object st x in the carrier of V holds ex y be object st y in the carrier of K & P[x, y]

      proof

        let x be object such that x in the carrier of V;

        per cases ;

          suppose

           A2: x in W1;

          then

          reconsider x as Vector of W1;

           P[x, (L1 . x)] by A2;

          hence thesis;

        end;

          suppose not x in W1;

          hence thesis;

        end;

      end;

      consider K1 be Function of V, K such that

       A3: for x be object st x in the carrier of V holds P[x, (K1 . x)] from FUNCT_2:sch 1( A1);

      

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

      then

      reconsider C = ( Carrier L1) as finite Subset of V by XBOOLE_1: 1;

       A5:

      now

        let v be Vector of V such that

         A6: not v in C;

         P[v, (L1 . v)] & v in the carrier of W1 or P[v, ( 0. K)] by STRUCT_0:def 5;

        then P[v, (L1 . v)] & (L1 . v) = ( 0. K) or P[v, ( 0. K)] by A6;

        hence (K1 . v) = ( 0. K) by A3;

      end;

      K1 is Element of ( Funcs (the carrier of V,the carrier of K)) by FUNCT_2: 8;

      then

      reconsider K1 as Linear_Combination of V by A5, VECTSP_6:def 1;

      reconsider K9 = (K1 | the carrier of W1) as Function of the carrier of W1, the carrier of K by A4, FUNCT_2: 32;

      take K1;

      now

        let x be object;

        assume that

         A7: x in ( Carrier K1) and

         A8: not x in the carrier of W1;

        consider v be Vector of V such that

         A9: x = v and

         A10: (K1 . v) <> ( 0. K) by A7;

         P[v, ( 0. K)] by A8, A9, STRUCT_0:def 5;

        hence contradiction by A3, A10;

      end;

      then

       A11: ( Carrier K1) c= the carrier of W1;

      now

        let x be object such that

         A12: x in the carrier of W1;

         P[x, (K1 . x)] by A3, A4, A12;

        hence (L9 . x) = (K9 . x) by A12, FUNCT_1: 49, STRUCT_0:def 5;

      end;

      then L9 = K9 by FUNCT_2: 12;

      hence thesis by A11, VECTSP_9: 7;

    end;

    theorem :: MATRLIN2:22

    ( rng (b1 | m)) is linearly-independent Subset of V1 & for A be Subset of V1 st A = ( rng (b1 | m)) holds (b1 | m) is OrdBasis of ( Lin A)

    proof

      reconsider RNG = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      

       A1: RNG is linearly-independent by VECTSP_7:def 3;

      ( rng (b1 | m)) c= RNG by RELAT_1: 70;

      hence ( rng (b1 | m)) is linearly-independent Subset of V1 by A1, VECTSP_7: 1, XBOOLE_1: 1;

      let A be Subset of V1 such that

       A2: A = ( rng (b1 | m));

      

       A3: A c= the carrier of ( Lin A)

      proof

        let x be object;

        assume x in A;

        then x in ( Lin A) by VECTSP_7: 8;

        hence thesis;

      end;

      A is linearly-independent by A1, A2, RELAT_1: 70, VECTSP_7: 1;

      then

      reconsider A9 = A as linearly-independent Subset of ( Lin A) by A3, VECTSP_9: 12;

      b1 is one-to-one by MATRLIN:def 2;

      then

       A4: (b1 | m) is one-to-one by FUNCT_1: 52;

      ( Lin A9) = the ModuleStr of ( Lin A) by VECTSP_9: 17;

      then ( rng (b1 | m)) is Basis of ( Lin A) & (b1 | m) is FinSequence of ( Lin A) by A2, FINSEQ_1:def 4, VECTSP_7:def 3;

      hence thesis by A4, MATRLIN:def 2;

    end;

    theorem :: MATRLIN2:23

    ( rng (b1 /^ m)) is linearly-independent Subset of V1 & for A be Subset of V1 st A = ( rng (b1 /^ m)) holds (b1 /^ m) is OrdBasis of ( Lin A)

    proof

      reconsider RNG = ( rng b1) as Basis of V1 by MATRLIN:def 2;

      

       A1: RNG is linearly-independent by VECTSP_7:def 3;

      ( rng (b1 /^ m)) c= RNG by FINSEQ_5: 33;

      hence ( rng (b1 /^ m)) is linearly-independent Subset of V1 by A1, VECTSP_7: 1, XBOOLE_1: 1;

      let A be Subset of V1 such that

       A2: A = ( rng (b1 /^ m));

      

       A3: A c= the carrier of ( Lin A)

      proof

        let x be object;

        assume x in A;

        then x in ( Lin A) by VECTSP_7: 8;

        hence thesis;

      end;

      A is linearly-independent by A1, A2, FINSEQ_5: 33, VECTSP_7: 1;

      then

      reconsider A9 = A as linearly-independent Subset of ( Lin A) by A3, VECTSP_9: 12;

      b1 is one-to-one & b1 = ((b1 | m) ^ (b1 /^ m)) by MATRLIN:def 2, RFINSEQ: 8;

      then

       A4: (b1 /^ m) is one-to-one by FINSEQ_3: 91;

      ( Lin A9) = the ModuleStr of ( Lin A) by VECTSP_9: 17;

      then ( rng (b1 /^ m)) is Basis of ( Lin A) & (b1 /^ m) is FinSequence of ( Lin A) by A2, FINSEQ_1:def 4, VECTSP_7:def 3;

      hence thesis by A4, MATRLIN:def 2;

    end;

    theorem :: MATRLIN2:24

    

     Th24: for W1,W2 be Subspace of V1 st (W1 /\ W2) = ( (0). V1) holds for b1 be OrdBasis of W1, b2 be OrdBasis of W2, b be OrdBasis of (W1 + W2) st b = (b1 ^ b2) holds for v,v1,v2 be Vector of (W1 + W2), w1 be Vector of W1, w2 be Vector of W2 st v = (v1 + v2) & v1 = w1 & v2 = w2 holds (v |-- b) = ((w1 |-- b1) ^ (w2 |-- b2))

    proof

      let W1,W2 be Subspace of V1 such that

       A1: (W1 /\ W2) = ( (0). V1);

      ( [#] ( (0). V1)) = {( 0. V1)} by VECTSP_4:def 3;

      then

       A2: ( card ( [#] ( (0). V1))) = 1 by CARD_1: 30;

      

       A3: (( dim W1) + ( dim W2)) = (( dim (W1 + W2)) + ( dim (W1 /\ W2))) by VECTSP_9: 32

      .= (( dim (W1 + W2)) + 0 ) by A1, A2, RANKNULL: 5;

      let b1 be OrdBasis of W1, b2 be OrdBasis of W2, b be OrdBasis of (W1 + W2) such that

       A4: b = (b1 ^ b2);

      reconsider R = ( rng b) as Basis of (W1 + W2) by MATRLIN:def 2;

      let v,v1,v2 be Vector of (W1 + W2), w1 be Vector of W1, w2 be Vector of W2 such that

       A5: v = (v1 + v2) & v1 = w1 & v2 = w2;

      set wb2 = (w2 |-- b2);

      consider L2 be Linear_Combination of W2 such that

       A6: w2 = ( Sum L2) and

       A7: ( Carrier L2) c= ( rng b2) and

       A8: for k st 1 <= k & k <= ( len wb2) holds (wb2 /. k) = (L2 . (b2 /. k)) by MATRLIN:def 7;

      

       A9: W2 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then

      consider K2 be Linear_Combination of (W1 + W2) such that

       A10: ( Carrier K2) = ( Carrier L2) and

       A11: ( Sum K2) = ( Sum L2) and

       A12: (K2 | the carrier of W2) = L2 by Lm4;

      ( rng b2) c= R by A4, FINSEQ_1: 30;

      then

       A13: ( Carrier K2) c= R by A7, A10;

      set wb1 = (w1 |-- b1);

      set vb = (v |-- b);

      consider L1 be Linear_Combination of W1 such that

       A14: w1 = ( Sum L1) and

       A15: ( Carrier L1) c= ( rng b1) and

       A16: for k st 1 <= k & k <= ( len wb1) holds (wb1 /. k) = (L1 . (b1 /. k)) by MATRLIN:def 7;

      consider L be Linear_Combination of (W1 + W2) such that

       A17: v = ( Sum L) & ( Carrier L) c= ( rng b) and

       A18: for k st 1 <= k & k <= ( len vb) holds (vb /. k) = (L . (b /. k)) by MATRLIN:def 7;

      

       A19: ( len vb) = ( len b) by MATRLIN:def 7;

      then

       A20: ( dom vb) = ( dom b) by FINSEQ_3: 29;

      

       A21: ( len wb2) = ( len b2) by MATRLIN:def 7;

      then

       A22: ( dom wb2) = ( dom b2) by FINSEQ_3: 29;

      

       A23: R is linearly-independent by VECTSP_7:def 3;

      

       A24: W1 is Subspace of (W1 + W2) by VECTSP_5: 7;

      then

      consider K1 be Linear_Combination of (W1 + W2) such that

       A25: ( Carrier K1) = ( Carrier L1) and

       A26: ( Sum K1) = ( Sum L1) and

       A27: (K1 | the carrier of W1) = L1 by Lm4;

      

       A28: ( len wb1) = ( len b1) by MATRLIN:def 7;

      then

       A29: ( dom wb1) = ( dom b1) by FINSEQ_3: 29;

      

       A30: ( len (wb1 ^ wb2)) = (( len wb1) + ( len wb2)) by FINSEQ_1: 22;

      

       A31: ( len b1) = ( dim W1) & ( len b2) = ( dim W2) by Th21;

      

       A32: ( len b) = ( dim (W1 + W2)) by Th21;

      then

       A33: ( dom b) = ( dom (wb1 ^ wb2)) by A28, A21, A31, A30, A3, FINSEQ_3: 29;

      ( rng b1) c= R by A4, FINSEQ_1: 29;

      then

       A34: ( Carrier K1) c= R by A15, A25;

      then

       A35: L = (K1 + K2) by A5, A14, A26, A6, A11, A17, A13, A23, MATRLIN: 6;

      now

        let k such that

         A36: 1 <= k & k <= ( len vb);

        

         A37: k in ( dom (wb1 ^ wb2)) by A28, A21, A19, A31, A32, A30, A3, A36, FINSEQ_3: 25;

        now

          per cases by A37, FINSEQ_1: 25;

            suppose

             A38: k in ( dom wb1);

            then 1 <= k & k <= ( len wb1) by FINSEQ_3: 25;

            

            then

             A39: (L1 . (b1 /. k)) = (wb1 /. k) by A16

            .= (wb1 . k) by A38, PARTFUN1:def 6

            .= ((wb1 ^ wb2) . k) by A38, FINSEQ_1:def 7;

            reconsider b1k = (b1 /. k) as Vector of (W1 + W2) by A24, VECTSP_4: 10;

            

             A40: (K1 . (b1 /. k)) = (L1 . (b1 /. k)) by A27, FUNCT_1: 49;

             not (b1 /. k) in ( Carrier K2)

            proof

              

               A41: (b1 /. k) in W1;

              assume

               A42: (b1 /. k) in ( Carrier K2);

              then (b1 /. k) in W2 by A10;

              then (b1 /. k) in (W1 /\ W2) by A41, VECTSP_5: 3;

              then (b1 /. k) in the carrier of ( (0). V1) by A1;

              then (b1 /. k) in {( 0. V1)} by VECTSP_4:def 3;

              

              then (b1 /. k) = ( 0. V1) by TARSKI:def 1

              .= ( 0. (W1 + W2)) by VECTSP_4: 11;

              hence thesis by A13, A23, A42, VECTSP_7: 2;

            end;

            then (K2 . b1k) = ( 0. K);

            

            then

             A43: (L . b1k) = ((K1 . b1k) + ( 0. K)) by A35, VECTSP_6: 22

            .= ((wb1 ^ wb2) . k) by A39, A40, RLVECT_1:def 4;

            b1k = (b1 . k) by A29, A38, PARTFUN1:def 6

            .= (b . k) by A4, A29, A38, FINSEQ_1:def 7

            .= (b /. k) by A33, A37, PARTFUN1:def 6;

            

            hence ((wb1 ^ wb2) . k) = (vb /. k) by A18, A36, A43

            .= (vb . k) by A33, A20, A37, PARTFUN1:def 6;

          end;

            suppose ex n st n in ( dom wb2) & k = (( len wb1) + n);

            then

            consider n such that

             A44: n in ( dom wb2) and

             A45: k = (( len wb1) + n);

            1 <= n & n <= ( len wb2) by A44, FINSEQ_3: 25;

            

            then

             A46: (L2 . (b2 /. n)) = (wb2 /. n) by A8

            .= (wb2 . n) by A44, PARTFUN1:def 6

            .= ((wb1 ^ wb2) . k) by A44, A45, FINSEQ_1:def 7;

            reconsider b2n = (b2 /. n) as Vector of (W1 + W2) by A9, VECTSP_4: 10;

            

             A47: (K2 . (b2 /. n)) = (L2 . (b2 /. n)) by A12, FUNCT_1: 49;

             not (b2 /. n) in ( Carrier K1)

            proof

              assume

               A48: (b2 /. n) in ( Carrier K1);

              then (b2 /. n) in W2 & (b2 /. n) in W1 by A25;

              then (b2 /. n) in (W1 /\ W2) by VECTSP_5: 3;

              then (b2 /. n) in the carrier of ( (0). V1) by A1;

              then (b2 /. n) in {( 0. V1)} by VECTSP_4:def 3;

              

              then (b2 /. n) = ( 0. V1) by TARSKI:def 1

              .= ( 0. (W1 + W2)) by VECTSP_4: 11;

              hence thesis by A34, A23, A48, VECTSP_7: 2;

            end;

            then (K1 . b2n) = ( 0. K);

            

            then

             A49: (L . b2n) = (( 0. K) + (K2 . b2n)) by A35, VECTSP_6: 22

            .= ((wb1 ^ wb2) . k) by A46, A47, RLVECT_1:def 4;

            b2n = (b2 . n) by A22, A44, PARTFUN1:def 6

            .= (b . k) by A4, A28, A22, A44, A45, FINSEQ_1:def 7

            .= (b /. k) by A33, A37, PARTFUN1:def 6;

            

            hence ((wb1 ^ wb2) . k) = (vb /. k) by A18, A36, A49

            .= (vb . k) by A33, A20, A37, PARTFUN1:def 6;

          end;

        end;

        hence (vb . k) = ((wb1 ^ wb2) . k);

      end;

      hence thesis by A28, A21, A19, A31, A30, A3, Th21;

    end;

    theorem :: MATRLIN2:25

    

     Th25: for W1 be Subspace of V1 st W1 = ( (Omega). V1) holds for w be Vector of W1, v be Vector of V1, w1 be OrdBasis of W1 st v = w & b1 = w1 holds (v |-- b1) = (w |-- w1)

    proof

      let W1 be Subspace of V1 such that

       A1: W1 = ( (Omega). V1);

      let w be Vector of W1, v be Vector of V1, w1 be OrdBasis of W1 such that

       A2: v = w and

       A3: b1 = w1;

      consider KL be Linear_Combination of W1 such that

       A4: w = ( Sum KL) & ( Carrier KL) c= ( rng w1) and

       A5: for k st 1 <= k & k <= ( len (w |-- w1)) holds ((w |-- w1) /. k) = (KL . (w1 /. k)) by MATRLIN:def 7;

      consider K1 be Linear_Combination of V1 such that

       A6: ( Carrier K1) = ( Carrier KL) & ( Sum K1) = ( Sum KL) and

       A7: (K1 | the carrier of W1) = KL by Lm4;

      

       A8: ( len w1) = ( len (w |-- w1)) by MATRLIN:def 7;

      now

        let k such that

         A9: 1 <= k & k <= ( len (w |-- w1));

        

         A10: k in ( dom w1) by A8, A9, FINSEQ_3: 25;

        ( dom K1) = the carrier of W1 by A1, FUNCT_2:def 1;

        then KL = K1 by A7;

        

        hence ((w |-- w1) /. k) = (K1 . (w1 /. k)) by A5, A9

        .= (K1 . (w1 . k)) by A10, PARTFUN1:def 6

        .= (K1 . (b1 /. k)) by A3, A10, PARTFUN1:def 6;

      end;

      hence thesis by A2, A3, A4, A6, A8, MATRLIN:def 7;

    end;

    theorem :: MATRLIN2:26

    

     Th26: for W1,W2 be Subspace of V1 st (W1 /\ W2) = ( (0). V1) holds for w1 be OrdBasis of W1, w2 be OrdBasis of W2 holds (w1 ^ w2) is OrdBasis of (W1 + W2)

    proof

      let W1,W2 be Subspace of V1 such that

       A1: (W1 /\ W2) = ( (0). V1);

      let w1 be OrdBasis of W1, w2 be OrdBasis of W2;

      reconsider R1 = ( rng w1) as Basis of W1 by MATRLIN:def 2;

      reconsider R2 = ( rng w2) as Basis of W2 by MATRLIN:def 2;

      

       A2: (R1 \/ R2) = ( rng (w1 ^ w2)) by FINSEQ_1: 31;

      

       A3: R1 misses R2

      proof

        assume R1 meets R2;

        then

        consider x be object such that

         A4: x in R1 and

         A5: x in R2 by XBOOLE_0: 3;

        x in W1 & x in W2 by A4, A5;

        then x in (W1 /\ W2) by VECTSP_5: 3;

        then x in the carrier of ( (0). V1) by A1;

        then x in {( 0. V1)} by VECTSP_4:def 3;

        

        then x = ( 0. V1) by TARSKI:def 1

        .= ( 0. W1) by VECTSP_4: 11;

        then not R1 is linearly-independent by A4, VECTSP_7: 2;

        hence thesis by VECTSP_7:def 3;

      end;

      

       A6: (R1 \/ R2) is Basis of (W1 + W2) by A1, Th3;

      then

      reconsider w12 = (w1 ^ w2) as FinSequence of (W1 + W2) by A2, FINSEQ_1:def 4;

      w1 is one-to-one & w2 is one-to-one by MATRLIN:def 2;

      then w12 is one-to-one by A3, FINSEQ_3: 91;

      hence thesis by A6, A2, MATRLIN:def 2;

    end;

    begin

    definition

      let K, V1, V2, f, B1, b2;

      :: original: AutMt

      redefine

      func AutMt (f,B1,b2) -> Matrix of ( len B1), ( len b2), K ;

      coherence

      proof

        reconsider A9 = ( AutMt (f,B1,b2)) as Matrix of ( len ( AutMt (f,B1,b2))), ( width ( AutMt (f,B1,b2))), K by MATRIX_0: 51;

        

         A1: ( len A9) = ( len B1) by MATRLIN:def 8;

        per cases ;

          suppose

           A2: ( len B1) = 0 ;

          then ( AutMt (f,B1,b2)) = {} by A1;

          hence thesis by A2, MATRIX_0: 13;

        end;

          suppose

           A3: ( len B1) > 0 ;

          

           A4: ( dom B1) = ( dom A9) by A1, FINSEQ_3: 29;

          

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

          

           A6: ( len B1) in ( Seg ( len B1)) by A3, FINSEQ_1: 3;

          

          then ((f . (B1 /. ( len B1))) |-- b2) = (A9 /. ( len B1)) by A5, MATRLIN:def 8

          .= (A9 . ( len B1)) by A3, A5, A4, FINSEQ_1: 3, PARTFUN1:def 6

          .= ( Line (A9,( len B1))) by A1, A6, MATRIX_0: 52;

          

          then

           A7: ( width A9) = ( len ((f . (B1 /. ( len B1))) |-- b2)) by CARD_1:def 7

          .= ( len b2) by MATRLIN:def 7;

          ( len A9) = ( len B1) by MATRLIN:def 8;

          hence thesis by A7;

        end;

      end;

    end

    definition

      let S be 1-sorted;

      let R be Relation;

      :: MATRLIN2:def1

      func R | S -> set equals (R | the carrier of S);

      coherence ;

    end

    theorem :: MATRLIN2:27

    for f be linear-transformation of V1, V2 holds for W1,W2 be Subspace of V1, U1,U2 be Subspace of V2 st (( dim W1) = 0 implies ( dim U1) = 0 ) & (( dim W2) = 0 implies ( dim U2) = 0 ) & V2 is_the_direct_sum_of (U1,U2) holds for fW1 be linear-transformation of W1, U1, fW2 be linear-transformation of W2, U2 st fW1 = (f | W1) & fW2 = (f | W2) holds for w1 be OrdBasis of W1, w2 be OrdBasis of W2, u1 be OrdBasis of U1, u2 be OrdBasis of U2 st (w1 ^ w2) = b1 & (u1 ^ u2) = b2 holds ( AutMt (f,b1,b2)) = ( block_diagonal ( <*( AutMt (fW1,w1,u1)), ( AutMt (fW2,w2,u2))*>,( 0. K)))

    proof

      let f be linear-transformation of V1, V2;

      let W1,W2 be Subspace of V1, U1,U2 be Subspace of V2 such that

       A1: ( dim W1) = 0 implies ( dim U1) = 0 and

       A2: ( dim W2) = 0 implies ( dim U2) = 0 and

       A3: V2 is_the_direct_sum_of (U1,U2);

      

       A4: (U1 /\ U2) = ( (0). V2) by A3, VECTSP_5:def 4;

      let fW1 be linear-transformation of W1, U1;

      let fW2 be linear-transformation of W2, U2 such that

       A5: fW1 = (f | W1) and

       A6: fW2 = (f | W2);

      let w1 be OrdBasis of W1, w2 be OrdBasis of W2, u1 be OrdBasis of U1, u2 be OrdBasis of U2 such that

       A7: (w1 ^ w2) = b1 and

       A8: (u1 ^ u2) = b2;

      

       A9: ( len b1) = (( len w1) + ( len w2)) by A7, FINSEQ_1: 22;

      

       A10: (U1 + U2) = ( (Omega). V2) by A3, VECTSP_5:def 4;

      set A = ( AutMt (f,b1,b2));

      

       A11: ( len b1) = ( len A) by MATRLIN:def 8;

      set A2 = ( AutMt (fW2,w2,u2));

      

       A12: ( len w2) = ( dim W2) & ( len u2) = ( dim U2) by Th21;

      then

       A13: ( len w2) = ( len A2) by A2, MATRIX13: 1;

      set A1 = ( AutMt (fW1,w1,u1));

      

       A14: ( len w1) = ( dim W1) & ( len u1) = ( dim U1) by Th21;

      then

       A15: ( len w1) = ( len A1) by A1, MATRIX13: 1;

      

       A16: ( len u2) = ( width A2) by A2, A12, MATRIX13: 1;

      

       A17: ( len u1) = ( width A1) by A1, A14, MATRIX13: 1;

       A18:

      now

        reconsider uu = (u1 ^ u2) as OrdBasis of (U1 + U2) by A4, Th26;

        let i;

        

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

        reconsider fb = (f . (b1 /. i)), fbi = (f . (b1 /. (i + ( len A1)))) as Vector of (U1 + U2) by A10;

        

         A20: ( dom A) = ( dom b1) by A11, FINSEQ_3: 29;

        

         A21: ( dom A1) = ( dom w1) by A15, FINSEQ_3: 29;

        

         A22: ( dom fW1) = the carrier of W1 by FUNCT_2:def 1;

        thus i in ( dom A1) implies ( Line (A,i)) = (( Line (A1,i)) ^ (( width A2) |-> ( 0. K)))

        proof

          assume

           A23: i in ( dom A1);

          

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

          

          then

           A25: ( Line (A1,i)) = (A1 . i) by A15, A23, MATRIX_0: 52

          .= (A1 /. i) by A23, PARTFUN1:def 6

          .= ((fW1 . (w1 /. i)) |-- u1) by A21, A23, MATRLIN:def 8;

          ( len A1) <= ( len A) by A9, A15, A11, NAT_1: 11;

          then

           A26: ( Seg ( len A1)) c= ( Seg ( len A)) by FINSEQ_1: 5;

          

          then (b1 /. i) = (b1 . i) by A19, A20, A23, A24, PARTFUN1:def 6

          .= (w1 . i) by A7, A21, A23, FINSEQ_1:def 7

          .= (w1 /. i) by A21, A23, PARTFUN1:def 6;

          then

           A27: fb = (fW1 . (w1 /. i)) by A5, A22, FUNCT_1: 47;

          

          thus ( Line (A,i)) = (A . i) by A11, A23, A24, A26, MATRIX_0: 52

          .= (A /. i) by A19, A23, A24, A26, PARTFUN1:def 6

          .= ((f . (b1 /. i)) |-- b2) by A19, A20, A23, A24, A26, MATRLIN:def 8

          .= (fb |-- uu) by A10, A8, Th25

          .= ((fb + ( 0. (U1 + U2))) |-- uu) by RLVECT_1:def 4

          .= (((fW1 . (w1 /. i)) |-- u1) ^ (( 0. U2) |-- u2)) by A4, A27, Th24, VECTSP_4: 12

          .= (( Line (A1,i)) ^ (( width A2) |-> ( 0. K))) by A16, A25, Th20;

        end;

        

         A28: ( dom A2) = ( dom w2) by A13, FINSEQ_3: 29;

        

         A29: ( dom fW2) = the carrier of W2 by FUNCT_2:def 1;

        thus i in ( dom A2) implies ( Line (A,(i + ( len A1)))) = ((( width A1) |-> ( 0. K)) ^ ( Line (A2,i)))

        proof

          assume

           A30: i in ( dom A2);

          

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

          then

           A32: (i + ( len A1)) in ( dom A) by A9, A15, A13, A11, A19, A30, FINSEQ_1: 60;

          (b1 /. (i + ( len A1))) = (b1 . (i + ( len A1))) by A9, A15, A13, A11, A19, A20, A30, A31, FINSEQ_1: 60, PARTFUN1:def 6

          .= (w2 . i) by A7, A15, A28, A30, FINSEQ_1:def 7

          .= (w2 /. i) by A28, A30, PARTFUN1:def 6;

          then

           A33: fbi = (fW2 . (w2 /. i)) by A6, A29, FUNCT_1: 47;

          

           A34: ( Line (A2,i)) = (A2 . i) by A13, A30, A31, MATRIX_0: 52

          .= (A2 /. i) by A30, PARTFUN1:def 6

          .= ((fW2 . (w2 /. i)) |-- u2) by A28, A30, MATRLIN:def 8;

          

          thus ( Line (A,(i + ( len A1)))) = (A . (i + ( len A1))) by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1: 60, MATRIX_0: 52

          .= (A /. (i + ( len A1))) by A9, A15, A13, A11, A19, A30, A31, FINSEQ_1: 60, PARTFUN1:def 6

          .= ((f . (b1 /. (i + ( len A1)))) |-- b2) by A20, A32, MATRLIN:def 8

          .= (fbi |-- uu) by A10, A8, Th25

          .= ((( 0. (U1 + U2)) + fbi) |-- uu) by RLVECT_1:def 4

          .= ((( 0. U1) |-- u1) ^ ((fW2 . (w2 /. i)) |-- u2)) by A4, A33, Th24, VECTSP_4: 12

          .= ((( width A1) |-> ( 0. K)) ^ ( Line (A2,i))) by A17, A34, Th20;

        end;

      end;

      set A12 = <*A1, A2*>;

      

       A35: ( Sum ( Len A12)) = (( len A1) + ( len A2)) & ( Sum ( Width A12)) = (( width A1) + ( width A2)) by MATRIXJ1: 16, MATRIXJ1: 20;

      ( len b2) = (( len u1) + ( len u2)) by A8, FINSEQ_1: 22;

      hence thesis by A9, A15, A13, A17, A16, A35, A18, MATRIXJ1: 23;

    end;

    definition

      let K, V1, V2;

      let f be Function of V1, V2;

      let B1 be FinSequence of V1;

      let b2 be OrdBasis of V2;

      assume

       A1: ( len B1) = ( len b2);

      :: MATRLIN2:def2

      func AutEqMt (f,B1,b2) -> Matrix of ( len B1), ( len B1), K equals

      : Def2: ( AutMt (f,B1,b2));

      coherence by A1;

    end

    theorem :: MATRLIN2:28

    

     Th28: ( AutMt (( id V1),b1,b1)) = ( 1. (K,( len b1)))

    proof

      set A = ( AutMt (( id V1),b1,b1));

      set ONE = ( 1. (K,( len b1)));

      

       A1: ( len A) = ( len b1) by MATRIX_0:def 2;

       A2:

      now

        let i such that

         A3: 1 <= i & i <= ( len b1);

        

         A4: i in ( dom b1) by A3, FINSEQ_3: 25;

        

         A5: i in ( Seg ( len b1)) by A3;

        i in ( dom A) by A1, A3, FINSEQ_3: 25;

        

        hence (A . i) = (A /. i) by PARTFUN1:def 6

        .= ((( id V1) . (b1 /. i)) |-- b1) by A4, MATRLIN:def 8

        .= ((b1 /. i) |-- b1)

        .= ( Line (ONE,i)) by A4, Th19

        .= (ONE . i) by A5, MATRIX_0: 52;

      end;

      ( len ONE) = ( len b1) by MATRIX_0:def 2;

      hence thesis by A1, A2;

    end;

    theorem :: MATRLIN2:29

    ( AutEqMt (( id V1),b1,b19)) is invertible & ( AutEqMt (( id V1),b19,b1)) = (( AutEqMt (( id V1),b1,b19)) ~ )

    proof

      set A = ( AutEqMt (( id V1),b1,b19));

      

       A1: ( 1_ K) <> ( 0. K);

      

       A2: ( len b1) = ( dim V1) by Th21

      .= ( len b19) by Th21;

      then

      reconsider A9 = ( AutEqMt (( id V1),b19,b1)) as Matrix of ( len b1), ( len b1), K;

      

       A3: A = ( AutMt (( id V1),b1,b19)) & A9 = ( AutMt (( id V1),b19,b1)) by A2, Def2;

      per cases ;

        suppose ( len b1) = 0 ;

        then ( Det A) = ( 1_ K) & A9 = (A ~ ) by MATRIXR2: 41, MATRIX_0: 45;

        hence thesis by A1, LAPLACE: 34;

      end;

        suppose

         A4: (( len b1) + 0 ) > 0 ;

        ( dom ( id V1)) = the carrier of V1;

        then

         A5: (( id V1) * ( id V1)) = ( id V1) by RELAT_1: 52;

        ( len b1) = ( dim V1) by Th21;

        then ( len b1) = ( len b19) by Th21;

        

        then

         A6: (A * A9) = ( AutMt ((( id V1) * ( id V1)),b1,b1)) by A3, A4, MATRLIN: 41

        .= ( 1. (K,( len b1))) by A5, Th28;

        ( len b1) >= 1 by A4, NAT_1: 19;

        

        then ( 1_ K) = ( Det (A * A9)) by A6, MATRIX_7: 16

        .= (( Det A) * ( Det A9)) by A4, MATRIX11: 62;

        then ( Det A) <> ( 0. K);

        then

         A7: A is invertible by LAPLACE: 34;

        then (A ~ ) is_reverse_of A by MATRIX_6:def 4;

        then (A * (A ~ )) = ( 1. (K,( len b1))) by MATRIX_6:def 2;

        hence thesis by A6, A7, MATRIX_8: 19;

      end;

    end;

    theorem :: MATRLIN2:30

    

     Th30: ( len p1) = ( len p2) & ( len p1) = ( len B1) & ( len p1) > 0 & j in ( dom b1) & (for i st i in ( dom p2) holds (p2 . i) = (((B1 /. i) |-- b1) . j)) implies (p1 "*" p2) = ((( Sum ( lmlt (p1,B1))) |-- b1) . j)

    proof

      assume that

       A1: ( len p1) = ( len p2) and

       A2: ( len p1) = ( len B1) and

       A3: ( len p1) > 0 and

       A4: j in ( dom b1) and

       A5: for i st i in ( dom p2) holds (p2 . i) = (((B1 /. i) |-- b1) . j);

      deffunc m( Nat, Nat) = (((B1 /. $1) |-- b1) /. $2);

      consider M be Matrix of ( len p1), ( len b1), K such that

       A6: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = m(i,j) from MATRIX_0:sch 1;

      

       A7: ( len M) = ( len p1) by A3, MATRIX_0: 23;

      then

       A8: ( dom p1) = ( dom M) by FINSEQ_3: 29;

      

       A9: ( width M) = ( len b1) by A3, MATRIX_0: 23;

      

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

      

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

      

       A12: ( dom p1) = ( dom p2) by A1, FINSEQ_3: 29;

       A13:

      now

        let i;

        assume 1 <= i & i <= ( len p2);

        then

         A14: i in ( dom p1) by A1, A11;

        then

         A15: [i, j] in ( Indices M) by A4, A9, A8, A10, ZFMISC_1: 87;

        ( len ((B1 /. i) |-- b1)) = ( len b1) by MATRLIN:def 7;

        then

         A16: ( dom ((B1 /. i) |-- b1)) = ( dom b1) by FINSEQ_3: 29;

        

        thus (( Col (M,j)) . i) = (M * (i,j)) by A8, A14, MATRIX_0:def 8

        .= (((B1 /. i) |-- b1) /. j) by A6, A15

        .= (((B1 /. i) |-- b1) . j) by A4, A16, PARTFUN1:def 6

        .= (p2 . i) by A5, A12, A14;

      end;

      deffunc mC( Nat) = ( Sum ( mlt (p1,( Col (M,$1)))));

      consider MC be FinSequence of K such that

       A17: ( len MC) = ( len b1) & for j be Nat st j in ( dom MC) holds (MC . j) = mC(j) from FINSEQ_2:sch 1;

      

       A18: for j st j in ( dom MC) holds (MC /. j) = mC(j)

      proof

        let j;

        assume

         A19: j in ( dom MC);

        then (MC . j) = mC(j) by A17;

        hence thesis by A19, PARTFUN1:def 6;

      end;

      

       A20: ( dom b1) = ( dom MC) by A17, FINSEQ_3: 29;

      

       A21: ( dom p1) = ( dom B1) by A2, FINSEQ_3: 29;

       A22:

      now

        let i such that

         A23: i in ( dom B1);

        

         A24: ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7;

        ( len ((B1 /. i) |-- b1)) = ( len b1) by MATRLIN:def 7;

        then

         A25: ( dom ( Line (M,i))) = ( dom ((B1 /. i) |-- b1)) by A9, A24, FINSEQ_3: 29;

        

         A26: ( dom ( Line (M,i))) = ( Seg ( width M)) by A24, FINSEQ_1:def 3;

         A27:

        now

          let k such that

           A28: k in ( dom ((B1 /. i) |-- b1));

          

           A29: [i, k] in ( Indices M) by A21, A8, A23, A25, A26, A28, ZFMISC_1: 87;

          

          thus (( Line (M,i)) . k) = (M * (i,k)) by A25, A26, A28, MATRIX_0:def 7

          .= (((B1 /. i) |-- b1) /. k) by A6, A29

          .= (((B1 /. i) |-- b1) . k) by A28, PARTFUN1:def 6;

        end;

        

        thus (B1 /. i) = ( Sum ( lmlt (((B1 /. i) |-- b1),b1))) by MATRLIN: 35

        .= ( Sum ( lmlt (( Line (M,i)),b1))) by A25, A27, FINSEQ_1: 13;

      end;

      

       A30: b1 <> {} by A4;

      

       A31: ( len ( Col (M,j))) = ( len M) by CARD_1:def 7;

      ( len (( Sum ( lmlt (p1,B1))) |-- b1)) = ( len b1) by MATRLIN:def 7;

      then ( dom (( Sum ( lmlt (p1,B1))) |-- b1)) = ( dom b1) by FINSEQ_3: 29;

      

      hence ((( Sum ( lmlt (p1,B1))) |-- b1) . j) = ((( Sum ( lmlt (p1,B1))) |-- b1) /. j) by A4, PARTFUN1:def 6

      .= ((( Sum ( lmlt (MC,b1))) |-- b1) /. j) by A2, A3, A17, A18, A30, A22, MATRLIN: 33

      .= (MC /. j) by A17, MATRLIN: 36

      .= (MC . j) by A4, A20, PARTFUN1:def 6

      .= ( Sum ( mlt (p1,( Col (M,j))))) by A4, A17, A20

      .= (p1 "*" p2) by A1, A7, A31, A13, FINSEQ_1: 14;

    end;

    theorem :: MATRLIN2:31

    

     Th31: ( len b1) > 0 & f is additive homogeneous implies (( LineVec2Mx (v1 |-- b1)) * ( AutMt (f,b1,b2))) = ( LineVec2Mx ((f . v1) |-- b2))

    proof

      assume that

       A1: ( len b1) > 0 and

       A2: f is additive homogeneous;

      set A = ( AutMt (f,b1,b2));

      set fb = ((f . v1) |-- b2);

      set vb = (v1 |-- b1);

      set L = ( LineVec2Mx vb);

      set LA = (L * A);

      set Lf = ( LineVec2Mx fb);

      

       A3: ( len A) = ( len b1) by MATRLIN:def 8;

      ( len fb) = ( len b2) by MATRLIN:def 7;

      then

       A4: ( width Lf) = ( len b2) by MATRIX_0: 23;

      

       A5: ( len vb) = ( len b1) by MATRLIN:def 7;

      then

       A6: ( width L) = ( len b1) by MATRIX_0: 23;

      ( len L) = 1 by MATRIX_0: 23;

      then

       A7: ( len LA) = 1 by A6, A3, MATRIX_3:def 4;

      

       A8: ( width A) = ( len b2) by A1, MATRLIN: 39;

      then

       A9: ( width LA) = ( len b2) by A6, A3, MATRIX_3:def 4;

       A10:

      now

        

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

        

         A12: ( dom LA) = ( Seg 1) by A7, FINSEQ_1:def 3;

        

         A13: ( len (f * b1)) = ( len b1) by FINSEQ_2: 33;

        let i, j such that

         A14: [i, j] in ( Indices LA);

        

         A15: j in ( Seg ( len b2)) by A9, A14, ZFMISC_1: 87;

        i in ( dom LA) by A14, ZFMISC_1: 87;

        then

         A16: i = 1 by A12, FINSEQ_1: 2, TARSKI:def 1;

        

         A17: ( len ( Col (A,j))) = ( len A) by CARD_1:def 7;

         A18:

        now

          

           A19: ( dom (f * b1)) = ( dom b1) by A13, FINSEQ_3: 29;

          

           A20: ( dom A) = ( dom ( Col (A,j))) by A17, FINSEQ_3: 29;

          let k such that

           A21: k in ( dom ( Col (A,j)));

          

           A22: ( dom A) = ( Seg ( len A)) & (A . k) = (A /. k) by A21, A20, FINSEQ_1:def 3, PARTFUN1:def 6;

          

           A23: ( dom A) = ( dom b1) by A3, FINSEQ_3: 29;

          

          then

           A24: (f . (b1 /. k)) = (f . (b1 . k)) by A21, A20, PARTFUN1:def 6

          .= ((f * b1) . k) by A21, A20, A23, FUNCT_1: 13

          .= ((f * b1) /. k) by A21, A20, A23, A19, PARTFUN1:def 6;

          

          thus (( Col (A,j)) . k) = (A * (k,j)) by A21, A20, MATRIX_0:def 8

          .= (( Line (A,k)) . j) by A8, A15, MATRIX_0:def 7

          .= ((A /. k) . j) by A3, A21, A20, A22, MATRIX_0: 52

          .= ((((f * b1) /. k) |-- b2) . j) by A21, A20, A23, A24, MATRLIN:def 8;

        end;

        

        thus (Lf * (i,j)) = (( Line (Lf,i)) . j) by A4, A15, MATRIX_0:def 7

        .= (((f . v1) |-- b2) . j) by A16, MATRIX15: 25

        .= (((f . ( Sum ( lmlt ((v1 |-- b1),b1)))) |-- b2) . j) by MATRLIN: 35

        .= ((( Sum ( lmlt ((v1 |-- b1),(f * b1)))) |-- b2) . j) by A2, A5, MATRLIN: 18

        .= ((v1 |-- b1) "*" ( Col (A,j))) by A1, A5, A3, A11, A15, A13, A17, A18, Th30

        .= (( Line (L,1)) "*" ( Col (A,j))) by MATRIX15: 25

        .= (LA * (i,j)) by A6, A3, A14, A16, MATRIX_3:def 4;

      end;

      ( len Lf) = 1 by MATRIX_0: 23;

      hence thesis by A7, A9, A4, A10, MATRIX_0: 21;

    end;

    begin

    definition

      let K, V1, V2, b1, B2;

      let M be Matrix of ( len b1), ( len B2), K;

      :: MATRLIN2:def3

      func Mx2Tran (M,b1,B2) -> Function of V1, V2 means

      : Def3: for v be Vector of V1 holds (it . v) = ( Sum ( lmlt (( Line ((( LineVec2Mx (v |-- b1)) * M),1)),B2)));

      existence

      proof

        deffunc F( Element of V1) = ( Sum ( lmlt (( Line ((( LineVec2Mx ($1 |-- b1)) * M),1)),B2)));

        consider f be Function of V1, V2 such that

         A1: for x be Element of V1 holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Function of V1, V2 such that

         A2: for v be Vector of V1 holds (F1 . v) = ( Sum ( lmlt (( Line ((( LineVec2Mx (v |-- b1)) * M),1)),B2))) and

         A3: for v be Vector of V1 holds (F2 . v) = ( Sum ( lmlt (( Line ((( LineVec2Mx (v |-- b1)) * M),1)),B2)));

        now

          let x be object;

          assume x in the carrier of V1;

          then

          reconsider v = x as Vector of V1;

          

          thus (F1 . x) = ( Sum ( lmlt (( Line ((( LineVec2Mx (v |-- b1)) * M),1)),B2))) by A2

          .= (F2 . x) by A3;

        end;

        hence thesis by FUNCT_2: 12;

      end;

    end

    theorem :: MATRLIN2:32

    

     Th32: for M be Matrix of ( len b1), ( len b2), K st ( len b1) > 0 holds ( LineVec2Mx ((( Mx2Tran (M,b1,b2)) . v1) |-- b2)) = (( LineVec2Mx (v1 |-- b1)) * M)

    proof

      set L = ( LineVec2Mx (v1 |-- b1));

      

       A1: ( width L) = ( len (v1 |-- b1)) & ( len (v1 |-- b1)) = ( len b1) by MATRIX_0: 23, MATRLIN:def 7;

      let M be Matrix of ( len b1), ( len b2), K such that

       A2: ( len b1) > 0 ;

      

       A3: ( len M) = ( len b1) by A2, MATRIX_0: 23;

      set LM = (L * M);

      ( width M) = ( len b2) by A2, MATRIX_0: 23;

      then ( width LM) = ( len b2) by A1, A3, MATRIX_3:def 4;

      then ( len ( Line (LM,1))) = ( len b2) by CARD_1:def 7;

      then

       A4: (( Sum ( lmlt (( Line (LM,1)),b2))) |-- b2) = ( Line (LM,1)) by MATRLIN: 36;

      ( len L) = 1 by MATRIX_0: 23;

      then ( len LM) = 1 by A1, A3, MATRIX_3:def 4;

      

      hence LM = ( LineVec2Mx (( Sum ( lmlt (( Line (LM,1)),b2))) |-- b2)) by A4, MATRIX15: 25

      .= ( LineVec2Mx ((( Mx2Tran (M,b1,b2)) . v1) |-- b2)) by Def3;

    end;

    theorem :: MATRLIN2:33

    

     Th33: for M be Matrix of ( len b1), ( len B2), K st ( len b1) = 0 holds (( Mx2Tran (M,b1,B2)) . v1) = ( 0. V2)

    proof

      let M be Matrix of ( len b1), ( len B2), K such that

       A1: ( len b1) = 0 ;

      set L = ( LineVec2Mx (v1 |-- b1));

      set LM = (L * M);

      set LL = ( Line (LM,1));

      

       A2: ( width L) = ( len (v1 |-- b1)) & ( len (v1 |-- b1)) = ( len b1) by MATRIX_0: 23, MATRLIN:def 7;

      

       A3: ( len M) = ( len b1) by MATRIX_0:def 2;

      then ( width M) = 0 by A1, MATRIX_0:def 3;

      then ( width LM) = 0 by A2, A3, MATRIX_3:def 4;

      then

       A4: ( dom LL) = {} ;

      ( dom ( lmlt (LL,B2))) = (( dom LL) /\ ( dom B2)) by Lm1;

      then ( lmlt (LL,B2)) = ( <*> the carrier of V2) by A4;

      then ( Sum ( lmlt (LL,B2))) = ( 0. V2) by RLVECT_1: 43;

      hence thesis by Def3;

    end;

    

     Lm5: for A,B be Matrix of K st ( width A) = ( width B) holds for i st 1 <= i & i <= ( len A) holds ( Line ((A + B),i)) = (( Line (A,i)) + ( Line (B,i)))

    proof

      let A,B be Matrix of K such that

       A1: ( width A) = ( width B);

      let i;

      assume 1 <= i & i <= ( len A);

      then

       A2: i in ( dom A) by FINSEQ_3: 25;

      reconsider LB = ( Line (B,i)) as Element of (( width A) -tuples_on the carrier of K) by A1;

      per cases ;

        suppose ( width A) > 0 ;

        then ( width A) in ( Seg ( width A)) by FINSEQ_1: 3;

        then [i, ( width A)] in ( Indices A) by A2, ZFMISC_1: 87;

        hence thesis by A1, MATRIX_4: 59;

      end;

        suppose

         A3: ( width A) = 0 ;

        then ( len (( Line (A,i)) + LB)) = 0 ;

        then

         A4: (( Line (A,i)) + ( Line (B,i))) = {} ;

        ( width (A + B)) = 0 by A3, MATRIX_3:def 3;

        hence thesis by A4;

      end;

    end;

    registration

      let K, V1, V2, b1, B2;

      let M be Matrix of ( len b1), ( len B2), K;

      cluster ( Mx2Tran (M,b1,B2)) -> homogeneous additive;

      coherence

      proof

        set Mx = ( Mx2Tran (M,b1,B2));

        per cases ;

          suppose

           A1: ( len b1) = 0 ;

           A2:

          now

            let a be Scalar of K, v1 be Vector of V1;

            

            thus (Mx . (a * v1)) = ( 0. V2) by A1, Th33

            .= (a * ( 0. V2)) by VECTSP_1: 14

            .= (a * (Mx . v1)) by A1, Th33;

          end;

          now

            let v1,w1 be Vector of V1;

            

            thus (Mx . (v1 + w1)) = ( 0. V2) by A1, Th33

            .= (( 0. V2) + ( 0. V2)) by RLVECT_1:def 4

            .= ((Mx . v1) + ( 0. V2)) by A1, Th33

            .= ((Mx . v1) + (Mx . w1)) by A1, Th33;

          end;

          then Mx is additive homogeneous by A2, MOD_2:def 2;

          hence thesis;

        end;

          suppose

           A3: ( len b1) > 0 ;

           A4:

          now

            let v1,w1 be Vector of V1;

            set vb = (v1 |-- b1);

            set wb = (w1 |-- b1);

            set vwb = ((v1 + w1) |-- b1);

            set Lvw = ( LineVec2Mx vwb);

            set Lv = ( LineVec2Mx vb);

            set Lw = ( LineVec2Mx wb);

            set LLvw = ( Line ((Lvw * M),1));

            set LLv = ( Line ((Lv * M),1));

            set LLw = ( Line ((Lw * M),1));

            

             A5: ( len Lw) = 1 by MATRIX_0: 23;

            

             A6: ( len b1) = ( len vb) by MATRLIN:def 7;

            

             A7: ( len M) = ( len b1) by A3, MATRIX_0: 23;

            

             A8: ( width Lv) = ( len vb) by MATRIX_0: 23;

            then

             A9: ( width (Lv * M)) = ( width M) by A7, A6, MATRIX_3:def 4;

            then

             A10: ( len LLv) = ( width M) by CARD_1:def 7;

            

             A11: ( len Lv) = 1 by MATRIX_0: 23;

            then

             A12: ( len (Lv * M)) = 1 by A8, A7, A6, MATRIX_3:def 4;

            

             A13: ( len b1) = ( len wb) by MATRLIN:def 7;

            ( width Lvw) = ( len vwb) & ( len b1) = ( len vwb) by MATRIX_0: 23, MATRLIN:def 7;

            then ( width (Lvw * M)) = ( width M) by A7, MATRIX_3:def 4;

            then

             A14: ( len LLvw) = ( width M) by CARD_1:def 7;

            

             A15: ( dom ( lmlt (LLvw,B2))) = (( dom LLvw) /\ ( dom B2)) by Lm1

            .= (( dom LLv) /\ ( dom B2)) by A14, A10, FINSEQ_3: 29

            .= ( dom ( lmlt (LLv,B2))) by Lm1;

            

             A16: ( width Lw) = ( len wb) by MATRIX_0: 23;

            then

             A17: ( width (Lw * M)) = ( width M) by A7, A13, MATRIX_3:def 4;

            then

             A18: ( len LLw) = ( width M) by CARD_1:def 7;

            

             A19: ( dom ( lmlt (LLvw,B2))) = (( dom LLvw) /\ ( dom B2)) by Lm1

            .= (( dom LLw) /\ ( dom B2)) by A14, A18, FINSEQ_3: 29

            .= ( dom ( lmlt (LLw,B2))) by Lm1;

            then

             A20: ( len ( lmlt (LLvw,B2))) = ( len ( lmlt (LLw,B2))) by FINSEQ_3: 29;

            Lvw = ( LineVec2Mx (vb + wb)) by Th17

            .= (Lv + Lw) by A6, A13, MATRIX15: 27;

            then (Lvw * M) = ((Lv * M) + (Lw * M)) by A3, A11, A8, A5, A16, A7, A6, A13, MATRIX_4: 63;

            then LLvw = (LLv + LLw) by A12, A9, A17, Lm5;

            then

             A21: ( lmlt (LLvw,B2)) = (( lmlt (LLv,B2)) + ( lmlt (LLw,B2))) by Th7;

             A22:

            now

              let i be Nat such that

               A23: i in ( dom ( lmlt (LLv,B2)));

              (( lmlt (LLv,B2)) /. i) = (( lmlt (LLv,B2)) . i) & (( lmlt (LLw,B2)) /. i) = (( lmlt (LLw,B2)) . i) by A15, A19, A23, PARTFUN1:def 6;

              hence (( lmlt (LLvw,B2)) . i) = ((( lmlt (LLv,B2)) /. i) + (( lmlt (LLw,B2)) /. i)) by A21, A15, A23, FVSUM_1: 17;

            end;

            ( len ( lmlt (LLvw,B2))) = ( len ( lmlt (LLv,B2))) by A15, FINSEQ_3: 29;

            then ( Sum ( lmlt (LLvw,B2))) = (( Sum ( lmlt (LLv,B2))) + ( Sum ( lmlt (LLw,B2)))) by A20, A22, RLVECT_2: 2;

            

            hence (Mx . (v1 + w1)) = (( Sum ( lmlt (LLv,B2))) + ( Sum ( lmlt (LLw,B2)))) by Def3

            .= ((Mx . v1) + ( Sum ( lmlt (LLw,B2)))) by Def3

            .= ((Mx . v1) + (Mx . w1)) by Def3;

          end;

          now

            let a be Scalar of K, v1 be Vector of V1;

            set vb = (v1 |-- b1);

            set avb = ((a * v1) |-- b1);

            set Lav = ( LineVec2Mx avb);

            set Lv = ( LineVec2Mx vb);

            set LLav = ( Line ((Lav * M),1));

            set LLv = ( Line ((Lv * M),1));

            

             A24: ( len M) = ( len b1) by A3, MATRIX_0: 23;

            ( width Lav) = ( len avb) & ( len b1) = ( len avb) by MATRIX_0: 23, MATRLIN:def 7;

            then ( width (Lav * M)) = ( width M) by A24, MATRIX_3:def 4;

            then

             A25: ( len LLav) = ( width M) by CARD_1:def 7;

            

             A26: ( width Lv) = ( len vb) & ( len b1) = ( len vb) by MATRIX_0: 23, MATRLIN:def 7;

            then ( width (Lv * M)) = ( width M) by A24, MATRIX_3:def 4;

            then ( len LLv) = ( width M) by CARD_1:def 7;

            then

             A27: ( dom LLav) = ( dom LLv) by A25, FINSEQ_3: 29;

            Lav = ( LineVec2Mx (a * vb)) by Th18

            .= (a * Lv) by MATRIX15: 29;

            then

             A28: (Lav * M) = (a * (Lv * M)) by A24, A26, MATRIX15: 1;

            

             A29: ( dom ( lmlt (LLav,B2))) = (( dom LLav) /\ ( dom B2)) by Lm1;

            

             A30: (( dom LLv) /\ ( dom B2)) = ( dom ( lmlt (LLv,B2))) by Lm1;

            ( len Lv) = 1 by MATRIX_0: 23;

            then ( len (Lv * M)) = 1 by A24, A26, MATRIX_3:def 4;

            then

             A31: LLav = (a * LLv) by A28, MATRIXR1: 20;

             A32:

            now

              let i be Nat such that

               A33: i in ( dom ( lmlt (LLv,B2)));

              

               A34: (( lmlt (LLv,B2)) . i) = (( lmlt (LLv,B2)) /. i) by A33, PARTFUN1:def 6;

              i in ( dom LLv) by A30, A33, XBOOLE_0:def 4;

              then

               A35: (LLv . i) = (LLv /. i) by PARTFUN1:def 6;

              i in ( dom B2) by A30, A33, XBOOLE_0:def 4;

              then

               A36: (B2 . i) = (B2 /. i) by PARTFUN1:def 6;

              

               A37: i in ( dom LLav) by A27, A30, A33, XBOOLE_0:def 4;

              then

               A38: (LLav . i) = (LLav /. i) by PARTFUN1:def 6;

              

              hence (( lmlt (LLav,B2)) . i) = (the lmult of V2 . ((LLav /. i),(B2 /. i))) by A29, A27, A30, A33, A36, FUNCOP_1: 22

              .= ((a * (LLv /. i)) * (B2 /. i)) by A31, A37, A35, A38, FVSUM_1: 50

              .= (a * ((LLv /. i) * (B2 /. i))) by VECTSP_1:def 16

              .= (a * (( lmlt (LLv,B2)) /. i)) by A33, A35, A36, A34, FUNCOP_1: 22;

            end;

            ( len ( lmlt (LLav,B2))) = ( len ( lmlt (LLv,B2))) by A29, A27, A30, FINSEQ_3: 29;

            then ( Sum ( lmlt (LLav,B2))) = (a * ( Sum ( lmlt (LLv,B2)))) by A32, RLVECT_2: 67;

            

            hence (Mx . (a * v1)) = (a * ( Sum ( lmlt (LLv,B2)))) by Def3

            .= (a * (Mx . v1)) by Def3;

          end;

          then Mx is additive homogeneous by A4, MOD_2:def 2;

          hence thesis;

        end;

      end;

    end

    theorem :: MATRLIN2:34

    

     Th34: f is additive homogeneous implies ( Mx2Tran (( AutMt (f,b1,b2)),b1,b2)) = f

    proof

      assume

       A1: f is additive homogeneous;

      set A = ( AutMt (f,b1,b2));

      set M = ( Mx2Tran (A,b1,b2));

      per cases ;

        suppose

         A2: ( len b1) = 0 ;

        now

          

           A3: b1 is one-to-one by MATRLIN:def 2;

          reconsider R = ( rng b1) as Basis of V1 by MATRLIN:def 2;

          let x be object such that

           A4: x in the carrier of V1;

          

           A5: ( Seg ( len b1)) = {} by A2;

          ( dim V1) = ( card R) by VECTSP_9:def 1

          .= ( card ( dom b1)) by A3, CARD_1: 70

          .= 0 by A5, CARD_1: 27, FINSEQ_1:def 3;

          then ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

          then the carrier of V1 = {( 0. V1)} by VECTSP_4:def 3;

          then x = ( 0. V1) by A4, TARSKI:def 1;

          

          hence (f . x) = (f . (( 0. K) * ( 0. V1))) by VECTSP_1: 15

          .= (( 0. K) * (f . ( 0. V1))) by A1, MOD_2:def 2

          .= ( 0. V2) by VECTSP_1: 15

          .= (M . x) by A2, A4, Th33;

        end;

        hence thesis by FUNCT_2: 12;

      end;

        suppose

         A6: ( len b1) > 0 ;

        reconsider fb = (f * b1), Mf = (M * b1) as FinSequence;

        

         A7: ( rng b1) is Subset of V1 by FINSEQ_1:def 4;

        ( dom f) = the carrier of V1 by FUNCT_2:def 1;

        then

         A8: ( len fb) = ( len b1) by A7, FINSEQ_2: 29;

        ( dom M) = the carrier of V1 by FUNCT_2:def 1;

        then

         A9: ( len Mf) = ( len b1) by A7, FINSEQ_2: 29;

        now

          

           A10: ( dom fb) = ( dom Mf) by A8, A9, FINSEQ_3: 29;

          let i;

          assume 1 <= i & i <= ( len fb);

          then

           A11: i in ( dom fb) by FINSEQ_3: 25;

          ( dom fb) = ( dom b1) by A8, FINSEQ_3: 29;

          then

           A12: (b1 . i) = (b1 /. i) by A11, PARTFUN1:def 6;

          ( LineVec2Mx ((M . (b1 /. i)) |-- b2)) = (( LineVec2Mx ((b1 /. i) |-- b1)) * A) by A6, Th32

          .= ( LineVec2Mx ((f . (b1 /. i)) |-- b2)) by A1, A6, Th31;

          

          then ((M . (b1 /. i)) |-- b2) = ( Line (( LineVec2Mx ((f . (b1 /. i)) |-- b2)),1)) by MATRIX15: 25

          .= ((f . (b1 /. i)) |-- b2) by MATRIX15: 25;

          then (M . (b1 /. i)) = (f . (b1 /. i)) by MATRLIN: 34;

          

          hence (fb . i) = (M . (b1 /. i)) by A11, A12, FUNCT_1: 12

          .= (Mf . i) by A11, A10, A12, FUNCT_1: 12;

        end;

        hence thesis by A1, A6, A8, A9, FINSEQ_1: 14, MATRLIN: 22;

      end;

    end;

    theorem :: MATRLIN2:35

    

     Th35: for A,B be Matrix of K st i in ( dom A) & ( width A) = ( len B) holds (( LineVec2Mx ( Line (A,i))) * B) = ( LineVec2Mx ( Line ((A * B),i)))

    proof

      let A,B be Matrix of K such that

       A1: i in ( dom A) and

       A2: ( width A) = ( len B);

      

       A3: ( width (A * B)) = ( width B) by A2, MATRIX_3:def 4;

      set LAB = ( LineVec2Mx ( Line ((A * B),i)));

      

       A4: ( width LAB) = ( len ( Line ((A * B),i))) & ( len ( Line ((A * B),i))) = ( width (A * B)) by CARD_1:def 7, MATRIX_0: 23;

      set L = ( LineVec2Mx ( Line (A,i)));

      

       A5: ( width L) = ( len ( Line (A,i))) & ( len ( Line (A,i))) = ( width A) by CARD_1:def 7, MATRIX_0: 23;

      then

       A6: ( width (L * B)) = ( width B) by A2, MATRIX_3:def 4;

      ( len L) = 1 by CARD_1:def 7;

      then

       A7: ( len (L * B)) = 1 by A2, A5, MATRIX_3:def 4;

      ( len (A * B)) = ( len A) by A2, MATRIX_3:def 4;

      then

       A8: ( dom A) = ( dom (A * B)) by FINSEQ_3: 29;

       A9:

      now

        let j, k such that

         A10: [j, k] in ( Indices (L * B));

        

         A11: k in ( Seg ( width (A * B))) by A3, A6, A10, ZFMISC_1: 87;

        then

         A12: [i, k] in ( Indices (A * B)) by A1, A8, ZFMISC_1: 87;

        ( Indices (L * B)) = [:( Seg 1), ( Seg ( width B)):] by A7, A6, FINSEQ_1:def 3;

        then j in ( Seg 1) by A10, ZFMISC_1: 87;

        then

         A13: j = 1 by FINSEQ_1: 2, TARSKI:def 1;

        

        hence ((L * B) * (j,k)) = (( Line (L,1)) "*" ( Col (B,k))) by A2, A5, A10, MATRIX_3:def 4

        .= (( Line (A,i)) "*" ( Col (B,k))) by MATRIX15: 25

        .= ((A * B) * (i,k)) by A2, A12, MATRIX_3:def 4

        .= (( Line ((A * B),i)) . k) by A11, MATRIX_0:def 7

        .= (( Line (LAB,j)) . k) by A13, MATRIX15: 25

        .= (LAB * (j,k)) by A4, A11, MATRIX_0:def 7;

      end;

      ( len LAB) = 1 by CARD_1:def 7;

      hence thesis by A4, A3, A7, A6, A9, MATRIX_0: 21;

    end;

    theorem :: MATRLIN2:36

    

     Th36: for M be Matrix of ( len b1), ( len b2), K holds ( AutMt (( Mx2Tran (M,b1,b2)),b1,b2)) = M

    proof

      let M be Matrix of ( len b1), ( len b2), K;

      set MX = ( Mx2Tran (M,b1,b2));

      set A = ( AutMt (MX,b1,b2));

      set ONE = ( 1. (K,( len b1)));

      

       A1: ( len M) = ( len b1) by MATRIX_0: 25;

      

       A2: ( len A) = ( len b1) by MATRIX_0: 25;

      

       A3: ( len ONE) = ( len b1) by MATRIX_0: 24;

      now

        let i such that

         A4: 1 <= i & i <= ( len M);

        

         A5: i in ( Seg ( len b1)) by A1, A4;

        

         A6: i in ( dom ONE) by A1, A3, A4, FINSEQ_3: 25;

        reconsider Ai = (A /. i) as FinSequence of K by FINSEQ_1:def 11;

        

         A7: i in ( dom b1) by A1, A4, FINSEQ_3: 25;

        then (A /. i) = ((MX . (b1 /. i)) |-- b2) by MATRLIN:def 8;

        

        then ( LineVec2Mx Ai qua FinSequence of K) = (( LineVec2Mx ((b1 /. i) |-- b1)) * M) by A1, A4, Th32

        .= (( LineVec2Mx ( Line (ONE,i))) * M) by A7, Th19

        .= ( LineVec2Mx ( Line ((ONE * M),i))) by A1, A6, Th35, MATRIX_0: 24

        .= ( LineVec2Mx ( Line (M,i))) by A1, MATRIXR2: 68;

        

        then

         A8: Ai = ( Line (( LineVec2Mx ( Line (M,i))),1)) by MATRIX15: 25

        .= ( Line (M,i)) by MATRIX15: 25

        .= (M . i) by A5, MATRIX_0: 52;

        i in ( dom A) by A1, A2, A4, FINSEQ_3: 25;

        hence (M . i) = (A . i) by A8, PARTFUN1:def 6;

      end;

      hence thesis by A2, FINSEQ_1: 14, MATRIX_0: 25;

    end;

    definition

      let n, m, K;

      let A be Matrix of n, m, K;

      let B be Matrix of K;

      :: original: +

      redefine

      func A + B -> Matrix of n, m, K ;

      coherence

      proof

        

         A1: ( width (A + B)) = ( width A) & ( len A) = n by MATRIX_0:def 2, MATRIX_3:def 3;

        

         A2: ( len (A + B)) = ( len A) by MATRIX_3:def 3;

        per cases ;

          suppose

           A3: n = 0 ;

          then (A + B) = {} by A2, MATRIX_0:def 2;

          hence thesis by A3, MATRIX_0: 13;

        end;

          suppose n > 0 ;

          then ( width A) = m by MATRIX_0: 23;

          hence thesis by A2, A1, MATRIX_0: 51;

        end;

      end;

    end

    theorem :: MATRLIN2:37

    for A,B be Matrix of ( len b1), ( len B2), K holds ( Mx2Tran ((A + B),b1,B2)) = (( Mx2Tran (A,b1,B2)) + ( Mx2Tran (B,b1,B2)))

    proof

      let A,B be Matrix of ( len b1), ( len B2), K;

      set AB = (A + B);

      set M = ( Mx2Tran ((A + B),b1,B2));

      set MA = ( Mx2Tran (A,b1,B2));

      set MB = ( Mx2Tran (B,b1,B2));

      now

        let x be object such that

         A1: x in the carrier of V1;

        reconsider v = x as Element of V1 by A1;

        now

          per cases ;

            suppose

             A2: ( len b1) = 0 ;

            

            hence (M . x) = ( 0. V2) by A1, Th33

            .= (( 0. V2) + ( 0. V2)) by RLVECT_1:def 4

            .= ((MA . v) + ( 0. V2)) by A2, Th33

            .= ((MA . v) + (MB . v)) by A2, Th33

            .= ((MA + MB) . x) by MATRLIN:def 3;

          end;

            suppose

             A3: ( len b1) > 0 ;

            set L = ( LineVec2Mx (v |-- b1));

            

             A4: ( width L) = ( len (v |-- b1)) & ( len (v |-- b1)) = ( len b1) by MATRIX_0: 23, MATRLIN:def 7;

            set mB = ( lmlt (( Line ((L * B),1)),B2));

            

             A5: ( len B) = ( len b1) & ( width B) = ( len B2) by A3, MATRIX_0: 23;

            then

             A6: ( width (L * B)) = ( len B2) by A4, MATRIX_3:def 4;

            then ( len ( Line ((L * B),1))) = ( len B2) by CARD_1:def 7;

            then ( dom ( Line ((L * B),1))) = ( dom B2) by FINSEQ_3: 29;

            then

             A7: ( dom mB) = ( dom B2) by MATRLIN: 12;

            then

             A8: ( len mB) = ( len B2) by FINSEQ_3: 29;

            

             A9: ( len A) = ( len b1) by A3, MATRIX_0: 23;

            

             A10: ( len L) = 1 by MATRIX_0: 23;

            then

             A11: ( len (L * A)) = 1 by A9, A4, MATRIX_3:def 4;

            set mA = ( lmlt (( Line ((L * A),1)),B2));

            

             A12: ( width A) = ( len B2) by A3, MATRIX_0: 23;

            then

             A13: ( width (L * A)) = ( len B2) by A9, A4, MATRIX_3:def 4;

            then ( len ( Line ((L * A),1))) = ( len B2) by CARD_1:def 7;

            then ( dom ( Line ((L * A),1))) = ( dom B2) by FINSEQ_3: 29;

            then

             A14: ( dom mA) = ( dom B2) by MATRLIN: 12;

            then

             A15: ( len mA) = ( len B2) by FINSEQ_3: 29;

            

             A16: ( dom (mA + mB)) = (( dom B2) /\ ( dom B2)) by A14, A7, Lm3

            .= ( dom B2);

            then

             A17: ( len (mA + mB)) = ( len B2) by FINSEQ_3: 29;

             A18:

            now

              let k be Nat such that

               A19: k in ( dom mA);

              (mA /. k) = (mA . k) & (mB /. k) = (mB . k) by A14, A7, A19, PARTFUN1:def 6;

              hence ((mA + mB) . k) = ((mA /. k) + (mB /. k)) by A14, A16, A19, FVSUM_1: 17;

            end;

            

            thus (M . x) = ( Sum ( lmlt (( Line ((L * AB),1)),B2))) by Def3

            .= ( Sum ( lmlt (( Line (((L * A) + (L * B)),1)),B2))) by A3, A10, A9, A12, A5, A4, MATRIX_4: 62

            .= ( Sum ( lmlt ((( Line ((L * A),1)) + ( Line ((L * B),1))),B2))) by A11, A13, A6, Lm5

            .= ( Sum (mA + mB)) by Th7

            .= (( Sum mA) + ( Sum mB)) by A15, A8, A17, A18, RLVECT_2: 2

            .= ((MA . v) + ( Sum mB)) by Def3

            .= ((MA . v) + (MB . v)) by Def3

            .= ((MA + MB) . x) by MATRLIN:def 3;

          end;

        end;

        hence (M . x) = ((MA + MB) . x);

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MATRLIN2:38

    for A be Matrix of ( len b1), ( len B2), K holds (a * ( Mx2Tran (A,b1,B2))) = ( Mx2Tran ((a * A),b1,B2))

    proof

      let A be Matrix of ( len b1), ( len B2), K;

      set aA = (a * A);

      set aM = ( Mx2Tran (aA,b1,B2));

      set M = ( Mx2Tran (A,b1,B2));

      now

        let x be object;

        assume x in the carrier of V1;

        then

        reconsider v = x as Element of V1;

        set L = ( LineVec2Mx (v |-- b1));

        set amA = ( lmlt ((a * ( Line ((L * A),1))),B2));

        set mA = ( lmlt (( Line ((L * A),1)),B2));

        

         A1: ( width L) = ( len (v |-- b1)) & ( len (v |-- b1)) = ( len b1) by MATRIX_0: 23, MATRLIN:def 7;

        

         A2: ( len A) = ( len b1) by MATRIX_0:def 2;

        ( len L) = 1 by MATRIX_0: 23;

        then

         A3: ( len (L * A)) = 1 by A1, A2, MATRIX_3:def 4;

        

         A4: ( dom mA) = (( dom ( Line ((L * A),1))) /\ ( dom B2)) by Lm1;

        ( len (a * ( Line ((L * A),1)))) = ( len ( Line ((L * A),1))) by MATRIXR1: 16;

        then

         A5: ( dom (a * ( Line ((L * A),1)))) = ( dom ( Line ((L * A),1))) by FINSEQ_3: 29;

        

         A6: ( dom amA) = (( dom (a * ( Line ((L * A),1)))) /\ ( dom B2)) by Lm1;

        then

         A7: ( len mA) = ( len amA) by A5, A4, FINSEQ_3: 29;

         A8:

        now

          let k be Nat such that

           A9: k in ( dom mA);

          

           A10: (mA . k) = (mA /. k) by A9, PARTFUN1:def 6;

          k in ( dom ( Line ((L * A),1))) by A4, A9, XBOOLE_0:def 4;

          then

           A11: (( Line ((L * A),1)) . k) = (( Line ((L * A),1)) /. k) by PARTFUN1:def 6;

          k in ( dom B2) by A4, A9, XBOOLE_0:def 4;

          then

           A12: (B2 . k) = (B2 /. k) by PARTFUN1:def 6;

          k in ( dom (a * ( Line ((L * A),1)))) by A5, A4, A9, XBOOLE_0:def 4;

          then ((a * ( Line ((L * A),1))) . k) = (a * (( Line ((L * A),1)) /. k)) by A11, FVSUM_1: 50;

          

          hence (amA . k) = ((a * (( Line ((L * A),1)) /. k)) * (B2 /. k)) by A6, A5, A4, A9, A12, FUNCOP_1: 22

          .= (a * ((( Line ((L * A),1)) /. k) * (B2 /. k))) by VECTSP_1:def 16

          .= (a * (mA /. k)) by A9, A11, A12, A10, FUNCOP_1: 22;

        end;

        

        thus (aM . x) = ( Sum ( lmlt (( Line ((L * aA),1)),B2))) by Def3

        .= ( Sum ( lmlt (( Line ((a * (L * A)),1)),B2))) by A1, A2, MATRIXR1: 22

        .= ( Sum amA) by A3, MATRIXR1: 20

        .= (a * ( Sum mA)) by A7, A8, RLVECT_2: 67

        .= (a * (M . v)) by Def3

        .= ((a * M) . x) by MATRLIN:def 4;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MATRLIN2:39

    for A,B be Matrix of ( len b1), ( len b2), K st ( Mx2Tran (A,b1,b2)) = ( Mx2Tran (B,b1,b2)) holds A = B

    proof

      let A,B be Matrix of ( len b1), ( len b2), K;

      assume ( Mx2Tran (A,b1,b2)) = ( Mx2Tran (B,b1,b2));

      

      hence A = ( AutMt (( Mx2Tran (B,b1,b2)),b1,b2)) by Th36

      .= B by Th36;

    end;

    theorem :: MATRLIN2:40

    for A be Matrix of ( len b1), ( len b2), K holds for B be Matrix of ( len b2), ( len B3), K st ( width A) = ( len B) holds for AB be Matrix of ( len b1), ( len B3), K st AB = (A * B) holds ( Mx2Tran (AB,b1,B3)) = (( Mx2Tran (B,b2,B3)) * ( Mx2Tran (A,b1,b2)))

    proof

      let A be Matrix of ( len b1), ( len b2), K;

      let B be Matrix of ( len b2), ( len B3), K such that

       A1: ( width A) = ( len B);

      set MB = ( Mx2Tran (B,b2,B3));

      set MA = ( Mx2Tran (A,b1,b2));

      let AB be Matrix of ( len b1), ( len B3), K such that

       A2: AB = (A * B);

      set MAB = ( Mx2Tran (AB,b1,B3));

      now

        let x be object;

        assume x in the carrier of V1;

        then

        reconsider v = x as Element of V1;

        set L = ( LineVec2Mx (v |-- b1));

        

         A3: ( len A) = ( len b1) by MATRIX_0:def 2;

        

         A4: ( width L) = ( len (v |-- b1)) & ( len (v |-- b1)) = ( len b1) by MATRIX_0: 23, MATRLIN:def 7;

        then ( len L) = 1 & ( len (L * A)) = ( len L) by A3, MATRIX_0: 23, MATRIX_3:def 4;

        then

         A5: ( dom (L * A)) = ( Seg 1) by FINSEQ_1:def 3;

        

         A6: ( width (L * A)) = ( width A) by A4, A3, MATRIX_3:def 4;

        then

         A7: ( len B) = ( len b2) & ( len ( Line ((L * A),1))) = ( width A) by CARD_1:def 7, MATRIX_0:def 2;

        

         A8: 1 in ( Seg 1);

        ( dom (MB * MA)) = the carrier of V1 by FUNCT_2:def 1;

        

        hence ((MB * MA) . x) = (MB . (MA . v)) by FUNCT_1: 12

        .= (MB . ( Sum ( lmlt (( Line ((L * A),1)),b2)))) by Def3

        .= ( Sum ( lmlt (( Line ((( LineVec2Mx (( Sum ( lmlt (( Line ((L * A),1)),b2))) |-- b2)) * B),1)),B3))) by Def3

        .= ( Sum ( lmlt (( Line ((( LineVec2Mx ( Line ((L * A),1))) * B),1)),B3))) by A1, A7, MATRLIN: 36

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line (((L * A) * B),1))),1)),B3))) by A1, A6, A5, A8, Th35

        .= ( Sum ( lmlt (( Line (( LineVec2Mx ( Line ((L * AB),1))),1)),B3))) by A1, A2, A4, A3, MATRIX_3: 33

        .= ( Sum ( lmlt (( Line ((L * AB),1)),B3))) by MATRIX15: 25

        .= (MAB . x) by Def3;

      end;

      hence thesis by FUNCT_2: 12;

    end;

    theorem :: MATRLIN2:41

    

     Th41: for A be Matrix of ( len b1), ( len b2), K st ( len b1) > 0 & ( len b2) > 0 holds v1 in ( ker ( Mx2Tran (A,b1,b2))) iff (v1 |-- b1) in ( Space_of_Solutions_of (A @ ))

    proof

      let A be Matrix of ( len b1), ( len b2), K such that

       A1: ( len b1) > 0 and

       A2: ( len b2) > 0 ;

      set AT = (A @ );

      

       A3: ( width A) = ( len b2) by A1, MATRIX_0: 23;

      then

       A4: ( len AT) = ( len b2) by A2, MATRIX_0: 54;

      set L = ( LineVec2Mx (v1 |-- b1));

      set M = ( Mx2Tran (A,b1,b2));

      set SA = ( Space_of_Solutions_of AT);

      

       A5: ( width L) = ( len (v1 |-- b1)) by MATRIX_0: 23;

      ( len (( len b2) |-> ( 0. K))) = ( len b2) by CARD_1:def 7;

      then

       A6: ( width ( LineVec2Mx (( len b2) |-> ( 0. K)))) = ( len b2) by MATRIX_0: 23;

      

       A7: ( width ( ColVec2Mx (( len b2) |-> ( 0. K)))) = 1 by A2, MATRIX_0: 23;

      

       A8: ( len (v1 |-- b1)) = ( len b1) by MATRLIN:def 7;

      then

       A9: ( len ( ColVec2Mx (v1 |-- b1))) = ( len (v1 |-- b1)) & ( width ( ColVec2Mx (v1 |-- b1))) = 1 by A1, MATRIX_0: 23;

      

       A10: ( len A) = ( len b1) by A1, MATRIX_0: 23;

      then

       A11: ( width AT) = 0 implies ( len AT) = 0 by A1, A2, A3, MATRIX_0: 54;

      

       A12: ( width AT) = ( len b1) by A2, A10, A3, MATRIX_0: 54;

      thus v1 in ( ker M) implies (v1 |-- b1) in SA

      proof

        assume v1 in ( ker M);

        then (M . v1) = ( 0. V2) by RANKNULL: 10;

        

        then (L * A) = ( LineVec2Mx (( 0. V2) |-- b2)) by A1, Th32

        .= ( LineVec2Mx (( len b2) |-> ( 0. K))) by Th20;

        then ( ColVec2Mx (( len b2) |-> ( 0. K))) = (AT * ( ColVec2Mx (v1 |-- b1))) by A2, A10, A3, A5, A8, MATRIX_3: 22;

        then ( ColVec2Mx (v1 |-- b1)) in ( Solutions_of (AT,( ColVec2Mx (( len b2) |-> ( 0. K))))) by A12, A8, A9, A7;

        then (v1 |-- b1) in ( Solutions_of (AT,(( len b2) |-> ( 0. K))));

        then (v1 |-- b1) in the carrier of SA by A4, A11, MATRIX15:def 5;

        hence thesis;

      end;

      assume (v1 |-- b1) in SA;

      then (v1 |-- b1) in the carrier of SA;

      then (v1 |-- b1) in ( Solutions_of (AT,(( len b2) |-> ( 0. K)))) by A4, A11, MATRIX15:def 5;

      then ex f be FinSequence of K st f = (v1 |-- b1) & ( ColVec2Mx f) in ( Solutions_of (AT,( ColVec2Mx (( len b2) |-> ( 0. K)))));

      then ex X be Matrix of K st X = ( ColVec2Mx (v1 |-- b1)) & ( len X) = ( width AT) & ( width X) = ( width ( ColVec2Mx (( len b2) |-> ( 0. K)))) & ( ColVec2Mx (( len b2) |-> ( 0. K))) = (AT * X);

      then

       A13: ( ColVec2Mx (( len b2) |-> ( 0. K))) = ((L * A) @ ) by A2, A10, A3, A5, A8, MATRIX_3: 22;

      ( width (L * A)) = ( width A) by A10, A5, A8, MATRIX_3:def 4;

      

      then (L * A) = ( LineVec2Mx (( len b2) |-> ( 0. K))) by A2, A3, A6, A13, MATRIX_0: 56

      .= ( LineVec2Mx (( 0. V2) |-- b2)) by Th20;

      then ( LineVec2Mx (( 0. V2) |-- b2)) = ( LineVec2Mx ((M . v1) |-- b2)) by A1, Th32;

      

      then (( 0. V2) |-- b2) = ( Line (( LineVec2Mx ((M . v1) |-- b2)),1)) by MATRIX15: 25

      .= ((M . v1) |-- b2) by MATRIX15: 25;

      then (M . v1) = ( 0. V2) by MATRLIN: 34;

      hence thesis by RANKNULL: 10;

    end;

    theorem :: MATRLIN2:42

    

     Th42: V1 is trivial iff ( dim V1) = 0

    proof

      hereby

        assume

         A1: V1 is trivial;

        the carrier of V1 c= {( 0. V1)}

        proof

          let x be object;

          assume

           A2: x in the carrier of V1;

          x = ( 0. V1) by A1, A2;

          hence thesis by TARSKI:def 1;

        end;

        

        then the carrier of ( (Omega). V1) = {( 0. V1)} by ZFMISC_1: 33

        .= the carrier of ( (0). V1) by VECTSP_4:def 3;

        then ( (Omega). V1) = ( (0). V1) by VECTSP_4: 29;

        hence ( dim V1) = 0 by VECTSP_9: 29;

      end;

      assume ( dim V1) = 0 ;

      then

       A3: ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

      for v1 holds v1 = ( 0. V1) by VECTSP_4: 35, A3, STRUCT_0:def 5;

      hence thesis;

    end;

    theorem :: MATRLIN2:43

    

     Th43: for V1,V2 be VectSp of K holds for f be linear-transformation of V1, V2 holds f is one-to-one iff ( ker f) = ( (0). V1)

    proof

      let V1,V2 be VectSp of K;

      let f be linear-transformation of V1, V2;

      ( ker f) = ( (0). V1) implies f is one-to-one

      proof

        assume

         A1: ( ker f) = ( (0). V1);

        let x,y be object such that

         A2: x in ( dom f) & y in ( dom f) and

         A3: (f . x) = (f . y);

        reconsider x9 = x, y9 = y as Element of V1 by A2, FUNCT_2:def 1;

        (x9 - y9) in ( ker f) by A3, RANKNULL: 17;

        then (x9 - y9) in the carrier of ( (0). V1) by A1;

        then (x9 - y9) in {( 0. V1)} by VECTSP_4:def 3;

        then (x9 + ( - y9)) = ( 0. V1) by TARSKI:def 1;

        

        hence x = ( - ( - y9)) by VECTSP_1: 16

        .= y by RLVECT_1: 17;

      end;

      hence thesis by RANKNULL: 15;

    end;

    registration

      let K;

      let V1,V2 be VectSp of K;

      let f,g be linear-transformation of V1, V2;

      cluster (f + g) -> homogeneous additive;

      coherence

      proof

         A1:

        now

          let a be Scalar of K, v1 be Vector of V1;

          

          thus ((f + g) . (a * v1)) = ((f . (a * v1)) + (g . (a * v1))) by MATRLIN:def 3

          .= ((a * (f . v1)) + (g . (a * v1))) by MOD_2:def 2

          .= ((a * (f . v1)) + (a * (g . v1))) by MOD_2:def 2

          .= (a * ((f . v1) + (g . v1))) by VECTSP_1:def 14

          .= (a * ((f + g) . v1)) by MATRLIN:def 3;

        end;

        now

          let v1,w1 be Vector of V1;

          

          thus ((f + g) . (v1 + w1)) = ((f . (v1 + w1)) + (g . (v1 + w1))) by MATRLIN:def 3

          .= (((f . v1) + (f . w1)) + (g . (v1 + w1))) by VECTSP_1:def 20

          .= (((f . v1) + (f . w1)) + ((g . v1) + (g . w1))) by VECTSP_1:def 20

          .= ((f . v1) + ((f . w1) + ((g . v1) + (g . w1)))) by RLVECT_1:def 3

          .= ((f . v1) + ((g . v1) + ((g . w1) + (f . w1)))) by RLVECT_1:def 3

          .= (((f . v1) + (g . v1)) + ((f . w1) + (g . w1))) by RLVECT_1:def 3

          .= (((f + g) . v1) + ((f . w1) + (g . w1))) by MATRLIN:def 3

          .= (((f + g) . v1) + ((f + g) . w1)) by MATRLIN:def 3;

        end;

        then (f + g) is additive homogeneous by A1, MOD_2:def 2;

        hence thesis;

      end;

    end

    registration

      let K;

      let V1,V2 be VectSp of K;

      let f be linear-transformation of V1, V2, a;

      cluster (a * f) -> homogeneous additive;

      coherence

      proof

         A1:

        now

          let b be Scalar of K, v1 be Vector of V1;

          

          thus ((a * f) . (b * v1)) = (a * (f . (b * v1))) by MATRLIN:def 4

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

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

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

          .= (b * ((a * f) . v1)) by MATRLIN:def 4;

        end;

        now

          let v1,w1 be Vector of V1;

          

          thus ((a * f) . (v1 + w1)) = (a * (f . (v1 + w1))) by MATRLIN:def 4

          .= (a * ((f . v1) + (f . w1))) by VECTSP_1:def 20

          .= ((a * (f . v1)) + (a * (f . w1))) by VECTSP_1:def 14

          .= (((a * f) . v1) + (a * (f . w1))) by MATRLIN:def 4

          .= (((a * f) . v1) + ((a * f) . w1)) by MATRLIN:def 4;

        end;

        then (a * f) is additive homogeneous by A1, MOD_2:def 2;

        hence thesis;

      end;

    end

    definition

      let K;

      let V1,V2,V3 be VectSp of K;

      let f1 be linear-transformation of V1, V2;

      let f2 be linear-transformation of V2, V3;

      :: original: *

      redefine

      func f2 * f1 -> linear-transformation of V1, V3 ;

      coherence by MOD_2: 2;

    end

    theorem :: MATRLIN2:44

    

     Th44: for A be Matrix of ( len b1), ( len b2), K st ( the_rank_of A) = ( len b1) holds ( Mx2Tran (A,b1,b2)) is one-to-one

    proof

      let A be Matrix of ( len b1), ( len b2), K such that

       A1: ( the_rank_of A) = ( len b1);

      set S = ( Space_of_Solutions_of (A @ ));

      set M = ( Mx2Tran (A,b1,b2));

       A2:

      now

        per cases ;

          suppose ( len b1) = 0 ;

          then ( dim V1) = 0 by Th21;

          then

           A3: ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

          the carrier of ( ker M) c= the carrier of V1 by VECTSP_4:def 2;

          hence the carrier of ( ker M) c= {( 0. V1)} by A3, VECTSP_4:def 3;

        end;

          suppose

           A4: ( len b1) > 0 ;

          

           A5: ( len b1) <= ( width A) by A1, MATRIX13: 74;

          then

           A6: ( width (A @ )) = ( len A) by A4, MATRIX_0: 54;

          

           A7: ( len A) = ( len b1) by A4, MATRIX_0: 23;

          

           A8: ( width A) = ( len b2) by A4, MATRIX_0: 23;

          thus the carrier of ( ker M) c= {( 0. V1)}

          proof

            let x be object such that

             A9: x in the carrier of ( ker M);

            the carrier of ( ker M) c= the carrier of V1 by VECTSP_4:def 2;

            then

            reconsider v = x as Element of V1 by A9;

            ( dim S) = (( len b1) - ( the_rank_of (A @ ))) by A4, A7, A6, MATRIX15: 68

            .= (( len b1) - ( len b1)) by A1, MATRIX13: 84

            .= 0 ;

            then

             A10: ( (Omega). S) = ( (0). S) by VECTSP_9: 29;

            v in ( ker M) by A9;

            then (v |-- b1) in S by A4, A8, A5, Th41;

            then (v |-- b1) in the carrier of ( (0). S) by A10;

            then (v |-- b1) in the carrier of ( (0). (( len b1) -VectSp_over K)) by A7, A6, VECTSP_4: 36;

            then (v |-- b1) in {( 0. (( len b1) -VectSp_over K))} by VECTSP_4:def 3;

            

            then (v |-- b1) = ( 0. (( len b1) -VectSp_over K)) by TARSKI:def 1

            .= (( len b1) |-> ( 0. K)) by MATRIX13: 102

            .= (( 0. V1) |-- b1) by Th20;

            then v = ( 0. V1) by MATRLIN: 34;

            hence thesis by TARSKI:def 1;

          end;

        end;

      end;

      ( 0. V1) in ( ker M) by RANKNULL: 11;

      then ( 0. V1) in the carrier of ( ker M);

      then {( 0. V1)} c= the carrier of ( ker M) by ZFMISC_1: 31;

      

      then the carrier of ( ker M) = {( 0. V1)} by A2, XBOOLE_0:def 10

      .= the carrier of ( (0). V1) by VECTSP_4:def 3;

      then ( ker M) = ( (0). V1) by VECTSP_4: 29;

      hence thesis by Th43;

    end;

    

     Lm6: ( the_rank_of ( 1. (K,n))) = n

    proof

      

       A1: ( 1_ K) <> ( 0. K);

      (n + 0 ) > 0 or n = 0 ;

      then

       A2: n >= 1 or n = 0 by NAT_1: 19;

      ( Det ( 1. (K,n))) = ( 1_ K) by A2, MATRIXR2: 41, MATRIX_7: 16;

      hence thesis by A1, MATRIX13: 83;

    end;

    theorem :: MATRLIN2:45

    

     Th45: ( MX2FinS ( 1. (K,n))) is OrdBasis of (n -VectSp_over K)

    proof

      set ONE = ( 1. (K,n));

      

       A1: ( the_rank_of ONE) = n by Lm6;

      then

       A2: ONE is one-to-one by MATRIX13: 105;

      for i, j st [i, j] in ( Indices ONE) & (ONE * (i,j)) <> ( 0. K) holds i = j by MATRIX_1:def 3;

      then ONE is diagonal by MATRIX_1:def 6;

      then ( lines ONE) is Basis of (n -VectSp_over K) by A1, MATRIX13: 111;

      hence thesis by A2, MATRLIN:def 2;

    end;

    theorem :: MATRLIN2:46

    

     Th46: for M be OrdBasis of (( len b2) -VectSp_over K) st M = ( MX2FinS ( 1. (K,( len b2)))) holds for v1 be Vector of (( len b2) -VectSp_over K) holds (v1 |-- M) = v1

    proof

      let M be OrdBasis of (( len b2) -VectSp_over K) such that

       A1: M = ( MX2FinS ( 1. (K,( len b2))));

      let v1 be Vector of (( len b2) -VectSp_over K);

      set vM = (v1 |-- M);

      consider KL be Linear_Combination of (( len b2) -VectSp_over K) such that

       A2: v1 = ( Sum KL) & ( Carrier KL) c= ( rng M) and

       A3: for k st 1 <= k & k <= ( len (v1 |-- M)) holds (vM /. k) = (KL . (M /. k)) by MATRLIN:def 7;

      reconsider t1 = v1 as Element of (( len b2) -tuples_on the carrier of K) by MATRIX13: 102;

      

       A4: ( len t1) = ( len b2) by CARD_1:def 7;

      

       A5: ( len M) = ( dim (( len b2) -VectSp_over K)) & ( dim (( len b2) -VectSp_over K)) = ( len b2) by Th21, MATRIX13: 112;

      

       A6: ( len vM) = ( len M) by MATRLIN:def 7;

      now

        

         A7: ( dom M) = ( dom vM) by A6, FINSEQ_3: 29;

        

         A8: ( the_rank_of ( 1. (K,( len b2)))) = ( len b2) by Lm6;

        set F = ( FinS2MX (KL (#) M));

        

         A9: ( Indices ( 1. (K,( len b2)))) = [:( Seg ( len b2)), ( Seg ( len b2)):] by MATRIX_0: 24;

        let i such that

         A10: 1 <= i & i <= ( len t1);

        

         A11: i in ( Seg ( len b2)) by A4, A10;

        then

         A12: [i, i] in [:( Seg ( len b2)), ( Seg ( len b2)):] by ZFMISC_1: 87;

        

         A13: ( width ( 1. (K,( len b2)))) = ( len b2) by MATRIX_0: 24;

        

        then

         A14: (( Line (( 1. (K,( len b2))),i)) . i) = (( 1. (K,( len b2))) * (i,i)) by A11, MATRIX_0:def 7

        .= ( 1_ K) by A9, A12, MATRIX_1:def 3;

        

         A15: ( len ( Col (F,i))) = ( len F) by CARD_1:def 7;

        then

         A16: ( dom ( Col (F,i))) = ( dom F) by FINSEQ_3: 29;

        

         A17: ( len F) = ( len M) by VECTSP_6:def 5;

        then

         A18: ( dom F) = ( dom M) by FINSEQ_3: 29;

        

         A19: i in ( dom ( Col (F,i))) by A4, A5, A10, A17, A15, FINSEQ_3: 25;

        

         A20: ( width F) = ( len b2) by A5, A17, MATRIX_0: 24;

        now

          let j such that

           A21: j in ( dom ( Col (F,i))) and

           A22: j <> i;

          

           A23: ( dom ( Col (F,i))) = ( Seg ( len b2)) by A5, A17, A15, FINSEQ_1:def 3;

          then

           A24: [j, i] in [:( Seg ( len b2)), ( Seg ( len b2)):] by A11, A21, ZFMISC_1: 87;

          

           A25: ( Line (F,j)) = ((KL (#) M) . j) by A5, A17, A21, A23, MATRIX_0: 52

          .= ((KL . (M /. j)) * (M /. j)) by A16, A21, VECTSP_6:def 5;

          

           A26: (( Col (F,i)) . j) = (F * (j,i)) by A16, A21, MATRIX_0:def 8

          .= (( Line (F,j)) . i) by A11, A20, MATRIX_0:def 7;

          

           A27: (( Line (( 1. (K,( len b2))),j)) . i) = (( 1. (K,( len b2))) * (j,i)) by A11, A13, MATRIX_0:def 7

          .= ( 0. K) by A9, A22, A24, MATRIX_1:def 3;

          (M /. j) = (M . j) by A16, A18, A21, PARTFUN1:def 6

          .= ( Line (( 1. (K,( len b2))),j)) by A1, A21, A23, MATRIX_0: 52;

          

          hence (( Col (F,i)) . j) = (((KL . (M /. j)) * ( Line (( 1. (K,( len b2))),j))) . i) by A13, A26, A25, MATRIX13: 102

          .= ((KL . (M /. j)) * ( 0. K)) by A11, A13, A27, FVSUM_1: 51

          .= ( 0. K);

        end;

        

        then

         A28: (( Col (F,i)) . i) = ( Sum ( Col (F,i))) by A19, MATRIX_3: 12

        .= (v1 . i) by A1, A2, A11, A8, MATRIX13: 105, MATRIX13: 107;

        

         A29: ( Line (F,i)) = ((KL (#) M) . i) by A5, A11, A17, MATRIX_0: 52

        .= ((KL . (M /. i)) * (M /. i)) by A19, A16, VECTSP_6:def 5;

        

         A30: (( Col (F,i)) . i) = (F * (i,i)) by A19, A16, MATRIX_0:def 8

        .= (( Line (F,i)) . i) by A11, A20, MATRIX_0:def 7;

        (M /. i) = (M . i) by A19, A16, A18, PARTFUN1:def 6

        .= ( Line (( 1. (K,( len b2))),i)) by A1, A11, MATRIX_0: 52;

        

        then (( Col (F,i)) . i) = (((KL . (M /. i)) * ( Line (( 1. (K,( len b2))),i))) . i) by A30, A13, A29, MATRIX13: 102

        .= ((KL . (M /. i)) * ( 1_ K)) by A11, A13, A14, FVSUM_1: 51

        .= (KL . (M /. i));

        

        hence (t1 . i) = (vM /. i) by A3, A4, A6, A5, A10, A28

        .= (vM . i) by A19, A16, A18, A7, PARTFUN1:def 6;

      end;

      hence thesis by A4, A6, A5, FINSEQ_1: 14;

    end;

    theorem :: MATRLIN2:47

    

     Th47: for M be OrdBasis of (( len b2) -VectSp_over K) st M = ( MX2FinS ( 1. (K,( len b2)))) holds for A be Matrix of ( len b1), ( len M), K st A = ( AutMt (f,b1,b2)) & f is additive homogeneous holds (( Mx2Tran (A,b1,M)) . v1) = ((f . v1) |-- b2)

    proof

      let M be OrdBasis of (( len b2) -VectSp_over K) such that

       A1: M = ( MX2FinS ( 1. (K,( len b2))));

      let A be Matrix of ( len b1), ( len M), K such that

       A2: A = ( AutMt (f,b1,b2)) and

       A3: f is additive homogeneous;

      reconsider f9 = f as linear-transformation of V1, V2 by A3;

      set MM = ( Mx2Tran (A,b1,M));

      per cases ;

        suppose

         A4: ( len b1) = 0 ;

        then ( dim V1) = 0 by Th21;

        then ( (Omega). V1) = ( (0). V1) by VECTSP_9: 29;

        then the carrier of V1 = {( 0. V1)} by VECTSP_4:def 3;

        then v1 = ( 0. V1) by TARSKI:def 1;

        then v1 in ( ker f9) by RANKNULL: 11;

        

        hence ((f . v1) |-- b2) = (( 0. V2) |-- b2) by RANKNULL: 10

        .= (( len b2) |-> ( 0. K)) by Th20

        .= ( 0. (( len b2) -VectSp_over K)) by MATRIX13: 102

        .= (MM . v1) by A4, Th33;

      end;

        suppose

         A5: ( len b1) > 0 ;

        

        then ( LineVec2Mx ((MM . v1) |-- M)) = (( LineVec2Mx (v1 |-- b1)) * A) by Th32

        .= ( LineVec2Mx ((f . v1) |-- b2)) by A2, A3, A5, Th31;

        

        hence ((f . v1) |-- b2) = ( Line (( LineVec2Mx ((MM . v1) |-- M)),1)) by MATRIX15: 25

        .= ((MM . v1) |-- M) by MATRIX15: 25

        .= (MM . v1) by A1, Th46;

      end;

    end;

    definition

      let K be add-associative right_zeroed right_complementable Abelian associative well-unital distributive non empty doubleLoopStr, V1,V2 be Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty ModuleStr over K;

      let W be Subspace of V1;

      let f be Function of V1, V2;

      :: original: |

      redefine

      func f | W -> Function of W, V2 ;

      coherence

      proof

        the carrier of W c= the carrier of V1 by VECTSP_4:def 2;

        hence thesis by FUNCT_2: 32;

      end;

    end

    definition

      let K be Field;

      let V1,V2 be VectSp of K;

      let W be Subspace of V1;

      let f be linear-transformation of V1, V2;

      :: original: |

      redefine

      func f | W -> linear-transformation of W, V2 ;

      coherence

      proof

        set F = (f | W);

        

         A1: ( dom F) = the carrier of W by FUNCT_2:def 1;

         A2:

        now

          let a be Scalar of K, v1 be Vector of W;

          reconsider v2 = v1 as Vector of V1 by VECTSP_4: 10;

          (a * v1) = (a * v2) by VECTSP_4: 14;

          

          hence (F . (a * v1)) = (f . (a * v2)) by A1, FUNCT_1: 47

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

          .= (a * (F . v1)) by A1, FUNCT_1: 47;

        end;

        now

          let v1,w1 be Vector of W;

          reconsider v2 = v1, w2 = w1 as Vector of V1 by VECTSP_4: 10;

          (v1 + w1) = (v2 + w2) by VECTSP_4: 13;

          

          hence (F . (v1 + w1)) = (f . (v2 + w2)) by A1, FUNCT_1: 47

          .= ((f . v2) + (f . w2)) by VECTSP_1:def 20

          .= ((F . v1) + (f . w2)) by A1, FUNCT_1: 47

          .= ((F . v1) + (F . w1)) by A1, FUNCT_1: 47;

        end;

        then F is additive homogeneous by A2, MOD_2:def 2;

        hence thesis;

      end;

    end

    

     Lm7: for A be Matrix of ( len b1), ( len b2), K st ( len b1) > 0 & ( len b2) > 0 holds ( nullity ( Mx2Tran (A,b1,b2))) = (( len b1) - ( the_rank_of A))

    proof

      set I = ( id V1);

      reconsider BB = ( MX2FinS ( 1. (K,( len b1)))) as OrdBasis of (( len b1) -VectSp_over K) by Th45;

      let A be Matrix of ( len b1), ( len b2), K such that

       A1: ( len b1) > 0 and

       A2: ( len b2) > 0 ;

      ( len BB) = ( dim (( len b1) -VectSp_over K)) by Th21

      .= ( len b1) by MATRIX13: 112;

      then

      reconsider AI = ( AutMt (I,b1,b1)) as Matrix of ( len b1), ( len BB), K;

      

       A3: ( AutMt (I,b1,b1)) = ( 1. (K,( len b1))) & ( 0. K) <> ( 1_ K) by Th28;

      (( len b1) + 0 ) > 0 by A1;

      then ( len b1) >= 1 by NAT_1: 19;

      then ( Det ( 1. (K,( len b1)))) = ( 1_ K) by MATRIX_7: 16;

      then

       A4: ( the_rank_of AI) = ( len b1) by A3, MATRIX13: 83;

      set S = ( Space_of_Solutions_of (A @ ));

      set KER = ( ker ( Mx2Tran (A,b1,b2)));

      set MAI = ( Mx2Tran (AI,b1,BB));

      set MK = (MAI | KER);

      

       A5: ( dom MK) = the carrier of KER by FUNCT_2:def 1;

      

       A6: the carrier of ( im MK) c= the carrier of S

      proof

        let x be object such that

         A7: x in the carrier of ( im MK);

        the carrier of ( im MK) c= the carrier of (( len b1) -VectSp_over K) by VECTSP_4:def 2;

        then

        reconsider v = x as Element of (( len b1) -VectSp_over K) by A7;

        v in ( im MK) by A7;

        then

        consider w be Element of KER such that

         A8: v = (MK . w) by RANKNULL: 13;

        

         A9: w in KER;

        then w in V1 by VECTSP_4: 9;

        then

        reconsider W = w as Vector of V1;

        (MK . w) = (MAI . w) by A5, FUNCT_1: 47

        .= ((I . W) |-- b1) by Th47

        .= (W |-- b1);

        then (MK . w) in S by A1, A2, A9, Th41;

        hence thesis by A8;

      end;

      ( len A) = ( len b1) & ( width A) = ( len b2) by A1, MATRIX_0: 23;

      then

       A10: ( width (A @ )) = ( len b1) by A2, MATRIX_0: 54;

      

       A11: MAI is one-to-one by A4, Th44;

      ( dim (( len b1) -VectSp_over K)) = ( len b1) by MATRIX13: 112

      .= ( dim V1) by Th21

      .= ( rank MAI) by A11, RANKNULL: 45

      .= ( dim ( im MAI));

      then

       A12: ( (Omega). (( len b1) -VectSp_over K)) = ( (Omega). ( im MAI)) by VECTSP_9: 28;

      the carrier of S c= the carrier of ( im MK)

      proof

        let x be object such that

         A13: x in the carrier of S;

        the carrier of S c= the carrier of (( len b1) -VectSp_over K) by A10, VECTSP_4:def 2;

        then

        reconsider v = x as Element of (( len b1) -VectSp_over K) by A13;

        

         A14: v in S by A13;

        v in ( im MAI) by A12;

        then

        consider w be Element of V1 such that

         A15: v = (MAI . w) by RANKNULL: 13;

        (MAI . w) = ((I . w) |-- b1) by Th47

        .= (w |-- b1);

        then w in KER by A1, A2, A15, A14, Th41;

        then

        reconsider W = w as Element of KER;

        v = (MK . W) by A5, A15, FUNCT_1: 47;

        then v in ( im MK) by RANKNULL: 13;

        hence thesis;

      end;

      then the carrier of S = the carrier of ( im MK) by A6, XBOOLE_0:def 10;

      then

       A16: ( im MK) = S by A10, VECTSP_4: 29;

      MAI is one-to-one by A4, Th44;

      then MK is one-to-one by FUNCT_1: 52;

      

      hence ( nullity ( Mx2Tran (A,b1,b2))) = ( rank MK) by RANKNULL: 45

      .= (( len b1) - ( the_rank_of (A @ ))) by A1, A10, A16, MATRIX15: 68

      .= (( len b1) - ( the_rank_of A)) by MATRIX13: 84;

    end;

    begin

    theorem :: MATRLIN2:48

    

     Th48: for f be linear-transformation of V1, V2 holds ( rank f) = ( the_rank_of ( AutMt (f,b1,b2)))

    proof

      let f be linear-transformation of V1, V2;

      set A = ( AutMt (f,b1,b2));

      per cases ;

        suppose

         A1: ( len b1) = 0 ;

        then ( len A) = 0 by MATRIX_0:def 2;

        then ( dim V1) = (( rank f) + ( nullity f)) & ( the_rank_of A) = 0 by MATRIX13: 74, RANKNULL: 44;

        hence thesis by A1, Th21;

      end;

        suppose

         A2: ( len b1) > 0 & ( len b2) = 0 ;

        then ( width A) = 0 by MATRIX_0: 23;

        then

         A3: ( the_rank_of A) = 0 by MATRIX13: 74;

        ( dim V2) = 0 by A2, Th21;

        hence thesis by A3, VECTSP_9: 25;

      end;

        suppose

         A4: ( len b1) > 0 & ( len b2) > 0 ;

        

         A5: (( rank f) + ( nullity f)) = ( dim V1) by RANKNULL: 44

        .= ( len b1) by Th21;

        ( nullity f) = ( nullity ( Mx2Tran (A,b1,b2))) by Th34

        .= (( len b1) - ( the_rank_of A)) by A4, Lm7;

        hence thesis by A5;

      end;

    end;

    theorem :: MATRLIN2:49

    for M be Matrix of ( len b1), ( len b2), K holds ( rank ( Mx2Tran (M,b1,b2))) = ( the_rank_of M)

    proof

      let M be Matrix of ( len b1), ( len b2), K;

      

      thus ( rank ( Mx2Tran (M,b1,b2))) = ( the_rank_of ( AutMt (( Mx2Tran (M,b1,b2)),b1,b2))) by Th48

      .= ( the_rank_of M) by Th36;

    end;

    theorem :: MATRLIN2:50

    for f be linear-transformation of V1, V2 st ( dim V1) = ( dim V2) holds ( ker f) is non trivial iff ( Det ( AutEqMt (f,b1,b2))) = ( 0. K)

    proof

      let f be linear-transformation of V1, V2 such that

       A1: ( dim V1) = ( dim V2);

      set A = ( AutEqMt (f,b1,b2));

      ( dim V2) = ( len b2) by Th21;

      then

       A2: A = ( AutMt (f,b1,b2)) by A1, Def2, Th21;

      

       A3: ( dim V1) = (( rank f) + ( nullity f)) by RANKNULL: 44;

      

       A4: ( len b1) = ( dim V1) & ( rank f) = ( the_rank_of ( AutMt (f,b1,b2))) by Th21, Th48;

      hereby

        assume ( ker f) is non trivial;

        then ( rank f) <> ( dim V1) by A3, Th42;

        hence ( Det A) = ( 0. K) by A4, A2, MATRIX13: 83;

      end;

      assume ( Det A) = ( 0. K);

      then ( dim ( ker f)) <> 0 by A4, A2, A3, MATRIX13: 83;

      hence thesis by Th42;

    end;

    

     Lm8: for f be linear-transformation of V1, V2, g be Function of V2, V3 holds (g * f) = ((g | ( im f)) * f)

    proof

      let f be linear-transformation of V1, V2, g be Function of V2, V3;

      ( dom f) = ( [#] V1) by FUNCT_2:def 1;

      

      then ( [#] ( im f)) = (f .: ( dom f)) by RANKNULL:def 2

      .= ( rng f) by RELAT_1: 113;

      

      hence ((g | ( im f)) * f) = ((g * ( id ( rng f))) * f) by RELAT_1: 65

      .= (g * (( id ( rng f)) * f)) by RELAT_1: 36

      .= (g * f) by RELAT_1: 54;

    end;

    theorem :: MATRLIN2:51

    for f be linear-transformation of V1, V2, g be linear-transformation of V2, V3 st (g | ( im f)) is one-to-one holds ( rank (g * f)) = ( rank f) & ( nullity (g * f)) = ( nullity f)

    proof

      let f be linear-transformation of V1, V2, g be linear-transformation of V2, V3 such that

       A1: (g | ( im f)) is one-to-one;

      the carrier of ( im (g * f)) = ( [#] ( im (g * f)))

      .= ((g * f) .: ( [#] V1)) by RANKNULL:def 2

      .= (((g | ( im f)) * f) .: ( [#] V1)) by Lm8

      .= ((g | ( im f)) .: (f .: ( [#] V1))) by RELAT_1: 126

      .= ((g | ( im f)) .: ( [#] ( im f))) by RANKNULL:def 2

      .= ( [#] ( im (g | ( im f)))) by RANKNULL:def 2

      .= the carrier of ( im (g | ( im f)));

      

      then

       A2: ( rank (g * f)) = ( rank (g | ( im f))) by VECTSP_4: 29

      .= ( rank f) by A1, RANKNULL: 45;

      (( nullity f) + ( rank f)) = ( dim V1) by RANKNULL: 44

      .= (( nullity (g * f)) + ( rank (g * f))) by RANKNULL: 44;

      hence thesis by A2;

    end;