matrtop2.miz



    begin

    reserve X for set,

n,m,k for Nat,

K for Field,

f for n -element real-valued FinSequence,

M for Matrix of n, m, F_Real ;

    

     Lm1: the carrier of (n -VectSp_over F_Real ) = the carrier of ( TOP-REAL n)

    proof

      

      thus the carrier of (n -VectSp_over F_Real ) = ( REAL n) by MATRIX13: 102

      .= the carrier of ( TOP-REAL n) by EUCLID: 22;

    end;

    

     Lm2: ( 0. (n -VectSp_over F_Real )) = ( 0. ( TOP-REAL n))

    proof

      

      thus ( 0. (n -VectSp_over F_Real )) = (n |-> ( 0. F_Real )) by MATRIX13: 102

      .= ( 0* n)

      .= ( 0. ( TOP-REAL n)) by EUCLID: 70;

    end;

    

     Lm3: f is Point of ( TOP-REAL n)

    proof

      ( len f) = n & ( @ ( @ f)) = f by CARD_1:def 7;

      hence thesis by TOPREAL3: 46;

    end;

    theorem :: MATRTOP2:1

    

     Th1: X is Linear_Combination of (n -VectSp_over F_Real ) iff X is Linear_Combination of ( TOP-REAL n)

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      hereby

        assume X is Linear_Combination of V;

        then

        reconsider L = X as Linear_Combination of V;

        consider S be finite Subset of V such that

         A1: for v be Element of V st not v in S holds (L . v) = ( 0. F_Real ) by VECTSP_6:def 1;

         A2:

        now

          let v be Element of T;

          assume

           A3: not v in S;

          v is Element of V by Lm1;

          hence 0 = (L . v) by A1, A3;

        end;

        (L is Element of ( Funcs (the carrier of T, REAL ))) & S is finite Subset of T by Lm1;

        hence X is Linear_Combination of T by A2, RLVECT_2:def 3;

      end;

      assume X is Linear_Combination of T;

      then

      reconsider L = X as Linear_Combination of T;

      consider S be finite Subset of T such that

       A4: for v be Element of T st not v in S holds (L . v) = 0 by RLVECT_2:def 3;

       A5:

      now

        let v be Element of V;

        assume

         A6: not v in S;

        v is Element of T by Lm1;

        hence ( 0. F_Real ) = (L . v) by A4, A6;

      end;

      L is Element of ( Funcs (the carrier of V,the carrier of F_Real )) & S is finite Subset of V by Lm1;

      hence thesis by A5, VECTSP_6:def 1;

    end;

    theorem :: MATRTOP2:2

    

     Th2: for Lv be Linear_Combination of (n -VectSp_over F_Real ), Lr be Linear_Combination of ( TOP-REAL n) st Lr = Lv holds ( Carrier Lr) = ( Carrier Lv)

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      let Lv be Linear_Combination of V, Lr be Linear_Combination of T such that

       A1: Lr = Lv;

      thus ( Carrier Lr) c= ( Carrier Lv)

      proof

        let x be object;

        assume

         A2: x in ( Carrier Lr);

        then

        reconsider v = x as Element of T;

        reconsider u = v as Element of V by Lm1;

        (Lv . u) <> ( 0. F_Real ) by A1, A2, RLVECT_2: 19;

        hence thesis by VECTSP_6: 1;

      end;

      let x be object;

      assume x in ( Carrier Lv);

      then

      consider u be Element of V such that

       A3: x = u and

       A4: (Lv . u) <> ( 0. F_Real ) by VECTSP_6: 1;

      reconsider v = u as Element of T by Lm1;

      v in ( Carrier Lr) by A1, A4, RLVECT_2: 19;

      hence thesis by A3;

    end;

    theorem :: MATRTOP2:3

    

     Th3: for F be FinSequence of ( TOP-REAL n), fr be Function of ( TOP-REAL n), REAL , Fv be FinSequence of (n -VectSp_over F_Real ), fv be Function of (n -VectSp_over F_Real ), F_Real st fr = fv & F = Fv holds (fr (#) F) = (fv (#) Fv)

    proof

      let F be FinSequence of ( TOP-REAL n), fr be Function of ( TOP-REAL n), REAL , Fv be FinSequence of (n -VectSp_over F_Real ), fv be Function of (n -VectSp_over F_Real ), F_Real ;

      assume that

       A1: fr = fv and

       A2: F = Fv;

      

       A3: ( len (fv (#) Fv)) = ( len Fv) by VECTSP_6:def 5;

      

       A4: ( len (fr (#) F)) = ( len F) by RLVECT_2:def 7;

      now

        reconsider T = ( TOP-REAL n) as RealLinearSpace;

        let i be Nat;

        reconsider Fi = (F /. i) as FinSequence of REAL by EUCLID: 24;

        reconsider Fvi = (Fv /. i) as Element of (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

        reconsider Fii = (F /. i) as Element of T;

        assume

         A5: 1 <= i & i <= ( len F);

        then

         A6: i in ( dom (fv (#) Fv)) by A2, A3, FINSEQ_3: 25;

        i in ( dom F) by A5, FINSEQ_3: 25;

        then

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

        i in ( dom Fv) by A2, A5, FINSEQ_3: 25;

        then

         A8: (Fv /. i) = (Fv . i) by PARTFUN1:def 6;

        i in ( dom (fr (#) F)) by A4, A5, FINSEQ_3: 25;

        

        hence ((fr (#) F) . i) = ((fr . Fii) * Fii) by RLVECT_2:def 7

        .= ((fr . Fi) * Fi) by EUCLID: 65

        .= ((fv . (Fv /. i)) * Fvi) by A1, A2, A7, A8, MATRIXR1: 17

        .= ((fv . (Fv /. i)) * (Fv /. i)) by MATRIX13: 102

        .= ((fv (#) Fv) . i) by A6, VECTSP_6:def 5;

      end;

      hence thesis by A2, A4, A3;

    end;

    theorem :: MATRTOP2:4

    

     Th4: for F be FinSequence of ( TOP-REAL n), Fv be FinSequence of (n -VectSp_over F_Real ) st Fv = F holds ( Sum F) = ( Sum Fv)

    proof

      set T = ( TOP-REAL n);

      set V = (n -VectSp_over F_Real );

      let F be FinSequence of T;

      let Fv be FinSequence of V such that

       A1: Fv = F;

      reconsider T = ( TOP-REAL n) as RealLinearSpace;

      consider f be sequence of the carrier of T such that

       A2: ( Sum F) = (f . ( len F)) and

       A3: (f . 0 ) = ( 0. T) and

       A4: for j be Nat, v be Element of T st j < ( len F) & v = (F . (j + 1)) holds (f . (j + 1)) = ((f . j) + v) by RLVECT_1:def 12;

      consider fv be sequence of the carrier of V such that

       A5: ( Sum Fv) = (fv . ( len Fv)) and

       A6: (fv . 0 ) = ( 0. V) and

       A7: for j be Nat, v be Element of V st j < ( len Fv) & v = (Fv . (j + 1)) holds (fv . (j + 1)) = ((fv . j) + v) by RLVECT_1:def 12;

      defpred P[ Nat] means $1 <= ( len F) implies (f . $1) = (fv . $1);

      

       A8: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A9: P[i];

        set i1 = (i + 1);

        reconsider Fvi1 = (Fv /. i1), fvi = (fv . i) as Element of (n -tuples_on the carrier of F_Real ) by MATRIX13: 102;

        

         A10: ( @ ( @ Fvi1)) = Fvi1 & ( @ ( @ fvi)) = fvi;

        reconsider Fi1 = (F /. i1) as Element of T;

        assume

         A11: i1 <= ( len F);

        then

         A12: i < ( len F) by NAT_1: 13;

        1 <= i1 by NAT_1: 11;

        then

         A13: i1 in ( dom F) by A11, FINSEQ_3: 25;

        then (F . i1) = (F /. i1) by PARTFUN1:def 6;

        then

         A14: (f . i1) = ((f . i) + Fi1) by A4, A12;

        

         A15: (Fv /. i1) = (Fv . i1) by A1, A13, PARTFUN1:def 6;

        then Fvi1 = (F /. i1) by A1, A13, PARTFUN1:def 6;

        

        hence (f . i1) = (( @ fvi) + ( @ Fvi1)) by A9, A11, A14, EUCLID: 64, NAT_1: 13

        .= (fvi + Fvi1) by A10, MATRTOP1: 1

        .= ((fv . i) + (Fv /. i1)) by MATRIX13: 102

        .= (fv . i1) by A1, A7, A12, A15;

      end;

      

       A16: P[ 0 ] by A3, A6, Lm2;

      for n be Nat holds P[n] from NAT_1:sch 2( A16, A8);

      hence thesis by A1, A2, A5;

    end;

    theorem :: MATRTOP2:5

    

     Th5: for Lv be Linear_Combination of (n -VectSp_over F_Real ), Lr be Linear_Combination of ( TOP-REAL n) st Lr = Lv holds ( Sum Lr) = ( Sum Lv)

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      let Lv be Linear_Combination of V;

      let Lr be Linear_Combination of T such that

       A1: Lr = Lv;

      consider F be FinSequence of the carrier of T such that

       A2: (F is one-to-one) & ( rng F) = ( Carrier Lr) and

       A3: ( Sum Lr) = ( Sum (Lr (#) F)) by RLVECT_2:def 8;

      reconsider F1 = F as FinSequence of the carrier of V by Lm1;

      

       A4: (Lr (#) F) = (Lv (#) F1) by A1, Th3;

      ( Carrier Lr) = ( Carrier Lv) by A1, Th2;

      

      hence ( Sum Lv) = ( Sum (Lv (#) F1)) by A2, VECTSP_6:def 6

      .= ( Sum Lr) by A3, A4, Th4;

    end;

    theorem :: MATRTOP2:6

    

     Th6: for Af be Subset of (n -VectSp_over F_Real ), Ar be Subset of ( TOP-REAL n) st Af = Ar holds ( [#] ( Lin Ar)) = ( [#] ( Lin Af))

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      let Af be Subset of V;

      let Ar be Subset of T such that

       A1: Af = Ar;

      hereby

        let x be object;

        assume x in ( [#] ( Lin Ar));

        then x in ( Lin Ar);

        then

        consider L be Linear_Combination of Ar such that

         A2: x = ( Sum L) by RLVECT_3: 14;

        reconsider L1 = L as Linear_Combination of V by Th1;

        ( Carrier L1) = ( Carrier L) & ( Carrier L) c= Ar by Th2, RLVECT_2:def 6;

        then

         A3: L1 is Linear_Combination of Af by A1, VECTSP_6:def 4;

        ( Sum L1) = ( Sum L) by Th5;

        then x in ( Lin Af) by A2, A3, VECTSP_7: 7;

        hence x in ( [#] ( Lin Af));

      end;

      let x be object;

      assume x in ( [#] ( Lin Af));

      then x in ( Lin Af);

      then

      consider L be Linear_Combination of Af such that

       A4: x = ( Sum L) by VECTSP_7: 7;

      reconsider L1 = L as Linear_Combination of T by Th1;

      ( Carrier L1) = ( Carrier L) & ( Carrier L) c= Af by Th2, VECTSP_6:def 4;

      then

       A5: L1 is Linear_Combination of Ar by A1, RLVECT_2:def 6;

      ( Sum L1) = ( Sum L) by Th5;

      then x in ( Lin Ar) by A4, A5, RLVECT_3: 14;

      hence thesis;

    end;

    theorem :: MATRTOP2:7

    

     Th7: for Af be Subset of (n -VectSp_over F_Real ), Ar be Subset of ( TOP-REAL n) st Af = Ar holds Af is linearly-independent iff Ar is linearly-independent

    proof

      set V = (n -VectSp_over F_Real );

      let AV be Subset of V;

      set T = ( TOP-REAL n);

      let AR be Subset of T such that

       A1: AV = AR;

      hereby

        assume

         A2: AV is linearly-independent;

        now

          let L be Linear_Combination of AR;

          reconsider L1 = L as Linear_Combination of V by Th1;

          

           A3: ( Carrier L1) = ( Carrier L) by Th2;

          assume ( Sum L) = ( 0. T);

          

          then

           A4: ( 0. V) = ( Sum L) by Lm2

          .= ( Sum L1) by Th5;

          ( Carrier L) c= AR by RLVECT_2:def 6;

          then L1 is Linear_Combination of AV by A1, A3, VECTSP_6:def 4;

          hence ( Carrier L) = {} by A2, A3, A4, VECTSP_7:def 1;

        end;

        hence AR is linearly-independent by RLVECT_3:def 1;

      end;

      assume

       A5: AR is linearly-independent;

      now

        let L be Linear_Combination of AV;

        reconsider L1 = L as Linear_Combination of T by Th1;

        

         A6: ( Carrier L1) = ( Carrier L) by Th2;

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

        then

        reconsider L1 as Linear_Combination of AR by A1, A6, RLVECT_2:def 6;

        assume ( Sum L) = ( 0. V);

        

        then ( 0. T) = ( Sum L) by Lm2

        .= ( Sum L1) by Th5;

        hence ( Carrier L) = {} by A5, A6, RLVECT_3:def 1;

      end;

      hence thesis by VECTSP_7:def 1;

    end;

    theorem :: MATRTOP2:8

    

     Th8: for V be VectSp of K, W be Subspace of V, L be Linear_Combination of V holds (L | the carrier of W) is Linear_Combination of W

    proof

      let V be VectSp of K;

      let W be Subspace of V;

      let L be Linear_Combination of V;

      set cW = the carrier of W;

      cW c= ( [#] V) by VECTSP_4:def 2;

      then (L | cW) is Function of cW, the carrier of K by FUNCT_2: 32;

      then

      reconsider L1 = (L | cW) as Element of ( Funcs (cW,the carrier of K)) by FUNCT_2: 8;

      

       A1: for v be Element of W st not v in (( Carrier L) /\ cW) holds (L1 . v) = ( 0. K)

      proof

        let v be Element of W;

        reconsider w = v as Element of V by VECTSP_4: 10;

        assume not v in (( Carrier L) /\ cW);

        then

         A2: not v in ( Carrier L) by XBOOLE_0:def 4;

        (L . w) = (L1 . v) by FUNCT_1: 49;

        hence thesis by A2, VECTSP_6: 2;

      end;

      (( Carrier L) /\ cW) c= cW by XBOOLE_1: 17;

      hence thesis by A1, VECTSP_6:def 1;

    end;

    theorem :: MATRTOP2:9

    for V be VectSp of K, A be linearly-independent Subset of V holds for L1,L2 be Linear_Combination of V st ( Carrier L1) c= A & ( Carrier L2) c= A & ( Sum L1) = ( Sum L2) holds L1 = L2

    proof

      let V be VectSp of K;

      let A be linearly-independent Subset of V;

      let L1,L2 be Linear_Combination of V such that

       A1: ( Carrier L1) c= A & ( Carrier L2) c= A and

       A2: ( Sum L1) = ( Sum L2);

      (L1 is Linear_Combination of A) & L2 is Linear_Combination of A by A1, VECTSP_6:def 4;

      then

       A3: (L1 - L2) is Linear_Combination of A by VECTSP_6: 42;

      ( Sum (L1 - L2)) = (( Sum L1) - ( Sum L2)) by VECTSP_6: 47

      .= ( 0. V) by A2, RLVECT_1: 15;

      then ( Carrier (L1 - L2)) = {} by A3, VECTSP_7:def 1;

      

      then ( ZeroLC V) = (L1 - L2) by VECTSP_6:def 3

      .= (L1 + ( - L2)) by VECTSP_6:def 11

      .= (( - L2) + L1) by VECTSP_6: 25;

      then L1 = ( - ( - L2)) by VECTSP_6: 37;

      hence thesis;

    end;

    theorem :: MATRTOP2:10

    for V be RealLinearSpace, W be Subspace of V holds for L be Linear_Combination of V holds (L | the carrier of W) is Linear_Combination of W

    proof

      let V be RealLinearSpace;

      let W be Subspace of V;

      let L be Linear_Combination of V;

      set cW = the carrier of W;

      cW c= ( [#] V) by RLSUB_1:def 2;

      then (L | cW) is Function of cW, REAL by FUNCT_2: 32;

      then

      reconsider L1 = (L | cW) as Element of ( Funcs (cW, REAL )) by FUNCT_2: 8;

      

       A1: for v be Element of W st not v in (( Carrier L) /\ cW) holds (L1 . v) = 0

      proof

        let v be Element of W;

        reconsider w = v as Element of V by RLSUB_1: 10;

        assume not v in (( Carrier L) /\ cW);

        then

         A2: not v in ( Carrier L) by XBOOLE_0:def 4;

        (L . w) = (L1 . v) by FUNCT_1: 49;

        hence thesis by A2, RLVECT_2: 19;

      end;

      (( Carrier L) /\ cW) c= cW by XBOOLE_1: 17;

      hence thesis by A1, RLVECT_2:def 3;

    end;

    theorem :: MATRTOP2:11

    for U be Subspace of (n -VectSp_over F_Real ), W be Subspace of ( TOP-REAL n) st ( [#] U) = ( [#] W) holds X is Linear_Combination of U iff X is Linear_Combination of W

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      let U be Subspace of V, W be Subspace of T such that

       A1: ( [#] U) = ( [#] W);

      hereby

        assume X is Linear_Combination of U;

        then

        reconsider L = X as Linear_Combination of U;

        ex S be finite Subset of U st for v be Element of U st not v in S holds (L . v) = ( 0. F_Real ) by VECTSP_6:def 1;

        hence X is Linear_Combination of W by A1, RLVECT_2:def 3;

      end;

      assume X is Linear_Combination of W;

      then

      reconsider L = X as Linear_Combination of W;

      consider S be finite Subset of W such that

       A2: for v be Element of W st not v in S holds (L . v) = 0 by RLVECT_2:def 3;

      for v be Element of U st not v in S holds ( 0. F_Real ) = (L . v) by A1, A2;

      hence thesis by A1, VECTSP_6:def 1;

    end;

    theorem :: MATRTOP2:12

    for U be Subspace of (n -VectSp_over F_Real ), W be Subspace of ( TOP-REAL n) holds for LU be Linear_Combination of U, LW be Linear_Combination of W st LU = LW holds ( Carrier LU) = ( Carrier LW) & ( Sum LU) = ( Sum LW)

    proof

      set V = (n -VectSp_over F_Real );

      set T = ( TOP-REAL n);

      let U be Subspace of V, W be Subspace of ( TOP-REAL n);

      let LU be Linear_Combination of U, LW be Linear_Combination of W such that

       A1: LU = LW;

      reconsider LW9 = LW as Function of the carrier of W, REAL ;

      defpred P[ object, object] means ($1 in W & $2 = (LW . $1)) or ( not $1 in W & $2 = ( In ( 0 , REAL )));

      

       A2: ( dom LU) = ( [#] U) & ( dom LW) = ( [#] W) by FUNCT_2:def 1;

      

       A3: for x be object st x in the carrier of T holds ex y be object st y in REAL & P[x, y]

      proof

        let x be object;

        assume x in the carrier of T;

        then

        reconsider x as VECTOR of T;

        per cases ;

          suppose

           A4: x in W;

          then

          reconsider x as VECTOR of W;

           P[x, (LW . x)] by A4;

          hence thesis;

        end;

          suppose not x in W;

          hence thesis;

        end;

      end;

      consider L be Function of the carrier of T, REAL such that

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

      

       A6: the carrier of W c= the carrier of T by RLSUB_1:def 2;

      then

      reconsider C = ( Carrier LW) as finite Subset of T by XBOOLE_1: 1;

      

       A7: L is Element of ( Funcs (the carrier of T, REAL )) by FUNCT_2: 8;

      now

        let v be VECTOR of T;

        assume not v in C;

        then P[v, (LW . v)] & not v in C & v in the carrier of W or P[v, 0 ] by STRUCT_0:def 5;

        then P[v, (LW . v)] & (LW . v) = 0 or P[v, 0 ] by RLVECT_2: 19;

        hence (L . v) = 0 by A5;

      end;

      then

      reconsider L as Linear_Combination of T by A7, RLVECT_2:def 3;

      reconsider L9 = (L | the carrier of W) as Function of the carrier of W, REAL by A6, FUNCT_2: 32;

      now

        let x be object;

        assume

         A8: x in the carrier of W;

        then P[x, (L . x)] by A6, A5;

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

      end;

      then

       A9: LW = L9 by FUNCT_2: 12;

      reconsider K = L as Linear_Combination of V by Th1;

      now

        let x be object;

        assume that

         A10: x in ( Carrier L) and

         A11: not x in the carrier of W;

        consider v be VECTOR of T such that

         A12: x = v and

         A13: (L . v) <> 0 by A10, RLVECT_5: 3;

         P[v, 0 ] by A11, A12, STRUCT_0:def 5;

        hence contradiction by A5, A13;

      end;

      then

       A14: ( Carrier L) c= the carrier of W;

      then

       A15: ( Carrier L) = ( Carrier LW) & ( Sum L) = ( Sum LW) by A9, RLVECT_5: 10;

      

       A16: ( Carrier L) = ( Carrier K) by Th2;

      then ( Sum K) = ( Sum LU) by A1, A2, A14, A9, VECTSP_9: 7;

      hence thesis by A1, A2, A9, A15, A16, Th5, VECTSP_9: 7;

    end;

    registration

      let m, K;

      let A be Subset of (m -VectSp_over K);

      cluster ( Lin A) -> finite-dimensional;

      coherence ;

    end

    

     Lm4: ( lines M) c= ( [#] ( Lin ( lines M)))

    proof

      let x be object;

      assume x in ( lines M);

      then x in ( Lin ( lines M)) by VECTSP_7: 8;

      hence thesis;

    end;

    begin

    theorem :: MATRTOP2:13

    ( the_rank_of M) = n implies M is OrdBasis of ( Lin ( lines M))

    proof

      

       A1: ( lines M) c= ( [#] ( Lin ( lines M))) by Lm4;

      then

      reconsider L = ( lines M) as Subset of ( Lin ( lines M));

      reconsider B = M as FinSequence of ( Lin ( lines M)) by A1, FINSEQ_1:def 4;

      assume that

       A2: ( the_rank_of M) = n;

      

       A3: M is one-to-one by A2, MATRIX13: 121;

      ( lines M) is linearly-independent by A2, MATRIX13: 121;

      then

       A4: L is linearly-independent by VECTSP_9: 12;

      ( Lin L) = ( Lin ( lines M)) by VECTSP_9: 17;

      then L is Basis of ( Lin ( lines M)) by A4, VECTSP_7:def 3;

      then B is OrdBasis of ( Lin ( lines M)) by A3, MATRLIN:def 2;

      hence thesis;

    end;

    theorem :: MATRTOP2:14

    

     Th14: for V,W be VectSp of K holds for T be linear-transformation of V, W holds for A be Subset of V holds for L be Linear_Combination of A st (T | A) is one-to-one holds (T . ( Sum L)) = ( Sum (T @ L))

    proof

      let V,W be VectSp of K;

      let T be linear-transformation of V, W;

      let A be Subset of V;

      let L be Linear_Combination of A;

      consider G be FinSequence of V such that

       A1: G is one-to-one and

       A2: ( rng G) = ( Carrier L) and

       A3: ( Sum L) = ( Sum (L (#) G)) by VECTSP_6:def 6;

      set H = (T * G);

      reconsider H as FinSequence of W;

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

      then

       A4: ((T | A) | ( Carrier L)) = (T | ( Carrier L)) by RELAT_1: 74;

      assume

       A5: (T | A) is one-to-one;

      then

       A6: (T | ( Carrier L)) is one-to-one by A4, FUNCT_1: 52;

      

       A7: ( rng H) = (T .: ( Carrier L)) by A2, RELAT_1: 127

      .= ( Carrier (T @ L)) by A6, RANKNULL: 39;

      ( dom T) = ( [#] V) by FUNCT_2:def 1;

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

      then

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

      (T * (L (#) G)) = ((T @ L) (#) H) by A6, A2, RANKNULL: 38;

      hence thesis by A3, A8, MATRLIN: 16;

    end;

    

     Lm5: ( card ( lines M)) = 1 implies ex L be Linear_Combination of ( lines M) st ( Sum L) = (( Mx2Tran M) . f) & for k st k in ( Seg n) holds (L . ( Line (M,k))) = ( Sum f) & (M " {( Line (M,k))}) = ( dom f)

    proof

      assume that

       A1: ( card ( lines M)) = 1;

      per cases ;

        suppose

         A2: n <> 0 ;

        deffunc F( set) = ( 0. F_Real );

        

         A3: ( len M) = n by A2, MATRIX13: 1;

        reconsider Sf = ( Sum f) as Element of F_Real by XREAL_0:def 1;

        set Mf = (( Mx2Tran M) . f);

        

         A4: ( len Mf) = m by CARD_1:def 7;

        

         A5: ( len f) = n by CARD_1:def 7;

        set V = (m -VectSp_over F_Real );

        consider x be object such that

         A6: ( lines M) = {x} by A1, CARD_2: 42;

        x in ( lines M) by A6, TARSKI:def 1;

        then

        consider j be object such that

         A7: j in ( dom M) and

         A8: (M . j) = x by FUNCT_1:def 3;

        reconsider j as Nat by A7;

        

         A9: ( width M) = m by A2, MATRIX13: 1;

        then

        reconsider LMj = ( Line (M,j)) as Element of V by MATRIX13: 102;

        consider L be Function of the carrier of V, the carrier of F_Real such that

         A10: (L . LMj) = ( 1. F_Real ) and

         A11: for z be Element of V st z <> LMj holds (L . z) = F(z) from FUNCT_2:sch 6;

        reconsider L as Element of ( Funcs (the carrier of V,the carrier of F_Real )) by FUNCT_2: 8;

        

         A12: x = ( Line (M,j)) by A7, A8, MATRIX_0: 60;

         A13:

        now

          let z be Vector of V such that

           A14: not z in ( lines M);

          z <> LMj by A6, A12, A14, TARSKI:def 1;

          hence (L . z) = ( 0. F_Real ) by A11;

        end;

        

         A15: ( len (Sf * ( Line (M,j)))) = m by A9, CARD_1:def 7;

         A16:

        now

          ( len ( @ f)) = n by CARD_1:def 7;

          then

          reconsider F = ( @ f) as Element of (n -tuples_on the carrier of F_Real ) by FINSEQ_2: 92;

          let w be Nat;

          set Mjw = (M * (j,w));

          assume

           A17: 1 <= w & w <= m;

          then

           A18: w in ( dom (Sf * ( Line (M,j)))) by A15, FINSEQ_3: 25;

          

           A19: w in ( Seg m) by A17;

          then

           A20: (( Line (M,j)) . w) = Mjw by A9, MATRIX_0:def 7;

           A21:

          now

            let z be Nat;

            assume

             A22: 1 <= z & z <= n;

            then

             A23: z in ( Seg n);

            then

             A24: ( Line (M,z)) in ( lines M) by MATRIX13: 103;

            z in ( dom M) by A3, A22, FINSEQ_3: 25;

            

            hence (( Col (M,w)) . z) = (M * (z,w)) by MATRIX_0:def 8

            .= (( Line (M,z)) . w) by A9, A19, MATRIX_0:def 7

            .= Mjw by A6, A12, A20, A24, TARSKI:def 1

            .= ((n |-> Mjw) . z) by A23, FINSEQ_2: 57;

          end;

          ( len ( Col (M,w))) = n & ( len (n |-> Mjw)) = n by A3, CARD_1:def 7;

          then

           A25: ( Col (M,w)) = (n |-> Mjw) by A21;

          

          thus (Mf . w) = (( @ f) "*" ( Col (M,w))) by A2, A17, MATRTOP1: 18

          .= ( Sum ( mlt (( @ f),( Col (M,w))))) by FVSUM_1:def 9

          .= ( Sum (Mjw * F)) by A25, FVSUM_1: 66

          .= (Mjw * ( Sum ( @ f))) by FVSUM_1: 73

          .= (Mjw * Sf) by MATRPROB: 36

          .= ((Sf * ( Line (M,j))) . w) by A18, A20, FVSUM_1: 50;

        end;

        reconsider L as Linear_Combination of V by A13, VECTSP_6:def 1;

        ( Carrier L) c= {LMj}

        proof

          let x be object such that

           A26: x in ( Carrier L);

          (L . x) <> ( 0. F_Real ) by A26, VECTSP_6: 2;

          then x = LMj by A11, A26;

          hence thesis by TARSKI:def 1;

        end;

        then

        reconsider L as Linear_Combination of ( lines M) by A6, A12, VECTSP_6:def 4;

        

         A27: ( Sum L) = (( 1. F_Real ) * LMj) by A6, A12, A10, VECTSP_6: 17

        .= LMj by VECTSP_1:def 17;

        reconsider SfL = (Sf * L) as Linear_Combination of ( lines M) by VECTSP_6: 31;

        take SfL;

        ( Sum SfL) = (Sf * ( Sum L)) by VECTSP_6: 45

        .= (Sf * ( Line (M,j))) by A9, A27, MATRIX13: 102;

        hence ( Sum SfL) = Mf by A15, A4, A16, FINSEQ_1: 14;

        let w be Nat such that

         A28: w in ( Seg n);

        ( Line (M,w)) in ( lines M) by A28, MATRIX13: 103;

        then

         A29: ( Line (M,w)) = LMj by A6, A12, TARSKI:def 1;

        

        thus ( Sum f) = (Sf * 1)

        .= (Sf * ( 1. F_Real ))

        .= (SfL . ( Line (M,w))) by A10, A29, VECTSP_6:def 9;

        

        thus (M " {( Line (M,w))}) = ( dom M) by A6, A12, A29, RELAT_1: 134

        .= ( dom f) by A3, A5, FINSEQ_3: 29;

      end;

        suppose

         A30: n = 0 ;

        reconsider L = ( ZeroLC (m -VectSp_over F_Real )) as Linear_Combination of ( lines M) by VECTSP_6: 5;

        take L;

        

        thus ( Sum L) = ( 0. (m -VectSp_over F_Real )) by VECTSP_6: 15

        .= ( 0. ( TOP-REAL m)) by Lm2

        .= (( Mx2Tran M) . f) by A30, MATRTOP1:def 3;

        thus thesis by A30;

      end;

    end;

    theorem :: MATRTOP2:15

    

     Th15: for S be Subset of ( Seg n) st (M | S) is one-to-one & ( rng (M | S)) = ( lines M) holds ex L be Linear_Combination of ( lines M) st ( Sum L) = (( Mx2Tran M) . f) & for k st k in S holds (L . ( Line (M,k))) = ( Sum ( Seq (f | (M " {( Line (M,k))}))))

    proof

      defpred P[ Nat] means for n, m, M, f holds for S be Subset of ( Seg n) st (n = 0 implies m = 0 ) & (M | S) is one-to-one & ( rng (M | S)) = ( lines M) & ( card ( lines M)) = $1 holds ex L be Linear_Combination of ( lines M) st ( Sum L) = (( Mx2Tran M) . f) & for i be Nat st i in S holds (L . ( Line (M,i))) = ( Sum ( Seq (f | (M " {( Line (M,i))}))));

      

       A1: for i be Nat st P[i] holds P[(i + 1)]

      proof

        let i be Nat such that

         A2: P[i];

        let n, m, M, f;

        let S be Subset of ( Seg n) such that

         A3: n = 0 implies m = 0 and

         A4: (M | S) is one-to-one and

         A5: ( rng (M | S)) = ( lines M) and

         A6: ( card ( lines M)) = (i + 1);

        

         A7: ( len M) = n by A3, MATRIX13: 1;

        

         A8: ( width M) = m by A3, MATRIX13: 1;

        per cases ;

          suppose i = 0 ;

          then

          consider L be Linear_Combination of ( lines M) such that

           A9: ( Sum L) = (( Mx2Tran M) . f) and

           A10: for i be Nat st i in ( Seg n) holds (L . ( Line (M,i))) = ( Sum f) & (M " {( Line (M,i))}) = ( dom f) by A6, Lm5;

          take L;

          thus ( Sum L) = (( Mx2Tran M) . f) by A9;

          let w be Nat such that

           A11: w in S;

          (M " {( Line (M,w))}) = ( dom f) by A10, A11;

          then

           A12: (f | (M " {( Line (M,w))})) = f;

          (L . ( Line (M,w))) = ( Sum f) by A10, A11;

          hence ( Sum ( Seq (f | (M " {( Line (M,w))})))) = (L . ( Line (M,w))) by A12, FINSEQ_3: 116;

        end;

          suppose

           A13: i > 0 ;

          ( lines M) <> {} by A6;

          then

          consider x be object such that

           A14: x in ( lines M) by XBOOLE_0:def 1;

          reconsider LM = {x} as Subset of ( lines M) by A14, ZFMISC_1: 31;

          set n1 = (n -' ( card (M " LM)));

          reconsider ML1 = (M - LM) as Matrix of n1, m, F_Real by MATRTOP1: 14;

          

           A15: (LM ` ) = (( lines M) \ LM) by SUBSET_1:def 4;

          then

           A16: LM misses (LM ` ) by XBOOLE_1: 79;

          (LM \/ (LM ` )) = ( [#] ( lines M)) by SUBSET_1: 10

          .= ( lines M) by SUBSET_1:def 3;

          

          then

           A17: ((M " LM) \/ (M " (LM ` ))) = (M " ( rng M)) by RELAT_1: 140

          .= ( dom M) by RELAT_1: 134;

          

           A18: ( len ML1) = (( len M) - ( card (M " LM))) by FINSEQ_3: 59;

          then

           A19: (n - ( card (M " LM))) = n1 by A7, XREAL_1: 49, XREAL_1: 233;

          LM misses (LM ` ) by A15, XBOOLE_1: 79;

          

          then

           A20: (( card (M " LM)) + ( card (M " (LM ` )))) = ( card ( dom M)) by A17, CARD_2: 40, FUNCT_1: 71

          .= n by A7, CARD_1: 62;

          

           A21: n1 <> 0

          proof

            assume n1 = 0 ;

            then (M " (LM ` )) = {} by A7, A18, A20, XREAL_1: 49, XREAL_1: 233;

            then (LM ` ) misses ( rng M) by RELAT_1: 138;

            then {} = (( lines M) \ LM) by A15, XBOOLE_1: 67;

            then ( lines M) c= LM by XBOOLE_1: 37;

            then ( lines M) = LM;

            then (i + 1) = 1 by A6, CARD_2: 42;

            hence contradiction by A13;

          end;

          set n2 = (n -' ( card (M " (LM ` ))));

          reconsider ML2 = (M - (LM ` )) as Matrix of n2, m, F_Real by MATRTOP1: 14;

          ( rng ML2) = (( rng M) \ (LM ` )) by FINSEQ_3: 65;

          then

           A22: ( rng ML2) = ((LM ` ) ` ) by SUBSET_1:def 4;

          reconsider FR = F_Real as Field;

          set Mf = (( Mx2Tran M) . f);

          set V = (m -VectSp_over F_Real );

          ( len f) = n by CARD_1:def 7;

          then

           A23: ( dom f) = ( Seg n) by FINSEQ_1:def 3;

          consider j be object such that

           A24: j in ( dom (M | S)) and

           A25: ((M | S) . j) = x by A5, A14, FUNCT_1:def 3;

          

           A26: x = (M . j) by A24, A25, FUNCT_1: 47;

          

           A27: j in ( dom M) by A24, RELAT_1: 57;

          

           A28: j in S by A24;

          reconsider j as Nat by A24;

          

           A29: x = ( Line (M,j)) by A27, A26, MATRIX_0: 60;

          

           A30: ( len ML2) = (( len M) - ( card (M " (LM ` )))) by FINSEQ_3: 59;

          then

           A31: (n - ( card (M " (LM ` )))) = n2 by A7, XREAL_1: 49, XREAL_1: 233;

          

           A32: ( rng ML1) = (( rng M) \ LM) by FINSEQ_3: 65;

          then

           A33: ( rng ML1) = (LM ` ) by SUBSET_1:def 4;

          reconsider LMj = ( Line (M,j)) as Element of V by A8, MATRIX13: 102;

          

           A34: ( card ( rng ML1)) = (( card ( rng M)) - ( card LM)) by A32, CARD_2: 44

          .= ((i + 1) - 1) by A6, CARD_2: 42;

          ((LM ` ) ` ) = LM;

          then

          consider P be Permutation of ( dom M) such that

           A35: ((M - LM) ^ (M - (LM ` ))) = (M * P) by FINSEQ_3: 115;

          ( dom M) = ( Seg n) by A7, FINSEQ_1:def 3;

          then

          reconsider p = P as Permutation of ( Seg n);

          

           A36: ((M | S) * P) = ((M | S) * (p | ( dom p)))

          .= ((M * p) | (( dom p) /\ (p " S))) by FUNCT_1: 100

          .= ((M * p) | (p " S)) by RELAT_1: 132, XBOOLE_1: 28;

          reconsider pp = P as one-to-one Function;

          ( len (M * p)) = n by MATRIX_0:def 2;

          then

           A37: ( dom (M * p)) = ( Seg n) by FINSEQ_1:def 3;

          set ppj = ((pp " ) . j);

          

           A38: ( rng p) = ( Seg n) by FUNCT_2:def 3;

          then

           A39: (p " S) = ((pp " ) .: S) & ( dom (pp " )) = ( Seg n) by FUNCT_1: 33, FUNCT_1: 85;

          then

           A40: ppj in (p " S) by A28, FUNCT_1:def 6;

          

           A41: (p . ppj) = j by A28, A38, FUNCT_1: 35;

          

           A42: not ppj in ( dom ML1)

          proof

            assume

             A43: ppj in ( dom ML1);

            ((M * P) . ppj) = (M . j) by A40, A41, A37, FUNCT_1: 12;

            then ((M * P) . ppj) = LMj by A27, MATRIX_0: 60;

            then (ML1 . ppj) = LMj by A35, A43, FINSEQ_1:def 7;

            then

             A44: (ML1 . ppj) in LM by A29, TARSKI:def 1;

            (ML1 . ppj) in (LM ` ) by A33, A43, FUNCT_1:def 3;

            hence contradiction by A16, A44, XBOOLE_0: 3;

          end;

          set pSj = ((p " S) \ {ppj});

          ( dom M) = ( Seg n) by A7, FINSEQ_1:def 3;

          then

           A45: ( dom (M | S)) = S by RELAT_1: 62;

          

           A46: pSj c= ( dom ML1)

          proof

            let y be object;

            assume

             A47: y in pSj;

            then

            reconsider Y = y as Nat;

            

             A48: ((M * p) . y) = (M . (p . y)) by A37, A47, FUNCT_1: 12;

             not y in {ppj} by A47, XBOOLE_0:def 5;

            then

             A49: y <> ppj by TARSKI:def 1;

            

             A50: ppj in ( dom P) by A40, FUNCT_1:def 7;

            

             A51: y in (p " S) by A47, XBOOLE_0:def 5;

            then

             A52: (p . y) in ( dom (M | S)) by A45, FUNCT_1:def 7;

            y in ( dom P) by A51, FUNCT_1:def 7;

            then (p . y) <> j by A41, A49, A50, FUNCT_1:def 4;

            then ((M | S) . (p . y)) <> ((M | S) . j) by A4, A24, A52, FUNCT_1:def 4;

            then ((M * p) . y) <> LMj by A25, A29, A48, A52, FUNCT_1: 47;

            then

             A53: not ((M * p) . y) in LM by A29, TARSKI:def 1;

            assume not y in ( dom ML1);

            then

            consider w be Nat such that

             A54: w in ( dom ML2) and

             A55: Y = (( len ML1) + w) by A35, A37, A47, FINSEQ_1: 25;

            ((M * p) . Y) = (ML2 . w) by A35, A54, A55, FINSEQ_1:def 7;

            hence contradiction by A22, A53, A54, FUNCT_1:def 3;

          end;

          then ((M * p) | pSj) = (((M * p) | (p " S)) | pSj) & ((M * p) | pSj) = (ML1 | pSj) by A35, FINSEQ_6: 11, RELAT_1: 74, XBOOLE_1: 36;

          then

           A56: (ML1 | pSj) is one-to-one by A4, A36, FUNCT_1: 52;

          ( dom p) = ( Seg n) & (p . ppj) = j by A28, A38, FUNCT_1: 35, FUNCT_2: 52;

          then

           A57: ppj in ( dom ((M | S) * p)) by A24, A40, FUNCT_1: 11;

          then (((M | S) * p) . ppj) = LMj by A25, A29, A41, FUNCT_1: 12;

          

          then

           A58: LM = ( Im (((M | S) * p),ppj)) by A29, A57, FUNCT_1: 59

          .= (((M * p) | (p " S)) .: {ppj}) by A36, RELAT_1:def 16;

          ( rng M) = ( rng ((M * p) | (p " S))) by A5, A36, A38, A45, RELAT_1: 28

          .= ((M * p) .: (p " S)) by RELAT_1: 115

          .= (((M * p) | (p " S)) .: (p " S)) by RELAT_1: 129;

          

          then

           A59: ( rng ML1) = (((M * p) | (p " S)) .: pSj) by A4, A36, A32, A58, FUNCT_1: 64

          .= ( rng (((M * p) | (p " S)) | pSj)) by RELAT_1: 115

          .= ( rng ((M * p) | pSj)) by RELAT_1: 74, XBOOLE_1: 36

          .= ( rng (ML1 | pSj)) by A35, A46, FINSEQ_6: 11;

          reconsider fp = (f * p) as n -element FinSequence of REAL by MATRTOP1: 21;

          

           A60: (n1 + n2) = ( len (ML1 ^ ML2)) by MATRIX_0:def 2

          .= ( len (M * p)) by A35

          .= n by MATRIX_0:def 2;

          ( len fp) = n by CARD_1:def 7;

          then

          consider fp1,fp2 be FinSequence of REAL such that

           A61: ( len fp1) = n1 and

           A62: ( len fp2) = n2 and

           A63: fp = (fp1 ^ fp2) by A60, FINSEQ_2: 23;

          

           A64: fp2 is n2 -element by A62, CARD_1:def 7;

          then

           A65: ( len (( Mx2Tran ML2) . fp2)) = m by CARD_1:def 7;

          ( card LM) = 1 by CARD_2: 42;

          then

          consider L2 be Linear_Combination of ( lines ML2) such that

           A66: ( Sum L2) = (( Mx2Tran ML2) . fp2) and

           A67: for i be Nat st i in ( Seg n2) holds (L2 . ( Line (ML2,i))) = ( Sum fp2) & (ML2 " {( Line (ML2,i))}) = ( dom fp2) by A64, A22, Lm5;

          

           A68: fp1 is n1 -element by A61, CARD_1:def 7;

          then ( len (( Mx2Tran ML1) . fp1)) = m by CARD_1:def 7;

          then

          reconsider Mf1 = ( @ (( Mx2Tran ML1) . fp1)), Mf2 = ( @ (( Mx2Tran ML2) . fp2)) as Element of (m -tuples_on the carrier of F_Real ) by A65, FINSEQ_2: 92;

          

           A69: ( Carrier L2) c= ( lines ML2) by VECTSP_6:def 4;

          ( len ML1) = n1 by A7, A18, XREAL_1: 49, XREAL_1: 233;

          then pSj is Subset of ( Seg n1) by A46, FINSEQ_1:def 3;

          then

          consider L1 be Linear_Combination of ( lines ML1) such that

           A70: ( Sum L1) = (( Mx2Tran ML1) . fp1) and

           A71: for i be Nat st i in pSj holds (L1 . ( Line (ML1,i))) = ( Sum ( Seq (fp1 | (ML1 " {( Line (ML1,i))})))) by A2, A68, A21, A56, A59, A34;

          

           A72: ( Carrier L1) c= ( lines ML1) by VECTSP_6:def 4;

          (( rng ML1) \/ ( rng ML2)) = ( [#] ( lines M)) by A22, A33, SUBSET_1: 10

          .= ( lines M) by SUBSET_1:def 3;

          then (L1 is Linear_Combination of ( lines M)) & L2 is Linear_Combination of ( lines M) by VECTSP_6: 4, XBOOLE_1: 7;

          then

          reconsider L12 = (L1 + L2) as Linear_Combination of ( lines M) by VECTSP_6: 24;

          take L12;

          

          thus (( Mx2Tran M) . f) = (( Mx2Tran (ML1 ^ ML2)) . (fp1 ^ fp2)) by A35, A60, A63, MATRTOP1: 21

          .= ((( Mx2Tran ML1) . fp1) + (( Mx2Tran ML2) . fp2)) by A68, A64, MATRTOP1: 36

          .= (Mf1 + Mf2) by MATRTOP1: 1

          .= (( Sum L1) + ( Sum L2)) by A70, A66, MATRIX13: 102

          .= ( Sum L12) by VECTSP_6: 44;

          let w be Nat such that

           A73: w in S;

          ( Line (M,w)) in ( lines M) by A73, MATRIX13: 103;

          then

          reconsider LMw = ( Line (M,w)) as Element of V;

          (p " (M " {LMw})) = ((M * p) " {LMw}) by RELAT_1: 146;

          

          then

           A74: ( Sum ( Seq (f | (M " {LMw})))) = ( Sum ( Seq (fp | ((M * p) " {LMw})))) by A23, MATRTOP1: 10

          .= ( Sum (( Seq (fp1 | (ML1 " {LMw}))) ^ ( Seq (fp2 | (ML2 " {LMw}))))) by A7, A35, A61, A62, A63, A18, A30, A19, A31, MATRTOP1: 13

          .= (( Sum ( Seq (fp1 | (ML1 " {LMw})))) + ( Sum ( Seq (fp2 | (ML2 " {LMw}))))) by RVSUM_1: 75;

          set ppw = ((pp " ) . w);

          

           A75: ppw in (p " S) by A39, A73, FUNCT_1:def 6;

          (p . ppw) = w by A38, A73, FUNCT_1: 35;

          then

           A76: ((M * P) . ppw) = (M . w) by A37, A75, FUNCT_1: 12;

          reconsider ppw as Nat by A75;

          

           A77: (M . w) = LMw by A73, MATRIX_0: 52;

          reconsider L1w = (L1 . LMw), L2w = (L2 . LMw) as Element of FR;

          

           A78: (L12 . LMw) = (L1w + L2w) by VECTSP_6: 22;

          per cases by A35, A37, A75, FINSEQ_1: 25;

            suppose

             A79: ppw in ( dom ML1);

            then

             A80: (ML1 . ppw) = LMw by A35, A76, A77, FINSEQ_1:def 7;

            then

             A81: LMw in ( rng ML1) by A79, FUNCT_1:def 3;

            then not LMw in ( Carrier L2) by A22, A33, A69, A16, XBOOLE_0: 3;

            then

             A82: (L2 . LMw) = ( 0. F_Real ) by VECTSP_6: 2;

             not LMw in ( rng ML2) by A22, A33, A16, A81, XBOOLE_0: 3;

            then {LMw} misses ( rng ML2) by ZFMISC_1: 50;

            then (ML2 " {LMw}) = {} by RELAT_1: 138;

            then

             A83: ( Sum ( Seq (fp2 | (ML2 " {LMw})))) = 0 by RVSUM_1: 72;

            ( Line (ML1,ppw)) = (ML1 . ppw) & ppw in pSj by A75, A42, A79, MATRIX_0: 60, ZFMISC_1: 56;

            then (L1 . LMw) = ( Sum ( Seq (fp1 | (ML1 " {LMw})))) by A71, A80;

            hence thesis by A74, A78, A82, A83, RLVECT_1:def 4;

          end;

            suppose ex z be Nat st z in ( dom ML2) & ppw = (( len ML1) + z);

            then

            consider z be Nat such that

             A84: z in ( dom ML2) and

             A85: ppw = (( len ML1) + z);

            

             A86: (ML2 . z) = LMw by A35, A76, A77, A84, A85, FINSEQ_1:def 7;

            then

             A87: LMw in ( rng ML2) by A84, FUNCT_1:def 3;

            then not LMw in ( Carrier L1) by A22, A33, A72, A16, XBOOLE_0: 3;

            then

             A88: (L1 . LMw) = ( 0. F_Real ) by VECTSP_6: 2;

             not LMw in (LM ` ) by A22, A16, A87, XBOOLE_0: 3;

            then {LMw} misses ( rng ML1) by A33, ZFMISC_1: 50;

            then (ML1 " {LMw}) = {} by RELAT_1: 138;

            then

             A89: ( Seq (fp1 | (ML1 " {LMw}))) = ( <*> REAL );

            (L1w + L2w) = (L2w + L1w) by RLVECT_1:def 2;

            then

             A90: (L12 . LMw) = (L2 . LMw) by A78, A88, RLVECT_1:def 4;

            

             A91: ( dom ML2) = ( Seg n2) by A7, A30, A31, FINSEQ_1:def 3;

            

             A92: (ML2 . z) = ( Line (ML2,z)) by A84, MATRIX_0: 60;

            then (ML2 " {LMw}) = ( dom fp2) by A67, A84, A86, A91;

            then

             A93: (fp2 | (ML2 " {LMw})) = fp2;

            (L2 . LMw) = ( Sum fp2) by A67, A84, A86, A92, A91;

            hence thesis by A74, A90, A89, A93, FINSEQ_3: 116, RVSUM_1: 72;

          end;

        end;

      end;

      

       A94: P[ 0 ]

      proof

        let n, m, M, f;

        let S be Subset of ( Seg n) such that

         A95: n = 0 implies m = 0 and (M | S) is one-to-one and ( rng (M | S)) = ( lines M) and

         A96: ( card ( lines M)) = 0 ;

        reconsider L = ( ZeroLC (m -VectSp_over F_Real )) as Linear_Combination of ( lines M) by VECTSP_6: 5;

        take L;

        

         A97: ( Sum L) = ( 0. (m -VectSp_over F_Real )) by VECTSP_6: 15

        .= ( 0. ( TOP-REAL m)) by Lm2;

        

         A98: ( len M) = n & M = {} by A95, A96, MATRIX13: 1;

        thus ( Sum L) = (( Mx2Tran M) . f) by A95, A98, A97;

        let i be Nat;

        thus thesis by A98;

      end;

      for i be Nat holds P[i] from NAT_1:sch 2( A94, A1);

      then

       A99: P[( card ( lines M))];

      per cases ;

        suppose n <> 0 ;

        hence thesis by A99;

      end;

        suppose

         A100: n = 0 ;

        let S be Subset of ( Seg n) such that (M | S) is one-to-one & ( rng (M | S)) = ( lines M);

        reconsider L = ( ZeroLC (m -VectSp_over F_Real )) as Linear_Combination of ( lines M) by VECTSP_6: 5;

        take L;

        

        thus ( Sum L) = ( 0. (m -VectSp_over F_Real )) by VECTSP_6: 15

        .= ( 0. ( TOP-REAL m)) by Lm2

        .= (( Mx2Tran M) . f) by A100, MATRTOP1:def 3;

        thus thesis by A100;

      end;

    end;

    theorem :: MATRTOP2:16

    

     Th16: M is without_repeated_line implies ex L be Linear_Combination of ( lines M) st ( Sum L) = (( Mx2Tran M) . f) & for k st k in ( dom f) holds (L . ( Line (M,k))) = (f . k)

    proof

      assume that

       A1: M is without_repeated_line;

      

       A2: ( len M) = n by MATRIX_0:def 2;

      then ( dom M) c= ( Seg n) by FINSEQ_1:def 3;

      then

      reconsider D = ( dom M) as Subset of ( Seg n);

      ( len f) = n by CARD_1:def 7;

      then

       A3: ( dom f) = ( dom M) by A2, FINSEQ_3: 29;

      (M | ( dom M)) = M;

      then

      consider L be Linear_Combination of ( lines M) such that

       A4: ( Sum L) = (( Mx2Tran M) . f) and

       A5: for i be Nat st i in D holds (L . ( Line (M,i))) = ( Sum ( Seq (f | (M " {( Line (M,i))})))) by A1, Th15;

      take L;

      thus ( Sum L) = (( Mx2Tran M) . f) by A4;

      let i be Nat such that

       A6: i in ( dom f);

      i >= 1 by A6, FINSEQ_3: 25;

      then

       A7: ( Sgm {i}) = <*i*> by FINSEQ_3: 44;

      set LM = ( Line (M,i));

      

       A8: LM in {LM} by TARSKI:def 1;

      ( dom M) = ( Seg n) by A2, FINSEQ_1:def 3;

      then LM in ( lines M) by A3, A6, MATRIX13: 103;

      then

      consider x be object such that

       A9: (M " {LM}) = {x} by A1, FUNCT_1: 74;

      

       A10: ( dom (f | {i})) = (( dom f) /\ {i}) by RELAT_1: 61;

       {i} c= ( dom f) by A6, ZFMISC_1: 31;

      then

       A11: ( dom (f | {i})) = {i} by A10, XBOOLE_1: 28;

      then i in ( dom (f | {i})) by TARSKI:def 1;

      then

       A12: ((f | {i}) . i) = (f . i) by FUNCT_1: 47;

      ( rng <*i*>) = {i} by FINSEQ_1: 38;

      then

       A13: <*i*> is FinSequence of {i} by FINSEQ_1:def 4;

      ( rng (f | {i})) <> {} & (f | {i}) is Function of {i}, ( rng (f | {i})) by A11, FUNCT_2: 1, RELAT_1: 42;

      then ( Seq (f | {i})) = <*(f . i)*> by A11, A7, A13, A12, FINSEQ_2: 35;

      then

       A14: ( Sum ( Seq (f | {i}))) = (f . i) by RVSUM_1: 73;

      (M . i) = LM by A3, A6, MATRIX_0: 60;

      then i in (M " {LM}) by A3, A6, A8, FUNCT_1:def 7;

      then (f | (M " {LM})) = (f | {i}) by A9, TARSKI:def 1;

      hence thesis by A5, A3, A6, A14;

    end;

    theorem :: MATRTOP2:17

    for B be OrdBasis of ( Lin ( lines M)) st B = M holds for Mf be Element of ( Lin ( lines M)) st Mf = (( Mx2Tran M) . f) holds (Mf |-- B) = f

    proof

      set LM = ( lines M);

      let B be OrdBasis of ( Lin LM) such that

       A1: B = M;

      

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

      let Mf be Element of ( Lin LM) such that

       A3: Mf = (( Mx2Tran M) . f);

      consider L be Linear_Combination of LM such that

       A4: ( Sum L) = Mf and

       A5: for i be Nat st i in ( dom f) holds (L . ( Line (M,i))) = (f . i) by A1, A3, A2, Th16;

      reconsider L1 = (L | the carrier of ( Lin LM)) as Linear_Combination of ( Lin LM) by Th8;

      

       A6: ( len M) = n by MATRIX_0:def 2;

      

       A7: ( len f) = n by CARD_1:def 7;

      

       A8: LM c= ( [#] ( Lin LM)) by Lm4;

       A9:

      now

        let k;

        assume

         A10: 1 <= k & k <= n;

        then k in ( Seg n);

        then

         A11: (M . k) = ( Line (M,k)) by MATRIX_0: 52;

        

         A12: k in ( dom M) by A6, A10, FINSEQ_3: 25;

        then

         A13: (B /. k) = (M . k) by A1, PARTFUN1:def 6;

        (M . k) in LM by A12, FUNCT_1:def 3;

        then

         A14: (L . (M . k)) = (L1 . (M . k)) by A8, FUNCT_1: 49;

        

         A15: k in ( dom f) by A7, A10, FINSEQ_3: 25;

        then (f . k) = (( @ f) /. k) by PARTFUN1:def 6;

        hence (( @ f) /. k) = (L1 . (B /. k)) by A5, A15, A13, A11, A14;

      end;

      

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

      then ( Carrier L) c= ( [#] ( Lin LM)) by A8;

      then ( Carrier L) = ( Carrier L1) & ( Sum L1) = ( Sum L) by VECTSP_9: 7;

      hence thesis by A1, A4, A6, A7, A16, A9, MATRLIN:def 7;

    end;

    theorem :: MATRTOP2:18

    

     Th18: ( rng ( Mx2Tran M)) = ( [#] ( Lin ( lines M)))

    proof

      consider X be set such that

       A1: X c= ( dom M) and

       A2: ( lines M) = ( rng (M | X)) and

       A3: (M | X) is one-to-one by MATRTOP1: 6;

      set V = (m -VectSp_over F_Real );

      set TM = ( Mx2Tran M);

      

       A4: ( len M) = n by MATRIX_0:def 2;

      then

      reconsider X as Subset of ( Seg n) by A1, FINSEQ_1:def 3;

      hereby

        let y be object;

        assume y in ( rng TM);

        then

        consider x be object such that

         A5: x in ( dom TM) and

         A6: (TM . x) = y by FUNCT_1:def 3;

        reconsider x as Element of ( TOP-REAL n) by A5;

        consider L be Linear_Combination of ( lines M) such that

         A7: ( Sum L) = y and for i be Nat st i in X holds (L . ( Line (M,i))) = ( Sum ( Seq (x | (M " {( Line (M,i))})))) by A2, A3, A6, Th15;

        ( Sum L) in ( Lin ( lines M)) by VECTSP_7: 7;

        hence y in ( [#] ( Lin ( lines M))) by A7;

      end;

      let y be object;

      assume y in ( [#] ( Lin ( lines M)));

      then y in ( Lin ( lines M));

      then

      consider L be Linear_Combination of ( lines M) such that

       A8: y = ( Sum L) by VECTSP_7: 7;

      defpred P[ set, object] means ($1 in X implies $2 = (L . (M . $1))) & ( not $1 in X implies $2 = 0 );

      

       A9: for i be Nat st i in ( Seg n) holds ex x be object st P[i, x]

      proof

        let i be Nat such that i in ( Seg n);

        i in X or not i in X;

        hence thesis;

      end;

      consider f be FinSequence such that

       A10: ( dom f) = ( Seg n) & for j be Nat st j in ( Seg n) holds P[j, (f . j)] from FINSEQ_1:sch 1( A9);

      

       A11: ( dom M) = ( Seg n) by A4, FINSEQ_1:def 3;

      ( rng f) c= REAL

      proof

        let z be object;

        assume z in ( rng f);

        then

        consider x be object such that

         A12: x in ( dom f) and

         A13: (f . x) = z by FUNCT_1:def 3;

        reconsider x as Nat by A12;

        

         A14: P[x, (f . x)] by A10, A12;

        (M . x) = ( Line (M,x)) by A11, A10, A12, MATRIX_0: 60;

        then (M . x) in ( lines M) by A10, A12, MATRIX13: 103;

        then

        reconsider Mx = (M . x) as Element of V;

        per cases ;

          suppose not x in X;

          then (f . x) = ( In ( 0 , REAL )) by A10, A12;

          hence thesis by A13;

        end;

          suppose x in X;

          thus thesis by A13, A14, XREAL_0:def 1;

        end;

      end;

      then

      reconsider f as FinSequence of REAL by FINSEQ_1:def 4;

      ( len f) = n by A4, A10, FINSEQ_1:def 3;

      then

       A15: f is n -element by CARD_1:def 7;

      then

      consider K be Linear_Combination of ( lines M) such that

       A16: ( Sum K) = (TM . f) and

       A17: for i be Nat st i in X holds (K . ( Line (M,i))) = ( Sum ( Seq (f | (M " {( Line (M,i))})))) by A2, A3, Th15;

      now

        let v be Element of V;

        per cases ;

          suppose v in ( lines M);

          then

          consider i be object such that

           A18: i in ( dom (M | X)) and

           A19: ((M | X) . i) = v by A2, FUNCT_1:def 3;

          

           A20: (M . i) = v by A18, A19, FUNCT_1: 47;

          set D = ( dom (f | (M " {v})));

          ( Seq (f | (M " {v}))) = ( @ ( @ ( Seq (f | (M " {v})))));

          then

          reconsider F = ( Seq (f | (M " {v}))) as FinSequence of REAL ;

          

           A21: ( rng ( Sgm D)) = D by FINSEQ_1: 50;

          then

           A22: ( dom F) = ( dom ( Sgm D)) by RELAT_1: 27;

          

           A23: i in ( dom M) by A18, RELAT_1: 57;

          

           A24: i in X by A18;

          reconsider i as Nat by A18;

          (M . i) = ( Line (M,i)) by A23, MATRIX_0: 60;

          then

           A25: (K . v) = ( Sum ( Seq (f | (M " {v})))) by A17, A24, A20;

          v in {v} by TARSKI:def 1;

          then i in (M " {v}) by A23, A20, FUNCT_1:def 7;

          then i in D by A10, A24, RELAT_1: 57;

          then

          consider j be object such that

           A26: j in ( dom ( Sgm D)) and

           A27: (( Sgm D) . j) = i by A21, FUNCT_1:def 3;

          reconsider j as Element of NAT by A26;

          (F . j) = ((f | (M " {v})) . i) & i in D by A22, A26, A27, FUNCT_1: 11, FUNCT_1: 12;

          then

           A28: (F . j) = (f . i) by FUNCT_1: 47;

          D c= ( dom f) by RELAT_1: 60;

          then

           A29: ( Sgm D) is one-to-one by A10, FINSEQ_3: 92;

          now

            let w be Nat;

            assume that

             A30: w in ( dom F) and

             A31: w <> j;

            

             A32: (( Sgm D) . w) in D by A21, A22, A30, FUNCT_1:def 3;

            then (( Sgm D) . w) in (M " {v}) by RELAT_1: 57;

            then (M . (( Sgm D) . w)) in {v} by FUNCT_1:def 7;

            then

             A33: (M . (( Sgm D) . w)) = v by TARSKI:def 1;

            

             A34: not (( Sgm D) . w) in X

            proof

              assume (( Sgm D) . w) in X;

              then

               A35: (( Sgm D) . w) in ( dom (M | X)) by A11, RELAT_1: 57;

              then v = ((M | X) . (( Sgm D) . w)) by A33, FUNCT_1: 47;

              then i = (( Sgm D) . w) by A3, A18, A19, A35, FUNCT_1:def 4;

              hence contradiction by A22, A29, A26, A27, A30, A31, FUNCT_1:def 4;

            end;

            (F . w) = ((f | (M " {v})) . (( Sgm D) . w)) by A30, FUNCT_1: 12;

            then

             A36: (F . w) = (f . (( Sgm D) . w)) by A32, FUNCT_1: 47;

            (( Sgm D) . w) in ( dom f) by A32, RELAT_1: 57;

            hence (F . w) = 0 by A10, A36, A34;

          end;

          then

           A37: F has_onlyone_value_in j by A22, A26, ENTROPY1:def 2;

          (f . i) = (L . v) by A10, A24, A20;

          hence (L . v) = (K . v) by A25, A28, A37, ENTROPY1: 13;

        end;

          suppose

           A38: not v in ( lines M);

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

          then not v in ( Carrier L) by A38;

          then

           A39: (L . v) = ( 0. F_Real ) by VECTSP_6: 2;

          ( Carrier K) c= ( lines M) by VECTSP_6:def 4;

          then not v in ( Carrier K) by A38;

          hence (L . v) = (K . v) by A39, VECTSP_6: 2;

        end;

      end;

      then

       A40: ( Sum K) = ( Sum L) by VECTSP_6:def 7;

      ( dom TM) = ( [#] ( TOP-REAL n)) & f is Point of ( TOP-REAL n) by A15, Lm3, FUNCT_2:def 1;

      hence thesis by A8, A16, A40, FUNCT_1:def 3;

    end;

    theorem :: MATRTOP2:19

    

     Th19: for F be one-to-one FinSequence of ( TOP-REAL n) st ( rng F) is linearly-independent holds ex M be Matrix of n, F_Real st M is invertible & (M | ( len F)) = F

    proof

      let F be one-to-one FinSequence of ( TOP-REAL n) such that

       A1: ( rng F) is linearly-independent;

      reconsider f = F as FinSequence of (n -VectSp_over F_Real ) by Lm1;

      set M = ( FinS2MX f);

      ( lines M) is linearly-independent by A1, Th7;

      then

       A2: ( the_rank_of M) = ( len F) by MATRIX13: 121;

      then

      consider A be Matrix of (n -' ( len F)), n, F_Real such that

       A3: ( the_rank_of (M ^ A)) = n by MATRTOP1: 16;

      ( len F) <= ( width M) by A2, MATRIX13: 74;

      then ( len F) <= n by MATRIX_0: 23;

      then (n - ( len F)) = (n -' ( len F)) by XREAL_1: 233;

      then

      reconsider MA = (M ^ A) as Matrix of n, F_Real ;

      take MA;

      ( Det MA) <> ( 0. F_Real ) by A3, MATRIX13: 83;

      hence MA is invertible by LAPLACE: 34;

      

      thus F = (MA | ( dom F)) by FINSEQ_1: 21

      .= (MA | ( len F)) by FINSEQ_1:def 3;

    end;

    theorem :: MATRTOP2:20

    

     Th20: for B be OrdBasis of (n -VectSp_over F_Real ) st B = ( MX2FinS ( 1. ( F_Real ,n))) holds f in ( Lin ( rng (B | k))) iff f = ((f | k) ^ ((n -' k) |-> 0 ))

    proof

      set V = (n -VectSp_over F_Real );

      set nk0 = ((n -' k) |-> 0 );

      let B be OrdBasis of (n -VectSp_over F_Real ) such that

       A1: B = ( MX2FinS ( 1. ( F_Real ,n)));

      

       A2: ( len B) = n by A1, MATRIX_0:def 2;

      

       A3: f is Point of ( TOP-REAL n) by Lm3;

      then

       A4: f is Point of V by Lm1;

      

       A5: ( rng B) is Basis of V by MATRLIN:def 2;

      then

       A6: ( rng B) is linearly-independent by VECTSP_7:def 3;

      ( Lin ( rng B)) = the ModuleStr of V by A5, VECTSP_7:def 3;

      then

       A7: f in ( Lin ( rng B)) by A4;

      

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

      reconsider F = f as Point of V by A3, Lm1;

      

       A9: ( len f) = n by CARD_1:def 7;

      per cases ;

        suppose

         A10: k >= n;

        then (n - k) <= 0 by XREAL_1: 47;

        then (n -' k) = 0 by XREAL_0:def 2;

        then

         A11: nk0 = {} ;

        (f | k) = f by A9, A10, FINSEQ_1: 58;

        hence thesis by A2, A7, A10, A11, FINSEQ_1: 34, FINSEQ_1: 58;

      end;

        suppose

         A12: k < n;

        then

         A13: ( len (f | k)) = k by A9, FINSEQ_1: 59;

        

         A14: ( len nk0) = (n -' k) by CARD_1:def 7;

        consider KL be Linear_Combination of V such that

         A15: F = ( Sum KL) and

         A16: ( Carrier KL) c= ( rng B) and

         A17: for k st 1 <= k & k <= ( len (F |-- B)) holds ((F |-- B) /. k) = (KL . (B /. k)) by MATRLIN:def 7;

        reconsider KL as Linear_Combination of ( rng B) by A16, VECTSP_6:def 4;

        

         A18: (F |-- B) = F by A1, A2, MATRLIN2: 46;

        (n -' k) = (n - k) by A12, XREAL_1: 233;

        then ( len ((f | k) ^ nk0)) = (k + (n - k)) by A13, A14, FINSEQ_1: 22;

        then

         A19: ( dom ((f | k) ^ nk0)) = ( dom f) by A9, FINSEQ_3: 29;

        hereby

          assume f in ( Lin ( rng (B | k)));

          then

          consider L be Linear_Combination of ( rng (B | k)) such that

           A20: ( Sum L) = f by VECTSP_7: 7;

          reconsider L1 = L as Linear_Combination of ( rng B) by RELAT_1: 70, VECTSP_6: 4;

          

           A21: (KL - L1) is Linear_Combination of ( rng B) by VECTSP_6: 42;

          ( Sum (KL - L1)) = (( Sum KL) - ( Sum L1)) by VECTSP_6: 47

          .= ( 0. V) by A15, A20, VECTSP_1: 19;

          then ( Carrier (KL - L1)) = {} by A6, A21, VECTSP_7:def 1;

          

          then

           A22: ( ZeroLC V) = (KL - L1) by VECTSP_6:def 3

          .= (KL + ( - L1)) by VECTSP_6:def 11

          .= (( - L1) + KL) by VECTSP_6: 25;

          reconsider M1 = ( - ( 1. F_Real )) as Element of F_Real ;

          

           A23: ( Carrier L) c= ( rng (B | k)) by VECTSP_6:def 4;

          L1 = ( - ( - L1));

          then

           A24: KL = L1 by A22, VECTSP_6: 37;

          now

            let i be Nat;

            assume

             A25: i in ( dom f);

            per cases by A13, A19, A25, FINSEQ_1: 25;

              suppose

               A26: i in ( dom (f | k));

              then ((f | k) . i) = (f . i) by FUNCT_1: 47;

              hence (((f | k) ^ nk0) . i) = (f . i) by A26, FINSEQ_1:def 7;

            end;

              suppose

               A27: ex j be Nat st j in ( dom nk0) & i = (k + j);

              

               A28: i in ( dom B) by A9, A2, A25, FINSEQ_3: 29;

              then

               A29: (B /. i) = (B . i) by PARTFUN1:def 6;

              consider j be Nat such that

               A30: j in ( dom nk0) and

               A31: i = (k + j) by A27;

              

               A32: 1 <= j by A30, FINSEQ_3: 25;

               not (B . i) in ( rng (B | k))

              proof

                assume (B . i) in ( rng (B | k));

                then

                consider x be object such that

                 A33: x in ( dom (B | k)) and

                 A34: ((B | k) . x) = (B . i) by FUNCT_1:def 3;

                (B . x) = (B . i) & x in ( dom B) by A33, A34, FUNCT_1: 47, RELAT_1: 57;

                then

                 A35: i = x by A8, A28, FUNCT_1:def 4;

                x in ( Seg k) by A33, RELAT_1: 57;

                then

                 A36: i <= k by A35, FINSEQ_1: 1;

                i >= (k + 1) by A31, A32, XREAL_1: 6;

                hence contradiction by A36, NAT_1: 13;

              end;

              then

               A37: not (B . i) in ( Carrier L) by A23;

              1 <= i & i <= n by A9, A25, FINSEQ_3: 25;

              then

               A38: ((F |-- B) /. i) = (KL . (B /. i)) by A9, A18, A17;

              (f . i) = ((F |-- B) /. i) by A18, A25, PARTFUN1:def 6;

              

              hence (f . i) = ( 0. F_Real ) by A24, A38, A29, A37, VECTSP_6: 2

              .= (nk0 . j)

              .= (((f | k) ^ nk0) . i) by A13, A30, A31, FINSEQ_1:def 7;

            end;

          end;

          hence ((f | k) ^ ((n -' k) |-> 0 )) = f by A19, FINSEQ_1: 13;

        end;

        assume

         A39: ((f | k) ^ nk0) = f;

        ( Carrier KL) c= ( rng (B | k))

        proof

          let x be object;

          assume

           A40: x in ( Carrier KL);

          ( Carrier KL) c= ( rng B) by VECTSP_6:def 4;

          then

          consider i be object such that

           A41: i in ( dom B) and

           A42: (B . i) = x by A40, FUNCT_1:def 3;

          reconsider i as Element of NAT by A41;

          

           A43: (B /. i) = (B . i) by A41, PARTFUN1:def 6;

          

           A44: ( dom B) = ( dom f) by A9, A2, FINSEQ_3: 29;

          assume

           A45: not x in ( rng (B | k));

           not i in ( Seg k)

          proof

            assume i in ( Seg k);

            then

             A46: i in ( dom (B | k)) by A41, RELAT_1: 57;

            then ((B | k) . i) = (B . i) by FUNCT_1: 47;

            hence contradiction by A42, A45, A46, FUNCT_1:def 3;

          end;

          then not i in ( dom (f | k)) by A13, FINSEQ_1:def 3;

          then

          consider j be Nat such that

           A47: j in ( dom nk0) and

           A48: i = (k + j) by A13, A19, A41, A44, FINSEQ_1: 25;

          

           A49: (nk0 . j) = 0 ;

          

           A50: 1 <= i & i <= n by A2, A41, FINSEQ_3: 25;

          ((F |-- B) /. i) = ((F |-- B) . i) by A18, A41, A44, PARTFUN1:def 6;

          

          then (KL . (B /. i)) = (f . i) by A9, A18, A17, A50

          .= ( 0. F_Real ) by A13, A39, A47, A48, A49, FINSEQ_1:def 7;

          hence contradiction by A40, A42, A43, VECTSP_6: 2;

        end;

        then KL is Linear_Combination of ( rng (B | k)) by VECTSP_6:def 4;

        hence thesis by A15, VECTSP_7: 7;

      end;

    end;

    theorem :: MATRTOP2:21

    

     Th21: for F be one-to-one FinSequence of ( TOP-REAL n) st ( rng F) is linearly-independent holds for B be OrdBasis of (n -VectSp_over F_Real ) st B = ( MX2FinS ( 1. ( F_Real ,n))) holds for M be Matrix of n, F_Real st M is invertible & (M | ( len F)) = F holds (( Mx2Tran M) .: ( [#] ( Lin ( rng (B | ( len F)))))) = ( [#] ( Lin ( rng F)))

    proof

      let F be one-to-one FinSequence of ( TOP-REAL n) such that

       A1: ( rng F) is linearly-independent;

      reconsider f = F as FinSequence of (n -VectSp_over F_Real ) by Lm1;

      set MF = ( FinS2MX f);

      set n1 = (n -' ( len F));

      set L = ( len F);

      ( lines MF) is linearly-independent by A1, Th7;

      then ( the_rank_of MF) = ( len F) by MATRIX13: 121;

      then L <= ( width MF) by MATRIX13: 74;

      then

       A2: L <= n by MATRIX_0: 23;

      then

       A3: (n - L) = n1 by XREAL_1: 233;

      set V = (n -VectSp_over F_Real );

      let B be OrdBasis of (n -VectSp_over F_Real ) such that

       A4: B = ( MX2FinS ( 1. ( F_Real ,n)));

      let M be Matrix of n, F_Real such that M is invertible and

       A5: (M | ( len F)) = F;

      consider q be FinSequence such that

       A6: M = (F ^ q) by A5, FINSEQ_1: 80;

      M = ( MX2FinS M);

      then

      reconsider q as FinSequence of (n -VectSp_over F_Real ) by A6, FINSEQ_1: 36;

      

       A7: ( len M) = (( len F) + ( len q)) by A6, FINSEQ_1: 22;

      set Mq = ( FinS2MX q);

      set MT = ( Mx2Tran M);

      

       A8: ( len M) = n by MATRIX_0:def 2;

      

       A9: ( dom MT) = ( [#] ( TOP-REAL n)) by FUNCT_2: 52;

      

       A10: ( dom ( Mx2Tran MF)) = ( [#] ( TOP-REAL L)) by FUNCT_2:def 1;

      

       A11: the carrier of ( TOP-REAL n) = ( REAL n) by EUCLID: 22

      .= (n -tuples_on REAL );

      

       A12: ( rng ( Mx2Tran MF)) = ( [#] ( Lin ( lines MF))) by Th18

      .= ( [#] ( Lin ( rng F))) by Th6;

      

       A13: (n |-> 0 ) = ( 0* n)

      .= ( 0. ( TOP-REAL n)) by EUCLID: 70;

      

       A14: (n1 |-> 0 ) = ( 0* n1)

      .= ( 0. ( TOP-REAL n1)) by EUCLID: 70;

      then

       A15: (( Mx2Tran Mq) . (n1 |-> 0 )) = ( 0. ( TOP-REAL n)) by A3, A8, A7, MATRTOP1: 29;

      thus (MT .: ( [#] ( Lin ( rng (B | L))))) c= ( [#] ( Lin ( rng F)))

      proof

        let y be object;

        assume y in (MT .: ( [#] ( Lin ( rng (B | L)))));

        then

        consider x be object such that

         A16: x in ( dom MT) and

         A17: x in ( [#] ( Lin ( rng (B | L)))) and

         A18: (MT . x) = y by FUNCT_1:def 6;

        reconsider x as Element of ( TOP-REAL n) by A16;

        ( len x) = n by CARD_1:def 7;

        then ( len (x | L)) = L by A2, FINSEQ_1: 59;

        then

         A19: (x | L) is L -element by CARD_1:def 7;

        then

         A20: (x | L) is Element of ( TOP-REAL L) by Lm3;

        

         A21: (( Mx2Tran MF) . (x | L)) is Element of (n -tuples_on REAL ) by A11, A19, Lm3;

        x in ( Lin ( rng (B | L))) by A17;

        then x = ((x | L) ^ ((n -' L) |-> 0 )) by A4, Th20;

        

        then y = ((( Mx2Tran MF) . (x | L)) + (( Mx2Tran Mq) . (n1 |-> 0 ))) by A3, A8, A6, A7, A18, A19, MATRTOP1: 36

        .= (( Mx2Tran MF) . (x | L)) by A13, A15, A21, RVSUM_1: 16;

        hence thesis by A12, A10, A20, FUNCT_1:def 3;

      end;

      let y be object;

      assume y in ( [#] ( Lin ( rng F)));

      then

      consider x be object such that

       A22: x in ( dom ( Mx2Tran MF)) and

       A23: (( Mx2Tran MF) . x) = y by A12, FUNCT_1:def 3;

      reconsider x as Element of ( TOP-REAL L) by A22;

      (( Mx2Tran MF) . x) is Element of ( TOP-REAL n) by Lm3;

      

      then

       A24: y = ((( Mx2Tran MF) . x) + ( 0. ( TOP-REAL n))) by A11, A13, A23, RVSUM_1: 16

      .= ((( Mx2Tran MF) . x) + (( Mx2Tran Mq) . (n1 |-> 0 ))) by A3, A8, A7, A14, MATRTOP1: 29

      .= (MT . (x ^ (n1 |-> 0 ))) by A6, A3, A8, A7, MATRTOP1: 36;

      set xx = (x ^ (n1 |-> 0 ));

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

      then ( dom x) = ( Seg L) by FINSEQ_1:def 3;

      then xx = ((xx | L) ^ (n1 |-> 0 )) by FINSEQ_1: 21;

      then xx in ( Lin ( rng (B | L))) by A4, A3, Th20;

      then

       A25: xx in ( [#] ( Lin ( rng (B | L))));

      xx is Element of ( TOP-REAL n) by A3, Lm3;

      hence thesis by A9, A24, A25, FUNCT_1:def 6;

    end;

    theorem :: MATRTOP2:22

    for A,B be linearly-independent Subset of ( TOP-REAL n) st ( card A) = ( card B) holds ex M be Matrix of n, F_Real st M is invertible & (( Mx2Tran M) .: ( [#] ( Lin A))) = ( [#] ( Lin B))

    proof

      set TRn = ( TOP-REAL n);

      let A,B be linearly-independent Subset of TRn such that

       A1: ( card A) = ( card B);

      reconsider BB = ( MX2FinS ( 1. ( F_Real ,n))) as OrdBasis of (n -VectSp_over F_Real ) by MATRLIN2: 45;

      set V = (n -VectSp_over F_Real );

      A is linearly-independent Subset of V by Lm1, Th7;

      then A is finite by VECTSP_9: 21;

      then

      consider fA be FinSequence such that

       A2: ( rng fA) = A and

       A3: fA is one-to-one by FINSEQ_4: 58;

      

       A4: ( len fA) = ( card A) by A2, A3, PRE_POLY: 19;

      B is linearly-independent Subset of V by Lm1, Th7;

      then B is finite by VECTSP_9: 21;

      then

      consider fB be FinSequence such that

       A5: ( rng fB) = B and

       A6: fB is one-to-one by FINSEQ_4: 58;

      

       A7: ( len fB) = ( card B) by A5, A6, PRE_POLY: 19;

      reconsider fA, fB as FinSequence of TRn by A2, A5, FINSEQ_1:def 4;

      consider MA be Matrix of n, F_Real such that

       A8: MA is invertible and

       A9: (MA | ( len fA)) = fA by A2, A3, Th19;

      

       A10: ( [#] ( Lin ( rng (BB | ( len fA))))) c= ( [#] V) by VECTSP_4:def 2;

      set Ma = ( Mx2Tran MA);

      

       A11: ( Det MA) <> ( 0. F_Real ) by A8, LAPLACE: 34;

      then

       A12: Ma is one-to-one by MATRTOP1: 40;

      then

       A13: ( rng (Ma " )) = ( dom Ma) by FUNCT_1: 33;

      

       A14: ( [#] ( TOP-REAL n)) = ( [#] V) & ( dom Ma) = ( [#] TRn) by Lm1, FUNCT_2: 52;

      ((Ma " ) " ( [#] ( Lin ( rng (BB | ( len fA)))))) = (Ma .: ( [#] ( Lin ( rng (BB | ( len fA)))))) by A12, FUNCT_1: 84

      .= ( [#] ( Lin A)) by A2, A3, A8, A9, Th21;

      then

       A15: ((Ma " ) .: ( [#] ( Lin A))) = ( [#] ( Lin ( rng (BB | ( len fB))))) by A1, A4, A7, A14, A13, A10, FUNCT_1: 77;

      consider MB be Matrix of n, F_Real such that

       A16: MB is invertible and

       A17: (MB | ( len fB)) = fB by A5, A6, Th19;

      set Mb = ( Mx2Tran MB);

      

       A18: n = 0 implies n = 0 ;

      then ( width (MA ~ )) = n by MATRIX13: 1;

      then

      reconsider mb = MB as Matrix of ( width (MA ~ )), n, F_Real ;

      

       A19: ( width MB) = n by A18, MATRIX13: 1;

      reconsider MM = ((MA ~ ) * mb) as Matrix of n, F_Real ;

      take MM;

      (MA ~ ) is invertible by A8;

      hence MM is invertible by A16, MATRIX_6: 45;

      (Mb * (Ma " )) = (( Mx2Tran mb) * (Ma " )) by A18, MATRIX13: 1

      .= (( Mx2Tran mb) * ( Mx2Tran (MA ~ ))) by A11, MATRTOP1: 43

      .= ( Mx2Tran ((MA ~ ) * mb)) by A18, MATRTOP1: 32

      .= ( Mx2Tran MM) by A18, A19, MATRIX13: 1;

      

      hence (( Mx2Tran MM) .: ( [#] ( Lin A))) = (Mb .: ( [#] ( Lin ( rng (BB | ( len fB)))))) by A15, RELAT_1: 126

      .= ( [#] ( Lin B)) by A5, A6, A16, A17, Th21;

    end;

    begin

    theorem :: MATRTOP2:23

    

     Th23: for A be linearly-independent Subset of ( TOP-REAL n) st ( the_rank_of M) = n holds (( Mx2Tran M) .: A) is linearly-independent

    proof

      let A be linearly-independent Subset of ( TOP-REAL n) such that

       A1: ( the_rank_of M) = n;

      set nV = (n -VectSp_over F_Real ), mV = (m -VectSp_over F_Real );

      reconsider Bn = ( MX2FinS ( 1. ( F_Real ,n))) as OrdBasis of nV by MATRLIN2: 45;

      reconsider Bm = ( MX2FinS ( 1. ( F_Real ,m))) as OrdBasis of mV by MATRLIN2: 45;

      

       A2: ( len Bm) = m by MATRTOP1: 19;

      ( len Bn) = n by MATRTOP1: 19;

      then

      reconsider M1 = M as Matrix of ( len Bn), ( len Bm), F_Real by A2;

      set MT = ( Mx2Tran (M1,Bn,Bm));

      

       A3: ( Mx2Tran M) = MT by MATRTOP1: 20;

      reconsider A1 = A as Subset of nV by Lm1;

      

       A4: A1 is linearly-independent by Th7;

      (MT .: A1) is linearly-independent

      proof

        assume (MT .: A1) is non linearly-independent;

        then

        consider L be Linear_Combination of (MT .: A1) such that

         A5: ( Carrier L) <> {} and

         A6: ( Sum L) = ( 0. mV) by RANKNULL: 41;

        

         A7: MT is one-to-one by A1, A3, MATRTOP1: 39;

        then

         A8: ( ker MT) = ( (0). nV) by RANKNULL: 15;

        

         A9: (MT | A1) is one-to-one by A7, FUNCT_1: 52;

        then

         A10: (MT @ (MT # L)) = L by RANKNULL: 43;

        (MT | ( Carrier (MT # L))) is one-to-one by A7, FUNCT_1: 52;

        then (MT .: ( Carrier (MT # L))) = ( Carrier L) by A10, RANKNULL: 39;

        then

         A11: ( Carrier (MT # L)) <> {} by A5;

        (MT . ( Sum (MT # L))) = ( 0. mV) by A6, A9, A10, Th14;

        then ( Sum (MT # L)) in ( ker MT) by RANKNULL: 10;

        then ( Sum (MT # L)) = ( 0. nV) by A8, VECTSP_4: 35;

        hence contradiction by A4, A11, VECTSP_7:def 1;

      end;

      hence thesis by A3, Th7;

    end;

    theorem :: MATRTOP2:24

    

     Th24: for A be affinely-independent Subset of ( TOP-REAL n) st ( the_rank_of M) = n holds (( Mx2Tran M) .: A) is affinely-independent

    proof

      set MT = ( Mx2Tran M);

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m);

      let A be affinely-independent Subset of TRn such that

       A1: ( the_rank_of M) = n;

      per cases ;

        suppose A is empty;

        then (MT .: A) is empty;

        hence thesis;

      end;

        suppose A is non empty;

        then

        consider v be Element of TRn such that

         A2: v in A and

         A3: ((( - v) + A) \ {( 0. TRn)}) is linearly-independent by RLAFFIN1:def 4;

        

         A4: ( dom MT) = ( [#] TRn) by FUNCT_2:def 1;

        then

         A5: (MT . v) in (MT .: A) by A2, FUNCT_1:def 6;

        (MT . ( 0. TRn)) = ( 0. TRm) by MATRTOP1: 29;

        

        then

         A6: {( 0. TRm)} = ( Im (MT,( 0. TRn))) by A4, FUNCT_1: 59

        .= (MT .: {( 0. TRn)}) by RELAT_1:def 16;

        ( - v) = (( 0. TRn) - v) by RLVECT_1: 14;

        

        then

         A7: (MT . ( - v)) = ((MT . ( 0. TRn)) - (MT . v)) by MATRTOP1: 28

        .= (( 0. TRm) - (MT . v)) by MATRTOP1: 29

        .= ( - (MT . v)) by RLVECT_1: 14;

        MT is one-to-one by A1, MATRTOP1: 39;

        

        then

         A8: (MT .: ((( - v) + A) \ {( 0. TRn)})) = ((MT .: (( - v) + A)) \ (MT .: {( 0. TRn)})) by FUNCT_1: 64

        .= ((( - (MT . v)) + (MT .: A)) \ {( 0. TRm)}) by A6, A7, MATRTOP1: 30;

        (MT .: ((( - v) + A) \ {( 0. TRn)})) is linearly-independent by A1, A3, Th23;

        hence thesis by A5, A8, RLAFFIN1:def 4;

      end;

    end;

    theorem :: MATRTOP2:25

    for A be affinely-independent Subset of ( TOP-REAL n) st ( the_rank_of M) = n holds for v be Element of ( TOP-REAL n) st v in ( Affin A) holds (( Mx2Tran M) . v) in ( Affin (( Mx2Tran M) .: A)) & for f holds ((v |-- A) . f) = (((( Mx2Tran M) . v) |-- (( Mx2Tran M) .: A)) . (( Mx2Tran M) . f))

    proof

      reconsider Z = 0 as Element of NAT ;

      set TRn = ( TOP-REAL n);

      set TRm = ( TOP-REAL m);

      let A be affinely-independent Subset of TRn such that

       A1: ( the_rank_of M) = n;

      set MT = ( Mx2Tran M);

      let v be Element of TRn such that

       A2: v in ( Affin A);

      set vA = (v |-- A);

      set C = ( Carrier vA);

      defpred P[ object, object] means ( not $1 in ( rng MT) implies $2 = 0 ) & ($1 in ( rng MT) implies for f st (MT . f) = $1 holds $2 = (vA . f));

      consider H be FinSequence of the carrier of TRn such that

       A3: H is one-to-one and

       A4: ( rng H) = C and

       A5: ( Sum (vA (#) H)) = ( Sum vA) by RLVECT_2:def 8;

      

       A6: ( Sum vA) = v by A2, RLAFFIN1:def 7;

      reconsider MTR = (MT * H) as FinSequence of TRm;

      

       A7: ( dom MT) = ( [#] TRn) by FUNCT_2:def 1;

      then ( rng H) c= ( dom MT);

      then

       A8: ( len MTR) = ( len H) by FINSEQ_2: 29;

      

       A9: MT is one-to-one by A1, MATRTOP1: 39;

      

       A10: for x be object st x in the carrier of TRm holds ex y be object st y in REAL & P[x, y]

      proof

        let y be object such that y in the carrier of TRm;

        per cases ;

          suppose

           A11: y in ( rng MT);

          then

          consider x be object such that

           A12: x in ( dom MT) and

           A13: (MT . x) = y by FUNCT_1:def 3;

          reconsider x as Element of TRn by A12;

          take (vA . x);

          thus (vA . x) in REAL & ( not y in ( rng MT) implies (vA . x) = 0 ) by A11;

          assume y in ( rng MT);

          let f;

          assume

           A14: (MT . f) = y;

          f is Element of TRn by Lm3;

          hence thesis by A7, A9, A13, A14, FUNCT_1:def 4;

        end;

          suppose

           A15: not y in ( rng MT);

          take x = 0 ;

          thus thesis by A15;

        end;

      end;

      consider F be Function of the carrier of TRm, REAL such that

       A16: for x be object st x in the carrier of TRm holds P[x, (F . x)] from FUNCT_2:sch 1( A10);

      reconsider F as Element of ( Funcs (the carrier of TRm, REAL )) by FUNCT_2: 8;

       A17:

      now

        let w be Element of TRm;

        assume

         A18: not w in (MT .: C);

        assume

         A19: (F . w) <> 0 ;

        then w in ( rng MT) by A16;

        then

        consider f be object such that

         A20: f in ( dom MT) and

         A21: (MT . f) = w by FUNCT_1:def 3;

        reconsider f as Element of TRn by A20;

        (vA . f) = (F . w) by A16, A19, A21;

        then f in C by A19, RLVECT_2: 19;

        hence contradiction by A18, A20, A21, FUNCT_1:def 6;

      end;

      then

      reconsider F as Linear_Combination of TRm by RLVECT_2:def 3;

      

       A22: (MT .: C) c= ( Carrier F)

      proof

        let y be object;

        assume

         A23: y in (MT .: C);

        then

        consider x be object such that

         A24: x in ( dom MT) and

         A25: x in C and

         A26: (MT . x) = y by FUNCT_1:def 6;

        reconsider x as Element of TRn by A24;

        

         A27: (vA . x) <> 0 by A25, RLVECT_2: 19;

        reconsider f = y as Element of TRm by A23;

         P[f, (F . f)] by A16;

        then (F . f) = (vA . x) by A24, A26, FUNCT_1:def 3;

        hence thesis by A27, RLVECT_2: 19;

      end;

      ( Carrier F) c= (MT .: C)

      proof

        let x be object;

        assume

         A28: x in ( Carrier F);

        then

        reconsider w = x as Element of TRm;

        (F . w) <> 0 by A28, RLVECT_2: 19;

        hence thesis by A17;

      end;

      then

       A29: ( Carrier F) = (MT .: C) by A22;

      C c= A by RLVECT_2:def 6;

      then (MT .: C) c= (MT .: A) by RELAT_1: 123;

      then

      reconsider F as Linear_Combination of (MT .: A) by A29, RLVECT_2:def 6;

      set Fm = (F (#) MTR);

      consider fm be sequence of TRm such that

       A30: ( Sum Fm) = (fm . ( len Fm)) and

       A31: (fm . 0 ) = ( 0. TRm) and

       A32: for j be Nat, v be Element of TRm st j < ( len Fm) & v = (Fm . (j + 1)) holds (fm . (j + 1)) = ((fm . j) + v) by RLVECT_1:def 12;

      

       A33: ( rng MTR) = (MT .: C) by A4, RELAT_1: 127;

      ( dom vA) = ( [#] TRn) by FUNCT_2:def 1;

      then

       A34: ( len (vA * H)) = ( len H) by A4, FINSEQ_2: 29;

      set vAH = (vA (#) H);

      consider h be sequence of TRn such that

       A35: ( Sum vAH) = (h . ( len vAH)) and

       A36: (h . 0 ) = ( 0. TRn) and

       A37: for j be Nat, v be Element of TRn st j < ( len vAH) & v = (vAH . (j + 1)) holds (h . (j + 1)) = ((h . j) + v) by RLVECT_1:def 12;

      

       A38: ( len vAH) = ( len H) by RLVECT_2:def 7;

      defpred P[ Nat] means $1 <= ( len Fm) implies (fm . $1) = (MT . (h . $1));

      

       A39: ( len Fm) = ( len MTR) by RLVECT_2:def 7;

      

       A40: (MT .: C) c= ( rng MT) by RELAT_1: 111;

      

       A41: for j be Nat st P[j] holds P[(j + 1)]

      proof

        reconsider TRM = TRm as RealLinearSpace;

        reconsider TRN = TRn as RealLinearSpace;

        let j be Nat;

        reconsider J = j as Element of NAT by ORDINAL1:def 12;

        set j1 = (J + 1);

        assume

         A42: P[j];

        reconsider MTRj1 = (MTR /. j1) as Element of TRM;

        reconsider hj1 = (H /. j1) as n -element real-valued FinSequence;

        reconsider Hj1 = (H /. j1) as Element of TRN;

        assume

         A43: (j + 1) <= ( len Fm);

        

         A44: 1 <= j1 by NAT_1: 11;

        then

         A45: j1 in ( dom MTR) by A39, A43, FINSEQ_3: 25;

        then

         A46: MTRj1 = (MTR . j1) by PARTFUN1:def 6;

        

         A47: (MTR . j1) in (MT .: C) by A33, A45, FUNCT_1:def 3;

        j1 in ( dom H) by A39, A8, A43, A44, FINSEQ_3: 25;

        then

         A48: Hj1 = (H . j1) by PARTFUN1:def 6;

        then (MTR . j1) = (MT . Hj1) by A45, FUNCT_1: 12;

        then

         A49: (F . MTRj1) = (vA . Hj1) by A16, A40, A46, A47;

        

         A50: j1 in ( dom vAH) by A39, A38, A8, A43, A44, FINSEQ_3: 25;

        then (vAH . j1) in ( rng vAH) by FUNCT_1:def 3;

        then

        reconsider vAHj1 = (vAH . j1) as Element of TRn;

        

         A51: j1 in ( dom Fm) by A43, A44, FINSEQ_3: 25;

        then (Fm . j1) in ( rng Fm) by FUNCT_1:def 3;

        then

        reconsider Fmj1 = (Fm . j1) as Element of TRm;

        

         A52: (MT . vAHj1) = (MT . ((vA . Hj1) * Hj1)) by A50, RLVECT_2:def 7

        .= (MT . ((vA . Hj1) * hj1)) by EUCLID: 65

        .= ((vA . Hj1) * (MT . hj1)) by MATRTOP1: 23

        .= ((F . MTRj1) * MTRj1) by A45, A48, A46, A49, EUCLID: 65, FUNCT_1: 12

        .= Fmj1 by A51, RLVECT_2:def 7;

        

         A53: j < ( len Fm) by A43, NAT_1: 13;

        then (h . j1) = ((h . J) + vAHj1) by A37, A39, A38, A8;

        

        hence (MT . (h . (j + 1))) = ((MT . (h . J)) + (MT . vAHj1)) by MATRTOP1: 27

        .= (fm . (j + 1)) by A32, A52, A53, A42;

      end;

      

       A54: P[ 0 ] by A36, A31, MATRTOP1: 29;

      for j be Nat holds P[j] from NAT_1:sch 2( A54, A41);

      then ( Sum Fm) = (MT . ( Sum vAH)) by A35, A30, A39, A38, A8;

      then

       A55: ( Sum F) = (MT . v) by A9, A29, A3, A5, A6, A33, RLVECT_2:def 8;

       A56:

      now

        let i be Nat;

        assume

         A57: 1 <= i & i <= ( len H);

        then

         A58: i in ( dom H) by FINSEQ_3: 25;

        then

         A59: ((vA * H) . i) = (vA . (H . i)) by FUNCT_1: 13;

        (H . i) in ( rng H) by A58, FUNCT_1:def 3;

        then

        reconsider Hi = (H . i) as Element of TRn;

        

         A60: (MTR . i) = (MT . (H . i)) by A58, FUNCT_1: 13;

        

         A61: i in ( dom MTR) by A8, A57, FINSEQ_3: 25;

        then

         A62: (MTR . i) in ( rng MTR) by FUNCT_1:def 3;

        ((F * MTR) . i) = (F . (MTR . i)) by A61, FUNCT_1: 13;

        then P[(MT . Hi), ((F * MTR) . i)] by A16, A60;

        hence ((F * MTR) . i) = ((vA * H) . i) by A33, A40, A59, A60, A62;

      end;

      ( dom F) = ( [#] TRm) by FUNCT_2:def 1;

      then ( len (F * MTR)) = ( len MTR) by A33, FINSEQ_2: 29;

      then (vA * H) = (F * MTR) by A8, A34, A56;

      

      then ( Sum (F * MTR)) = ( sum vA) by A3, A4, RLAFFIN1:def 3

      .= 1 by A2, RLAFFIN1:def 7;

      then

       A63: ( sum F) = 1 by A9, A29, A3, A33, RLAFFIN1:def 3;

      then ( Sum F) in { ( Sum L) where L be Linear_Combination of (MT .: A) : ( sum L) = 1 };

      hence

       A64: (MT . v) in ( Affin (MT .: A)) by A55, RLAFFIN1: 59;

      let f;

      f is Element of TRn by Lm3;

      then

       A65: (MT . f) in ( rng MT) by A7, FUNCT_1:def 3;

      (MT .: A) is affinely-independent by A1, Th24;

      then F = ((MT . v) |-- (MT .: A)) by A55, A63, A64, RLAFFIN1:def 7;

      hence thesis by A16, A65;

    end;

    theorem :: MATRTOP2:26

    

     Th26: for A be linearly-independent Subset of ( TOP-REAL m) st ( the_rank_of M) = n holds (( Mx2Tran M) " A) is linearly-independent

    proof

      let A be linearly-independent Subset of ( TOP-REAL m) such that

       A1: ( the_rank_of M) = n;

      set nV = (n -VectSp_over F_Real ), mV = (m -VectSp_over F_Real );

      reconsider Bm = ( MX2FinS ( 1. ( F_Real ,m))) as OrdBasis of mV by MATRLIN2: 45;

      reconsider A1 = A as Subset of mV by Lm1;

      reconsider Bn = ( MX2FinS ( 1. ( F_Real ,n))) as OrdBasis of nV by MATRLIN2: 45;

      

       A2: ( len Bm) = m by MATRTOP1: 19;

      ( len Bn) = n by MATRTOP1: 19;

      then

      reconsider M1 = M as Matrix of ( len Bn), ( len Bm), F_Real by A2;

      set MT = ( Mx2Tran (M1,Bn,Bm));

      

       A3: ( Mx2Tran M) = MT by MATRTOP1: 20;

      

       A4: MT is one-to-one by A1, A3, MATRTOP1: 39;

      reconsider R = (A /\ ( rng MT)) as Subset of mV;

      

       A5: R c= A by XBOOLE_1: 17;

      A1 is linearly-independent by Th7;

      then

       A6: ( dom MT) = ( [#] nV) & R is linearly-independent by A5, FUNCT_2:def 1, VECTSP_7: 1;

      (MT " R) is linearly-independent

      proof

        assume (MT " R) is non linearly-independent;

        then

        consider L be Linear_Combination of (MT " R) such that

         A7: ( Carrier L) <> {} and

         A8: ( Sum L) = ( 0. nV) by RANKNULL: 41;

        set C = ( Carrier L);

        

         A9: C c= (MT " R) by VECTSP_6:def 4;

        (MT .: (MT " R)) = R & (MT @ L) is Linear_Combination of (MT .: C) by FUNCT_1: 77, RANKNULL: 29, XBOOLE_1: 17;

        then

         A10: (MT @ L) is Linear_Combination of R by A9, RELAT_1: 123, VECTSP_6: 4;

        (MT | C) is one-to-one by A4, FUNCT_1: 52;

        then

         A11: ( Carrier (MT @ L)) = (MT .: C) by RANKNULL: 39;

        (MT | (MT " R)) is one-to-one by A4, FUNCT_1: 52;

        

        then ( Sum (MT @ L)) = (MT . ( Sum L)) by Th14

        .= ( 0. mV) by A8, RANKNULL: 9;

        hence contradiction by A6, A7, A11, A10, VECTSP_7:def 1;

      end;

      then (MT " A) is linearly-independent by RELAT_1: 133;

      hence thesis by A3, Th7;

    end;

    theorem :: MATRTOP2:27

    for A be affinely-independent Subset of ( TOP-REAL m) st ( the_rank_of M) = n holds (( Mx2Tran M) " A) is affinely-independent

    proof

      set MT = ( Mx2Tran M);

      set TRn = ( TOP-REAL n), TRm = ( TOP-REAL m);

      let A be affinely-independent Subset of TRm such that

       A1: ( the_rank_of M) = n;

      reconsider R = (A /\ ( rng MT)) as affinely-independent Subset of TRm by RLAFFIN1: 43, XBOOLE_1: 17;

      

       A2: (MT " A) = (MT " (A /\ ( rng MT))) by RELAT_1: 133;

      per cases ;

        suppose R is empty;

        then (MT " A) is empty by A2;

        hence thesis;

      end;

        suppose R is non empty;

        then

        consider v be Element of TRm such that

         A3: v in R and

         A4: ((( - v) + R) \ {( 0. TRm)}) is linearly-independent by RLAFFIN1:def 4;

        v in ( rng MT) by A3, XBOOLE_0:def 4;

        then

        consider x be object such that

         A5: x in ( dom MT) and

         A6: (MT . x) = v by FUNCT_1:def 3;

        reconsider x as Element of TRn by A5;

        ( - x) = (( 0. TRn) - x) by RLVECT_1: 14;

        

        then

         A7: (MT . ( - x)) = ((MT . ( 0. TRn)) - (MT . x)) by MATRTOP1: 28

        .= (( 0. TRm) - (MT . x)) by MATRTOP1: 29

        .= ( - v) by A6, RLVECT_1: 14;

        

         A8: ( dom MT) = ( [#] TRn) by FUNCT_2:def 1;

        (MT . ( 0. TRn)) = ( 0. TRm) by MATRTOP1: 29;

        

        then

         A9: {( 0. TRm)} = ( Im (MT,( 0. TRn))) by A8, FUNCT_1: 59

        .= (MT .: {( 0. TRn)}) by RELAT_1:def 16;

        MT is one-to-one by A1, MATRTOP1: 39;

        then

         A10: (MT " {( 0. TRm)}) c= {( 0. TRn)} by A9, FUNCT_1: 82;

         {( 0. TRn)} c= ( [#] TRn) by ZFMISC_1: 31;

        then {( 0. TRn)} c= (MT " {( 0. TRm)}) by A8, A9, FUNCT_1: 76;

        then (MT " {( 0. TRm)}) = {( 0. TRn)} by A10;

        

        then (MT " ((( - v) + R) \ {( 0. TRm)})) = ((MT " (( - v) + R)) \ {( 0. TRn)}) by FUNCT_1: 69

        .= ((( - x) + (MT " R)) \ {( 0. TRn)}) by A7, MATRTOP1: 31;

        then

         A11: ((( - x) + (MT " R)) \ {( 0. TRn)}) is linearly-independent by A1, A4, Th26;

        x in (MT " R) by A3, A5, A6, FUNCT_1:def 7;

        hence thesis by A2, A11, RLAFFIN1:def 4;

      end;

    end;