matrtop1.miz



    begin

    reserve X,Y for set,

n,m,k,i for Nat,

r for Real,

R for Element of F_Real ,

K for Field,

f,f1,f2,g1,g2 for FinSequence,

rf,rf1,rf2 for real-valued FinSequence,

cf,cf1,cf2 for complex-valued FinSequence,

F for Function;

    registration

      let X, Y;

      let F be positive-yielding PartFunc of X, REAL ;

      cluster (F | Y) -> positive-yielding;

      coherence

      proof

        let r be Real;

        assume

         A1: r in ( rng (F | Y));

        ( rng (F | Y)) c= ( rng F) by RELAT_1: 70;

        hence thesis by A1, PARTFUN3:def 1;

      end;

    end

    registration

      let X, Y;

      let F be negative-yielding PartFunc of X, REAL ;

      cluster (F | Y) -> negative-yielding;

      coherence

      proof

        let r be Real;

        assume

         A1: r in ( rng (F | Y));

        ( rng (F | Y)) c= ( rng F) by RELAT_1: 70;

        hence thesis by A1, PARTFUN3:def 2;

      end;

    end

    registration

      let X, Y;

      let F be nonpositive-yielding PartFunc of X, REAL ;

      cluster (F | Y) -> nonpositive-yielding;

      coherence

      proof

        let r be Real;

        assume

         A1: r in ( rng (F | Y));

        ( rng (F | Y)) c= ( rng F) by RELAT_1: 70;

        hence thesis by A1, PARTFUN3:def 3;

      end;

    end

    registration

      let X, Y;

      let F be nonnegative-yielding PartFunc of X, REAL ;

      cluster (F | Y) -> nonnegative-yielding;

      coherence

      proof

        let r be Real;

        assume

         A1: r in ( rng (F | Y));

        ( rng (F | Y)) c= ( rng F) by RELAT_1: 70;

        hence thesis by A1, PARTFUN3:def 4;

      end;

    end

    registration

      let rf;

      cluster ( sqrt rf) -> FinSequence-like;

      coherence

      proof

        ( dom rf) = ( dom ( sqrt rf)) & ex n st ( dom rf) = ( Seg n) by FINSEQ_1:def 2, PARTFUN3:def 5;

        hence thesis;

      end;

    end

    definition

      let rf;

      :: MATRTOP1:def1

      func @ rf -> FinSequence of F_Real equals rf;

      coherence

      proof

        ( rng rf) c= REAL ;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let p be FinSequence of F_Real ;

      :: MATRTOP1:def2

      func @ p -> FinSequence of REAL equals p;

      coherence ;

    end

    theorem :: MATRTOP1:1

    (( @ rf1) + ( @ rf2)) = (rf1 + rf2) by RVSUM_1:def 4;

    theorem :: MATRTOP1:2

    

     Th2: ( sqrt (rf1 ^ rf2)) = (( sqrt rf1) ^ ( sqrt rf2))

    proof

      set rf12 = (rf1 ^ rf2);

      set s12 = ( sqrt rf12), s1 = ( sqrt rf1), s2 = ( sqrt rf2);

      

       A1: ( dom s12) = ( dom rf12) by PARTFUN3:def 5;

      

       A2: ( dom s2) = ( dom rf2) by PARTFUN3:def 5;

      then

       A3: ( len s2) = ( len rf2) by FINSEQ_3: 29;

      

       A4: ( dom s1) = ( dom rf1) by PARTFUN3:def 5;

      then

       A5: ( len s1) = ( len rf1) by FINSEQ_3: 29;

      

       A6: 1 <= n & n <= ( len s12) implies (s12 . n) = ((s1 ^ s2) . n)

      proof

        assume 1 <= n & n <= ( len s12);

        then

         A7: n in ( dom s12) by FINSEQ_3: 25;

        then

         A8: (s12 . n) = ( sqrt (rf12 . n)) by PARTFUN3:def 5;

        per cases by A1, A7, FINSEQ_1: 25;

          suppose

           A9: n in ( dom rf1);

          then (rf12 . n) = (rf1 . n) & (s1 . n) = ( sqrt (rf1 . n)) by A4, FINSEQ_1:def 7, PARTFUN3:def 5;

          hence thesis by A4, A8, A9, FINSEQ_1:def 7;

        end;

          suppose ex m st m in ( dom rf2) & n = (( len rf1) + m);

          then

          consider m such that

           A10: m in ( dom rf2) & n = (( len rf1) + m);

          (rf12 . n) = (rf2 . m) & (s2 . m) = ( sqrt (rf2 . m)) by A2, A10, FINSEQ_1:def 7, PARTFUN3:def 5;

          hence thesis by A2, A5, A8, A10, FINSEQ_1:def 7;

        end;

      end;

      ( len s12) = ( len rf12) by A1, FINSEQ_3: 29;

      then ( len s12) = (( len s1) + ( len s2)) by A5, A3, FINSEQ_1: 22;

      then ( len s12) = ( len (s1 ^ s2)) by FINSEQ_1: 22;

      hence thesis by A6;

    end;

    theorem :: MATRTOP1:3

    

     Th3: ( sqrt <*r*>) = <*( sqrt r)*>

    proof

      set R = <*r*>;

      

       A1: (R . 1) = r by FINSEQ_1: 40;

      

       A2: ( dom R) = ( dom ( sqrt R)) by PARTFUN3:def 5;

      then

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

      1 in ( Seg 1) & ( dom R) = ( Seg 1) by FINSEQ_1: 38;

      then ( len R) = 1 & (( sqrt R) . 1) = ( sqrt r) by A2, A1, FINSEQ_1: 40, PARTFUN3:def 5;

      hence thesis by A3, FINSEQ_1: 40;

    end;

    theorem :: MATRTOP1:4

    

     Th4: ( sqrt (rf ^2 )) = ( abs rf)

    proof

      set F = (rf ^2 );

      set S = ( sqrt F);

      

       A1: ( dom S) = ( dom F) by PARTFUN3:def 5;

      

       A2: ( dom ( abs rf)) = ( dom rf) & ( dom F) = ( dom rf) by VALUED_1: 11, VALUED_1:def 11;

      now

        let x be object;

        reconsider fx = (rf . x) as Real;

        

         A3: fx >= 0 or fx < 0 ;

        assume

         A4: x in ( dom ( abs rf));

        then (F . x) = (fx ^2 ) & (S . x) = ( sqrt (F . x)) by A2, A1, PARTFUN3:def 5, VALUED_1: 11;

        then

         A5: (S . x) = fx & fx >= 0 or (S . x) = ( - fx) & fx < 0 by A3, SQUARE_1: 22, SQUARE_1: 23;

        (( abs rf) . x) = |.fx.| by A4, VALUED_1:def 11;

        hence (( abs rf) . x) = (S . x) by A5, ABSVALUE:def 1;

      end;

      hence thesis by A2, A1, FUNCT_1: 2;

    end;

    theorem :: MATRTOP1:5

    

     Th5: rf is nonnegative-yielding implies ( sqrt ( Sum rf)) <= ( Sum ( sqrt rf))

    proof

      defpred P[ Nat] means for f be real-valued FinSequence st ( len f) = $1 & f is nonnegative-yielding holds ( sqrt ( Sum f)) <= ( Sum ( sqrt f)) & 0 <= ( Sum f);

      

       A1: P[n] implies P[(n + 1)]

      proof

        assume

         A2: P[n];

        set n1 = (n + 1);

        let f be real-valued FinSequence such that

         A3: ( len f) = n1 and

         A4: f is nonnegative-yielding;

        ( rng f) c= REAL ;

        then

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

        reconsider fn = (F | n) as FinSequence of REAL ;

        

         A5: F = (fn ^ <*(F . n1)*>) by A3, FINSEQ_3: 55;

        

        then ( sqrt F) = (( sqrt fn) ^ ( sqrt <*(F . n1)*>)) by Th2

        .= (( sqrt fn) ^ <*( sqrt (F . n1))*>) by Th3;

        then

         A6: ( Sum ( sqrt F)) = (( Sum ( sqrt fn)) + ( sqrt (F . n1))) by RVSUM_1: 74;

        

         A7: ( len fn) = n by A3, FINSEQ_3: 53;

        then ( sqrt ( Sum fn)) <= ( Sum ( sqrt fn)) by A2, A4;

        then

         A8: (( sqrt ( Sum fn)) + ( sqrt (f . n1))) <= ( Sum ( sqrt F)) by A6, XREAL_1: 6;

        

         A9: ( Sum f) = (( Sum fn) + (f . n1)) by A5, RVSUM_1: 74;

        n1 >= 1 by NAT_1: 11;

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

        then (f . n1) in ( rng f) by FUNCT_1:def 3;

        then

         A10: (f . n1) >= 0 by A4;

        

         A11: ( Sum fn) >= 0 by A2, A4, A7;

        then ( sqrt ( Sum f)) <= (( sqrt ( Sum fn)) + ( sqrt (f . n1))) by A9, A10, SQUARE_1: 59;

        hence thesis by A9, A11, A10, A8, XXREAL_0: 2;

      end;

      

       A12: P[ 0 qua Nat]

      proof

        let f be real-valued FinSequence such that

         A13: ( len f) = 0 and f is nonnegative-yielding;

        ( dom f) = ( dom ( sqrt f)) by PARTFUN3:def 5;

        then ( len f) = ( len ( sqrt f)) by FINSEQ_3: 29;

        then

         A14: ( sqrt f) = ( <*> REAL ) by A13;

        f = ( <*> REAL ) by A13;

        hence thesis by A14, RVSUM_1: 72, SQUARE_1: 17;

      end;

       P[n] from NAT_1:sch 2( A12, A1);

      then P[( len rf)];

      hence thesis;

    end;

    theorem :: MATRTOP1:6

    ex X st X c= ( dom F) & ( rng F) = ( rng (F | X)) & (F | X) is one-to-one

    proof

      defpred P[ object, object] means (F . $2) = $1;

      

       A1: for x be object st x in ( rng F) holds ex y be object st y in ( dom F) & P[x, y] by FUNCT_1:def 3;

      consider g be Function of ( rng F), ( dom F) such that

       A2: for x be object st x in ( rng F) holds P[x, (g . x)] from FUNCT_2:sch 1( A1);

      take X = ( rng g);

      set FX = (F | X);

      ( dom F) = {} iff ( rng F) = {} by RELAT_1: 42;

      then

       A3: ( dom g) = ( rng F) by FUNCT_2:def 1;

      thus

       A4: X c= ( dom F) by RELAT_1:def 19;

      

       A5: ( rng F) c= ( rng FX)

      proof

        let y be object;

        assume y in ( rng F);

        then (g . y) in X & (F . (g . y)) = y by A2, A3, FUNCT_1:def 3;

        hence thesis by A4, FUNCT_1: 50;

      end;

      ( rng FX) c= ( rng F) by RELAT_1: 70;

      hence ( rng F) = ( rng FX) by A5;

      now

        let x1,x2 be object;

        assume that

         A6: x1 in ( dom FX) and

         A7: x2 in ( dom FX) and

         A8: (FX . x1) = (FX . x2);

        

         A9: (FX . x1) = (F . x1) & (FX . x2) = (F . x2) by A6, A7, FUNCT_1: 47;

        

         A10: ( dom FX) c= X by RELAT_1: 58;

        then

        consider y1 be object such that

         A11: y1 in ( dom g) and

         A12: (g . y1) = x1 by A6, FUNCT_1:def 3;

        consider y2 be object such that

         A13: y2 in ( dom g) & (g . y2) = x2 by A7, A10, FUNCT_1:def 3;

        (F . x1) = y1 by A2, A3, A11, A12;

        hence x1 = x2 by A2, A3, A8, A9, A12, A13;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    registration

      let cf, X;

      cluster (cf - X) -> complex-valued;

      coherence

      proof

        ( rng cf) c= COMPLEX & ( rng (cf - X)) c= ( rng cf) by FINSEQ_3: 66, VALUED_0:def 1;

        then ( rng (cf - X)) c= COMPLEX ;

        hence thesis by VALUED_0:def 1;

      end;

    end

    registration

      let rf, X;

      cluster (rf - X) -> real-valued;

      coherence

      proof

        ( rng (rf - X)) c= ( rng rf) by FINSEQ_3: 66;

        then ( rng (rf - X)) c= REAL by XBOOLE_1: 1;

        hence thesis by VALUED_0:def 3;

      end;

    end

    registration

      let cf be complex-valued FinSubsequence;

      cluster ( Seq cf) -> complex-valued;

      coherence ;

    end

    registration

      let rf be real-valued FinSubsequence;

      cluster ( Seq rf) -> real-valued;

      coherence ;

    end

    theorem :: MATRTOP1:7

    

     Th7: for P be Permutation of ( dom f) st f1 = (f * P) holds ex Q be Permutation of ( dom (f - X)) st (f1 - X) = ((f - X) * Q)

    proof

      let P be Permutation of ( dom f) such that

       A1: f1 = (f * P);

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

      

       A2: ( rng P) = ( dom f) by FUNCT_2:def 3;

      then

       A3: ( dom (p " )) = ( dom f) by FUNCT_1: 33;

      

       A4: (P .: (f1 " X)) = (P .: (P " (f " X))) by A1, RELAT_1: 146

      .= (f " X) by A2, FUNCT_1: 77, RELAT_1: 132;

      

       A5: ( dom P) = ( dom f) by FUNCT_2: 52;

      then

       A6: ( dom f1) = ( dom f) by A1, A2, RELAT_1: 27;

      set DfX = (( dom f1) \ (f1 " X));

      set DX = (( dom f) \ (f " X));

      

       A7: ( card DX) = (( card ( dom f)) - ( card (f " X))) by CARD_2: 44, RELAT_1: 132;

      

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

      then

       A9: ( dom ( Sgm DX)) = ( Seg ( card DX)) by FINSEQ_3: 40, XBOOLE_1: 36;

      

       A10: (p " (f " X)) = ((p " ) .: (f " X)) by FUNCT_1: 85;

      (f1 " X) = (P " (f " X)) by A1, RELAT_1: 146;

      then

       A11: ((f " X),(f1 " X)) are_equipotent by A3, A10, CARD_1: 33, RELAT_1: 132;

      

       A12: DfX c= ( dom f1) by XBOOLE_1: 36;

      

       A13: ( rng (P * ( Sgm DfX))) = (P .: ( rng ( Sgm DfX))) by RELAT_1: 127

      .= (P .: DfX) by A6, A8, A12, FINSEQ_1:def 13

      .= ((P .: ( dom P)) \ (P .: (f1 " X))) by A5, A6, FUNCT_1: 64

      .= DX by A4, A2, RELAT_1: 113;

      reconsider SDX = ( Sgm DX) as one-to-one Function by A8, FINSEQ_3: 92, XBOOLE_1: 36;

      

       A14: ( dom (SDX " )) = ( rng SDX) by FUNCT_1: 33;

      ( card ( dom f)) = ( len f) by CARD_1: 62;

      then

       A15: ( dom (f - X)) = ( dom SDX) by A7, A9, FINSEQ_3: 62;

      ( card DfX) = (( card ( dom f1)) - ( card (f1 " X))) by CARD_2: 44, RELAT_1: 132;

      then ( card DX) = ( card DfX) by A11, A6, A7, CARD_1: 5;

      then

       A16: ( dom SDX) = ( dom ( Sgm DfX)) by A6, A8, A9, FINSEQ_3: 40, XBOOLE_1: 36;

      DX c= ( dom f) by XBOOLE_1: 36;

      then

       A17: ( rng ( Sgm DX)) = DX by A8, FINSEQ_1:def 13;

      ( rng (SDX " )) = ( dom SDX) by FUNCT_1: 33;

      then

       A18: ( rng ((SDX " ) * (P * ( Sgm DfX)))) = ( dom SDX) by A17, A14, A13, RELAT_1: 28;

      ( rng ( Sgm DfX)) = DfX by A6, A8, A12, FINSEQ_1:def 13;

      then ( dom (P * ( Sgm DfX))) = ( dom ( Sgm DfX)) by A5, A6, RELAT_1: 27, XBOOLE_1: 36;

      then ( dom ((SDX " ) * (P * ( Sgm DfX)))) = ( dom ( Sgm DfX)) by A17, A14, A13, RELAT_1: 27;

      then

      reconsider Q = ((SDX " ) * (P * ( Sgm DfX))) as Function of ( dom (f - X)), ( dom (f - X)) by A18, A15, A16, FUNCT_2: 1;

      

       A19: Q is onto by A18, A15, FUNCT_2:def 3;

      ( Sgm DfX) is one-to-one by A6, A8, FINSEQ_3: 92, XBOOLE_1: 36;

      then

      reconsider Q as Permutation of ( dom (f - X)) by A19;

      (SDX * (SDX " )) = ( id DX) by A17, FUNCT_1: 39;

      

      then

       A20: (SDX * Q) = (( id DX) * (P * ( Sgm DfX))) by RELAT_1: 36

      .= (P * ( Sgm DfX)) by A13, RELAT_1: 53;

      ((f - X) * Q) = ((f * SDX) * Q) by FINSEQ_3:def 1

      .= (f * (P * ( Sgm DfX))) by A20, RELAT_1: 36

      .= (f1 * ( Sgm DfX)) by A1, RELAT_1: 36

      .= (f1 - X) by FINSEQ_3:def 1;

      hence thesis;

    end;

    theorem :: MATRTOP1:8

    for P be Permutation of ( dom cf) st cf1 = (cf * P) holds ( Sum (cf1 - X)) = ( Sum (cf - X))

    proof

      ( rng (cf1 - X)) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider fPX = (cf1 - X) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      ( rng (cf - X)) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider fX = (cf - X) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      let P be Permutation of ( dom cf) such that

       A1: cf1 = (cf * P);

      consider Q be Permutation of ( dom (cf - X)) such that

       A2: (cf1 - X) = ((cf - X) * Q) by A1, Th7;

      

      thus ( Sum (cf1 - X)) = ( addcomplex "**" fPX) by RVSUM_1:def 11

      .= ( addcomplex "**" fX) by A2, FINSOP_1: 7

      .= ( Sum (cf - X)) by RVSUM_1:def 11;

    end;

    theorem :: MATRTOP1:9

    

     Th9: for f,f1 be FinSubsequence holds for P be Permutation of ( dom f) st f1 = (f * P) holds ex Q be Permutation of ( dom ( Seq (f1 | (P " X)))) st ( Seq (f | X)) = (( Seq (f1 | (P " X))) * Q)

    proof

      let f,f1 be FinSubsequence;

      consider n be Nat such that

       A1: ( dom f) c= ( Seg n) by FINSEQ_1:def 12;

      let P be Permutation of ( dom f) such that

       A2: f1 = (f * P);

      set SPX = ( Sgm (P " X));

      

       A3: (P " X) c= ( dom P) by RELAT_1: 132;

      then

       A4: ( dom (P | (P " X))) = (P " X) by RELAT_1: 62;

      

       A5: ( dom P) = ( dom f) by FUNCT_2: 52;

      then

       A6: SPX is one-to-one by A1, A3, FINSEQ_3: 92, XBOOLE_1: 1;

      set dfX = (( dom f) /\ X);

      set SdX = ( Sgm dfX);

      

       A7: dfX c= ( dom f) by XBOOLE_1: 17;

      then dfX c= ( Seg n) by A1;

      then

       A8: ( rng SdX) = dfX by FINSEQ_1:def 13;

      

       A9: ( rng P) = ( dom f) by FUNCT_2:def 3;

      then

       A10: (P " X) = (P " dfX) by RELAT_1: 133;

      then

       A11: (P " X) = ((P " ) .: dfX) by FUNCT_1: 85;

      set PS = ((P | (P " X)) * SPX);

      

       A12: (P | (P " X)) is one-to-one by FUNCT_1: 52;

      (P " X) c= ( Seg n) by A1, A5, A3;

      then

       A13: ( rng SPX) = (P " X) by FINSEQ_1:def 13;

      ( rng (P | (P " X))) = (P .: (P " dfX)) by A10, RELAT_1: 115

      .= dfX by A9, FUNCT_1: 77, XBOOLE_1: 17;

      then

       A14: ( rng PS) = dfX by A4, A13, RELAT_1: 28;

      

       A15: ( dom (PS qua Function " )) = dfX by A6, A12, A14, FUNCT_1: 33;

      ( dom (P " )) = ( rng P) by FUNCT_1: 33;

      then (dfX,((P " ) .: dfX)) are_equipotent by A9, CARD_1: 33, XBOOLE_1: 17;

      then ( card dfX) = ( card (P " X)) by A11, CARD_1: 5;

      then

       A16: ( dom SPX) = ( Seg ( card dfX)) by A1, A5, A3, FINSEQ_3: 40, XBOOLE_1: 1;

      then ( dom PS) = ( Seg ( card dfX)) by A4, A13, RELAT_1: 27;

      then ( rng (PS qua Function " )) = ( Seg ( card dfX)) by A6, A12, FUNCT_1: 33;

      then

       A17: ( rng ((PS qua Function " ) * SdX)) = ( Seg ( card dfX)) by A15, A8, RELAT_1: 28;

      ( dom f1) = ( dom P) by A2, A9, RELAT_1: 27;

      then

       A18: ( dom (f1 | (P " X))) = (P " X) by RELAT_1: 62, RELAT_1: 132;

      then

       A19: ( dom ( Seq (f1 | (P " X)))) = ( Seg ( card dfX)) by A16, A13, RELAT_1: 27;

      ( dom SdX) = ( Seg ( card dfX)) by A1, A7, FINSEQ_3: 40, XBOOLE_1: 1;

      then ( dom ((PS qua Function " ) * SdX)) = ( Seg ( card dfX)) by A15, A8, RELAT_1: 27;

      then

      reconsider PSS = ((PS qua Function " ) * SdX) as Function of ( dom ( Seq (f1 | (P " X)))), ( dom ( Seq (f1 | (P " X)))) by A19, A17, FUNCT_2: 1;

      

       A20: PSS is onto by A19, A17, FUNCT_2:def 3;

      SdX is one-to-one by A1, A7, FINSEQ_3: 92, XBOOLE_1: 1;

      then

      reconsider PSS as Permutation of ( dom ( Seq (f1 | (P " X)))) by A6, A12, A20;

      

       A21: (PS * PSS) = ((PS * (PS qua Function " )) * SdX) by RELAT_1: 36

      .= (( id dfX) * SdX) by A6, A12, A14, FUNCT_1: 39;

      set fX = (f | X);

      

       A22: fX = (f | dfX) by RELAT_1: 157;

      take PSS;

      (f1 | (P " X)) = (f * (P | (P " X))) by A2, RELAT_1: 83;

      

      hence (( Seq (f1 | (P " X))) * PSS) = ((f * PS) * PSS) by A18, RELAT_1: 36

      .= (f * (( id dfX) * SdX)) by A21, RELAT_1: 36

      .= ((f * ( id dfX)) * SdX) by RELAT_1: 36

      .= (fX * SdX) by A22, RELAT_1: 65

      .= ( Seq fX) by RELAT_1: 61;

    end;

    theorem :: MATRTOP1:10

    for cf,cf1 be complex-valued FinSubsequence holds for P be Permutation of ( dom cf) st cf1 = (cf * P) holds ( Sum ( Seq (cf | X))) = ( Sum ( Seq (cf1 | (P " X))))

    proof

      let cf,cf1 be complex-valued FinSubsequence;

      ( rng ( Seq (cf | X))) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider SfX = ( Seq (cf | X)) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      let P be Permutation of ( dom cf) such that

       A1: cf1 = (cf * P);

      consider Q be Permutation of ( dom ( Seq (cf1 | (P " X)))) such that

       A2: ( Seq (cf | X)) = (( Seq (cf1 | (P " X))) * Q) by A1, Th9;

      ( rng ( Seq (cf1 | (P " X)))) c= COMPLEX by VALUED_0:def 1;

      then

      reconsider SfPX = ( Seq (cf1 | (P " X))) as FinSequence of COMPLEX by FINSEQ_1:def 4;

      

      thus ( Sum ( Seq (cf1 | (P " X)))) = ( addcomplex "**" SfPX) by RVSUM_1:def 11

      .= ( addcomplex "**" SfX) by A2, FINSOP_1: 7

      .= ( Sum ( Seq (cf | X))) by RVSUM_1:def 11;

    end;

    theorem :: MATRTOP1:11

    

     Th11: for f be FinSubsequence holds for n be Element of NAT st for i holds (i + n) in X iff i in Y holds ((n Shift f) | X) = (n Shift (f | Y))

    proof

      let f be FinSubsequence;

      let n be Element of NAT such that

       A1: (i + n) in X iff i in Y;

      set fY = (f | Y);

      set nf = (n Shift f);

      set nfX = (nf | X);

      set nfY = (n Shift fY);

      

       A2: ( dom nfY) = { (k + n) where k be Nat : k in ( dom fY) } by VALUED_1:def 12;

       A3:

      now

        let x be object;

        assume x in ( dom nfY);

        then

        consider k be Nat such that

         A4: x = (k + n) and

         A5: k in ( dom fY) by A2;

        

         A6: k in ( dom f) by A5, RELAT_1: 57;

        

         A7: k in Y by A5, RELAT_1: 57;

        then x in X by A1, A4;

        

        hence (nfX . x) = (nf . x) by FUNCT_1: 49

        .= (f . k) by A4, A6, VALUED_1:def 12

        .= (fY . k) by A7, FUNCT_1: 49

        .= (nfY . x) by A4, A5, VALUED_1:def 12;

      end;

      

       A8: ( dom nf) = { (k + n) where k be Nat : k in ( dom f) } by VALUED_1:def 12;

      

       A9: ( dom nfY) c= ( dom nfX)

      proof

        let x be object;

        assume x in ( dom nfY);

        then

        consider k be Nat such that

         A10: x = (k + n) and

         A11: k in ( dom fY) by A2;

        k in Y by A11, RELAT_1: 57;

        then

         A12: x in X by A1, A10;

        k in ( dom f) by A11, RELAT_1: 57;

        then x in ( dom nf) by A8, A10;

        hence thesis by A12, RELAT_1: 57;

      end;

      ( dom nfX) c= ( dom nfY)

      proof

        let x be object;

        assume

         A13: x in ( dom nfX);

        then x in ( dom nf) by RELAT_1: 57;

        then

        consider k be Nat such that

         A14: x = (k + n) and

         A15: k in ( dom f) by A8;

        x in X by A13, RELAT_1: 57;

        then k in Y by A1, A14;

        then k in ( dom fY) by A15, RELAT_1: 57;

        hence thesis by A2, A14;

      end;

      then ( dom nfY) = ( dom nfX) by A9;

      hence thesis by A3, FUNCT_1: 2;

    end;

    theorem :: MATRTOP1:12

    

     Th12: ex Y be Subset of NAT st ( Seq ((f1 ^ f2) | X)) = (( Seq (f1 | X)) ^ ( Seq (f2 | Y))) & for n st n > 0 holds n in Y iff (n + ( len f1)) in (X /\ ( dom (f1 ^ f2)))

    proof

      set f12 = (f1 ^ f2);

      set n1 = ( len f1), n2 = ( len f2);

      set X12 = (X /\ ( dom f12));

      set X1 = (X12 /\ ( Seg n1)), X2 = (X12 \ ( Seg n1));

      set Y2 = { i where i be Element of NAT : (i + n1) in X2 };

      Y2 c= NAT

      proof

        let x be object;

        assume x in Y2;

        then ex i be Element of NAT st i = x & (i + n1) in X2;

        hence thesis;

      end;

      then

      reconsider Y2 as Subset of NAT ;

      set Sf2 = (n1 Shift f2);

      

       A1: f12 = (f1 \/ Sf2) by VALUED_1: 49;

      take Y2;

      

       A2: (X12 /\ ( dom Sf2)) c= X2

      proof

        let x be object;

        assume

         A3: x in (X12 /\ ( dom Sf2));

        then x in ( dom Sf2) by XBOOLE_0:def 4;

        then x in { (k + n1) where k be Nat : k in ( dom f2) } by VALUED_1:def 12;

        then

        consider k be Nat such that

         A4: x = (k + n1) and

         A5: k in ( dom f2);

        1 <= k by A5, FINSEQ_3: 25;

        then (1 + n1) <= (k + n1) by XREAL_1: 6;

        then n1 < (k + n1) by NAT_1: 13;

        then

         A6: not x in ( Seg n1) by A4, FINSEQ_1: 1;

        x in X12 by A3, XBOOLE_0:def 4;

        hence thesis by A6, XBOOLE_0:def 5;

      end;

       A7:

      now

        let i;

        thus (i + n1) in X2 implies i in Y2

        proof

          assume

           A8: (i + n1) in X2;

          i in NAT by ORDINAL1:def 12;

          hence thesis by A8;

        end;

        assume i in Y2;

        then ex j be Element of NAT st i = j & (j + n1) in X2;

        hence (i + n1) in X2;

      end;

      (f1 | X1) c= f1 & (f2 | Y2) c= f2 by RELAT_1: 59;

      then

      consider ss be FinSubsequence such that

       A9: ss = ((f1 | X1) \/ (n1 Shift (f2 | Y2))) & (( Seq (f1 | X1)) ^ ( Seq (f2 | Y2))) = ( Seq ss) by VALUED_1: 64;

      

       A10: ( dom f1) = ( Seg n1) by FINSEQ_1:def 3;

      then (( dom f12) /\ ( Seg n1)) = ( Seg n1) by FINSEQ_1: 26, XBOOLE_1: 28;

      

      then

       A11: (f1 | X) = (f1 | (X /\ (( dom f12) /\ ( Seg n1)))) by A10, RELAT_1: 157

      .= (f1 | X1) by XBOOLE_1: 16;

      X2 c= (X12 /\ ( dom Sf2))

      proof

        let x be object;

        assume

         A12: x in X2;

        then

         A13: not x in ( Seg n1) by XBOOLE_0:def 5;

        

         A14: x in X12 by A12, XBOOLE_0:def 5;

        then x in ( dom f12) by XBOOLE_0:def 4;

        then

        consider k be Nat such that

         A15: k in ( dom f2) & x = (n1 + k) by A10, A13, FINSEQ_1: 25;

        x in { (i + n1) where i be Nat : i in ( dom f2) } by A15;

        then x in ( dom Sf2) by VALUED_1:def 12;

        hence thesis by A14, XBOOLE_0:def 4;

      end;

      then

       A16: X2 = (X12 /\ ( dom Sf2)) by A2;

      (f12 | X) = (f12 | X12) by RELAT_1: 157;

      

      then (f12 | X) = (f12 * ( id X12)) by RELAT_1: 65

      .= ((f1 * ( id X12)) \/ (Sf2 * ( id X12))) by A1, RELAT_1: 32

      .= ((f1 | X12) \/ (Sf2 * ( id X12))) by RELAT_1: 65

      .= ((f1 | X12) \/ (Sf2 | X12)) by RELAT_1: 65

      .= ((f1 | X12) \/ (Sf2 | X2)) by A16, RELAT_1: 157

      .= ((f1 | X1) \/ (Sf2 | X2)) by A10, RELAT_1: 157;

      hence ( Seq ((f1 ^ f2) | X)) = (( Seq (f1 | X)) ^ ( Seq (f2 | Y2))) by A7, A11, A9, Th11;

      let n;

      assume n > 0 ;

      then (n + n1) > ( 0 qua Nat + n1) by XREAL_1: 6;

      then

       A17: not (n + n1) in ( Seg n1) by FINSEQ_1: 1;

      hereby

        assume n in Y2;

        then (n + n1) in X2 by A7;

        hence (n + n1) in X12 by XBOOLE_0:def 5;

      end;

      assume (n + n1) in X12;

      then (n + n1) in X2 by A17, XBOOLE_0:def 5;

      hence n in Y2 by A7;

    end;

    theorem :: MATRTOP1:13

    ( len g1) = ( len f1) & ( len g2) <= ( len f2) implies ( Seq ((f1 ^ f2) | ((g1 ^ g2) " X))) = (( Seq (f1 | (g1 " X))) ^ ( Seq (f2 | (g2 " X))))

    proof

      assume that

       A1: ( len f1) = ( len g1) and

       A2: ( len g2) <= ( len f2);

      set f12 = (f1 ^ f2), g12 = (g1 ^ g2);

      

       A3: ( dom f12) = ( Seg ( len f12)) & ( dom g12) = ( Seg ( len g12)) by FINSEQ_1:def 3;

      set g12X = (g12 " X);

      consider Y be Subset of NAT such that

       A4: ( Seq (f12 | g12X)) = (( Seq (f1 | g12X)) ^ ( Seq (f2 | Y))) and

       A5: for n st n > 0 holds n in Y iff (n + ( len f1)) in (g12X /\ ( dom f12)) by Th12;

      

       A6: (Y /\ ( dom f2)) c= (g2 " X)

      proof

        let x be object;

        assume

         A7: x in (Y /\ ( dom f2));

        then

        reconsider i = x as Nat;

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

        then

         A8: i > 0 by FINSEQ_3: 25;

        then (i + ( len f1)) > (( len f1) + 0 qua Nat) by XREAL_1: 6;

        then

         A9: not (i + ( len f1)) in ( dom g1) by A1, FINSEQ_3: 25;

        x in Y by A7, XBOOLE_0:def 4;

        then (i + ( len f1)) in (g12X /\ ( dom f12)) by A5, A8;

        then

         A10: (i + ( len f1)) in g12X by XBOOLE_0:def 4;

        then

         A11: (g12 . (i + ( len f1))) in X by FUNCT_1:def 7;

        (i + ( len f1)) in ( dom g12) by A10, FUNCT_1:def 7;

        then

         A12: ex j be Nat st j in ( dom g2) & (i + ( len f1)) = (( len g1) + j) by A9, FINSEQ_1: 25;

        then (g12 . (i + ( len f1))) = (g2 . i) by A1, FINSEQ_1:def 7;

        hence thesis by A1, A11, A12, FUNCT_1:def 7;

      end;

      

       A13: ( dom f1) = ( dom g1) by A1, FINSEQ_3: 29;

      

       A14: (g1 " X) c= (g12X /\ ( dom f1))

      proof

        let x be object;

        assume

         A15: x in (g1 " X);

        then

         A16: x in ( dom g1) by FUNCT_1:def 7;

        

         A17: (g1 . x) in X by A15, FUNCT_1:def 7;

        ( dom g1) c= ( dom g12) & (g12 . x) = (g1 . x) by A16, FINSEQ_1: 26, FINSEQ_1:def 7;

        then x in g12X by A16, A17, FUNCT_1:def 7;

        hence thesis by A13, A16, XBOOLE_0:def 4;

      end;

      ( len f12) = (( len f1) + ( len f2)) & ( len g12) = (( len g1) + ( len g2)) by FINSEQ_1: 22;

      then ( len g12) <= ( len f12) by A1, A2, XREAL_1: 6;

      then

       A18: ( dom g12) c= ( dom f12) by A3, FINSEQ_1: 5;

      (g12X /\ ( dom f1)) c= (g1 " X)

      proof

        let x be object;

        assume

         A19: x in (g12X /\ ( dom f1));

        then x in g12X by XBOOLE_0:def 4;

        then

         A20: (g12 . x) in X by FUNCT_1:def 7;

        

         A21: x in ( dom f1) by A19, XBOOLE_0:def 4;

        then (g12 . x) = (g1 . x) by A13, FINSEQ_1:def 7;

        hence thesis by A13, A21, A20, FUNCT_1:def 7;

      end;

      then (g12X /\ ( dom f1)) = (g1 " X) by A14;

      then

       A22: (f1 | (g1 " X)) = (f1 | g12X) by RELAT_1: 157;

      ( dom f2) = ( Seg ( len f2)) & ( dom g2) = ( Seg ( len g2)) by FINSEQ_1:def 3;

      then

       A23: ( dom g2) c= ( dom f2) by A2, FINSEQ_1: 5;

      (g2 " X) c= (Y /\ ( dom f2))

      proof

        let x be object;

        assume

         A24: x in (g2 " X);

        then

         A25: x in ( dom g2) by FUNCT_1:def 7;

        then

        reconsider i = x as Nat;

        

         A26: (g2 . x) in X by A24, FUNCT_1:def 7;

        

         A27: (i + ( len g1)) in ( dom g12) by A25, FINSEQ_1: 28;

        (g12 . (i + ( len g1))) = (g2 . i) by A25, FINSEQ_1:def 7;

        then (i + ( len g1)) in g12X by A26, A27, FUNCT_1:def 7;

        then

         A28: (i + ( len g1)) in (g12X /\ ( dom f12)) by A18, A27, XBOOLE_0:def 4;

        i > 0 by A25, FINSEQ_3: 25;

        then i in Y by A1, A5, A28;

        hence thesis by A23, A25, XBOOLE_0:def 4;

      end;

      then (Y /\ ( dom f2)) = (g2 " X) by A6;

      hence thesis by A4, A22, RELAT_1: 157;

    end;

    theorem :: MATRTOP1:14

    for D be non empty set holds for M be Matrix of n, m, D holds (M - X) is Matrix of (n -' ( card (M " X))), m, D

    proof

      let D be non empty set;

      let M be Matrix of n, m, D;

      

       A1: ( rng (M - X)) c= ( rng M) by FINSEQ_3: 66;

      ( rng M) c= (D * ) by FINSEQ_1:def 4;

      then ( rng (M - X)) c= (D * ) by A1;

      then

      reconsider MX = (M - X) as FinSequence of (D * ) by FINSEQ_1:def 4;

      

       A2: ( len MX) = (( len M) - ( card (M " X))) by FINSEQ_3: 59;

      then ( len M) >= ( card (M " X)) by XREAL_1: 49;

      then

       A3: ( len M) = n & ( len MX) = (( len M) -' ( card (M " X))) by A2, MATRIX_0:def 2, XREAL_1: 233;

      per cases ;

        suppose ( len MX) = 0 ;

        then MX = {} ;

        hence thesis by A3, MATRIX_0: 13;

      end;

        suppose ( len MX) > 0 ;

        

         A4: for x be object st x in ( rng MX) holds ex s be FinSequence st s = x & ( len s) = m

        proof

          let x be object;

          consider nn be Nat such that

           A5: for x be object st x in ( rng M) holds ex p be FinSequence of D st x = p & ( len p) = nn by MATRIX_0: 9;

          assume

           A6: x in ( rng MX);

          then ex p be FinSequence of D st x = p & ( len p) = nn by A1, A5;

          then

          reconsider p = x as FinSequence of D;

          ( len p) = m by A1, A6, MATRIX_0:def 2;

          hence thesis;

        end;

        then

        reconsider MX as Matrix of D by MATRIX_0:def 1;

        now

          let p be FinSequence of D;

          assume p in ( rng MX);

          then ex s be FinSequence st s = p & ( len s) = m by A4;

          hence ( len p) = m;

        end;

        hence thesis by A3, MATRIX_0:def 2;

      end;

    end;

    theorem :: MATRTOP1:15

    

     Th15: for F be Function of ( Seg n), ( Seg n), D be non empty set holds for M be Matrix of n, m, D holds for i st i in ( Seg ( width M)) holds ( Col ((M * F),i)) = (( Col (M,i)) * F)

    proof

      let F be Function of ( Seg n), ( Seg n), D be non empty set;

      let M be Matrix of n, m, D;

      let i;

      assume

       A1: i in ( Seg ( width M));

      

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

      then

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

      ( len ( Col (M,i))) = n by A2, CARD_1:def 7;

      then

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

      ( dom F) = ( Seg n) & ( rng F) c= ( Seg n) by FUNCT_2: 52, RELAT_1:def 19;

      then

       A5: ( dom (( Col (M,i)) * F)) = ( Seg n) by A4, RELAT_1: 27;

      

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

      then

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

       A8:

      now

        let x be object;

        assume

         A9: x in ( Seg n);

        then

        reconsider j = x as Element of NAT ;

        ( Indices M) = [:( dom M), ( Seg ( width M)):] by MATRIX_0:def 4;

        then

         A10: [j, i] in ( Indices M) by A1, A3, A9, ZFMISC_1: 87;

        

         A11: (F . x) in ( Seg n) by A4, A5, A9, FUNCT_1: 11;

        then

        reconsider Fj = (F . x) as Element of NAT ;

        

        thus ((( Col (M,i)) * F) . x) = (( Col (M,i)) . Fj) by A5, A9, FUNCT_1: 12

        .= (M * (Fj,i)) by A3, A11, MATRIX_0:def 8

        .= ((M * F) * (j,i)) by A10, MATRIX11:def 4

        .= (( Col ((M * F),i)) . x) by A7, A9, MATRIX_0:def 8;

      end;

      ( len ( Col ((M * F),i))) = n by A6, CARD_1:def 7;

      then ( dom ( Col ((M * F),i))) = ( Seg n) by FINSEQ_1:def 3;

      hence thesis by A5, A8, FUNCT_1: 2;

    end;

    

     Lm1: for A be Matrix of n, m, K st (n = 0 implies m = 0 ) & ( the_rank_of A) = n holds ex B be Matrix of (m -' n), m, K st ( the_rank_of (A ^ B)) = m

    proof

      let A be Matrix of n, m, K;

      set V = (m -VectSp_over K), L = ( lines A);

      assume that

       A1: n = 0 implies m = 0 and

       A2: ( the_rank_of A) = n;

      

       A3: ( len A) = n by A1, MATRIX13: 1;

      L is linearly-independent by A2, MATRIX13: 121;

      then

      consider B be Subset of V such that

       A4: L c= B and

       a5: B is base by VECTSP_7: 17;

      

       A5: B is linearly-independent by a5, VECTSP_7:def 3;

      

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

      reconsider B as finite Subset of V by A5, VECTSP_9: 21;

      B is Basis of V by A5, A6, VECTSP_7:def 3;

      

      then

       A7: ( card B) = ( dim V) by VECTSP_9:def 1

      .= m by MATRIX13: 112;

      ( width A) = m by A1, MATRIX13: 1;

      then

       A8: (m - n) >= 0 by A2, MATRIX13: 74, XREAL_1: 48;

      then

       A9: (m - n) = (m -' n) by XREAL_0:def 2;

      

       A10: A is without_repeated_line by A2, MATRIX13: 121;

      then

       A11: ( len A) = ( card L) by FINSEQ_4: 62;

      set BL = (B \ L);

      consider p be FinSequence such that

       A12: ( rng p) = BL and

       A13: p is one-to-one by FINSEQ_4: 58;

      reconsider p as FinSequence of V by A12, FINSEQ_1:def 4;

      ( len p) = ( card BL) by A12, A13, FINSEQ_4: 62

      .= (( card B) - ( card L)) by A4, CARD_2: 44

      .= (m -' n) by A3, A11, A7, A8, XREAL_0:def 2;

      then

      reconsider P = ( FinS2MX p) as Matrix of (m -' n), m, K;

      ( rng A) misses ( rng P) by A12, XBOOLE_1: 79;

      then

       A14: (A ^ P) is without_repeated_line by A10, A13, FINSEQ_3: 91;

      take P;

      ( lines (A ^ P)) = (L \/ ( rng P)) by FINSEQ_1: 31

      .= (L \/ B) by A12, XBOOLE_1: 39

      .= B by A4, XBOOLE_1: 12;

      hence thesis by A5, A9, A14, MATRIX13: 121;

    end;

    theorem :: MATRTOP1:16

    

     Th16: for A be Matrix of n, m, K st ( the_rank_of A) = n holds ex B be Matrix of (m -' n), m, K st ( the_rank_of (A ^ B)) = m

    proof

      let A be Matrix of n, m, K such that

       A1: ( the_rank_of A) = n;

      per cases ;

        suppose

         A2: n = 0 ;

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

        then

        reconsider ONE = ( 1. (K,m)) as Matrix of (m -' n), m, K by A2;

        ( Det ( 1. (K,m))) <> ( 0. K) by LAPLACE: 34;

        then

         A3: ( the_rank_of ONE) = m by MATRIX13: 83;

        ( len A) = 0 by A2, MATRIX_0:def 2;

        then A is empty;

        then (A ^ ONE) = ONE by FINSEQ_1: 34;

        hence thesis by A3;

      end;

        suppose n > 0 ;

        hence thesis by A1, Lm1;

      end;

    end;

    theorem :: MATRTOP1:17

    for A be Matrix of n, m, K st ( the_rank_of A) = m holds ex B be Matrix of n, (n -' m), K st ( the_rank_of (A ^^ B)) = n

    proof

      let A be Matrix of n, m, K such that

       A1: ( the_rank_of A) = m;

      

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

      per cases ;

        suppose

         A3: m = 0 ;

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

        then

        reconsider ONE = ( 1. (K,n)) as Matrix of n, (n -' m), K by A3;

        

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

        ( Det ( 1. (K,n))) <> ( 0. K) by LAPLACE: 34;

        then

         A5: ( the_rank_of ONE) = n by MATRIX13: 83;

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

        then (A ^^ ONE) = ONE by A2, A3, A4, MATRIX15: 22;

        hence thesis by A5;

      end;

        suppose

         A6: m > 0 ;

        (n - m) >= 0 by A1, A2, MATRIX13: 74, XREAL_1: 48;

        then

         A7: (n -' m) = (n - m) by XREAL_0:def 2;

        

         A8: n > 0 by A1, A2, A6, MATRIX13: 74;

        then

         A9: ( width A) = m by MATRIX13: 1;

        per cases ;

          suppose

           A10: n = m;

          take B = the Matrix of n, (n -' m), K;

          ( len B) = n & ( width B) = 0 by A6, A7, A10, MATRIX_0: 23;

          hence thesis by A1, A2, A10, MATRIX15: 22;

        end;

          suppose

           A11: n <> m;

          

           A12: ( width (A @ )) = n by A2, A6, A9, MATRIX_0: 54;

          ( len (A @ )) = m by A6, A9, MATRIX_0: 54;

          then

          reconsider A1 = (A @ ) as Matrix of m, n, K by A12, MATRIX_0: 51;

          ( the_rank_of A1) = m by A1, MATRIX13: 84;

          then

          consider B be Matrix of (n -' m), n, K such that

           A13: ( the_rank_of (A1 ^ B)) = n by Th16;

          

           A14: (n -' m) <> 0 by A7, A11;

          then

           A15: ( width B) = n by MATRIX13: 1;

          then

           A16: ( len (B @ )) = n by A8, MATRIX_0: 54;

          ( len B) = (n -' m) by A14, MATRIX13: 1;

          then ( width (B @ )) = (n -' m) by A8, A15, MATRIX_0: 54;

          then

          reconsider B1 = (B @ ) as Matrix of n, (n -' m), K by A16, MATRIX_0: 51;

          (A1 @ ) = A by A2, A6, A8, A9, MATRIX_0: 57;

          then

           A17: ((A1 ^ B) @ ) = (A ^^ B1) by A12, A15, MATRLIN: 28;

          ( the_rank_of ((A1 ^ B) @ )) = n by A13, MATRIX13: 84;

          hence thesis by A17;

        end;

      end;

    end;

    reserve f,f1,f2 for n -element real-valued FinSequence,

p,p1,p2 for Point of ( TOP-REAL n),

M,M1,M2 for Matrix of n, m, F_Real ,

A,B for Matrix of n, F_Real ;

    

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

    proof

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

      hence thesis by TOPREAL3: 46;

    end;

    begin

    definition

      let n, m, M;

      :: MATRTOP1:def3

      func Mx2Tran M -> Function of ( TOP-REAL n), ( TOP-REAL m) means

      : Def3: (it . f) = ( Line ((( LineVec2Mx ( @ f)) * M),1)) if n <> 0

      otherwise (it . f) = ( 0. ( TOP-REAL m));

      existence

      proof

        set Tm = ( TOP-REAL m);

        set Tn = ( TOP-REAL n);

         A1:

        now

          assume

           A2: n <> 0 ;

          defpred P[ Element of Tn, Element of Tm] means $2 = ( Line ((( LineVec2Mx ( @ $1)) * M),1));

          

           A3: for x be Element of Tn holds ex y be Element of Tm st P[x, y]

          proof

            let x be Element of Tn;

            set L = ( LineVec2Mx ( @ x));

            set LL = ( Line ((L * M),1));

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

            then

             A4: ( width L) = n by MATRIX13: 1;

            ( len M) = n & ( width M) = m by A2, MATRIX13: 1;

            then ( width (L * M)) = m by A4, MATRIX_3:def 4;

            then LL in ( REAL m);

            then

            reconsider LL as Element of Tm by EUCLID: 22;

             P[x, LL];

            hence thesis;

          end;

          consider F be Function of Tn, Tm such that

           A5: for x be Element of Tn holds P[x, (F . x)] from FUNCT_2:sch 3( A3);

          take F;

          let f;

          (( @ f) is FinSequence of REAL ) & ( len f) = n by CARD_1:def 7;

          then f is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

          then f in ( REAL n);

          then f is Element of Tn by EUCLID: 22;

          hence (F . f) = ( Line ((( LineVec2Mx ( @ f)) * M),1)) by A5;

        end;

        now

          assume n = 0 ;

          defpred P[ Element of Tn, Element of Tm] means $2 = ( 0. Tm);

          

           A6: for x be Element of Tn holds ex y be Element of Tm st P[x, y];

          consider F be Function of Tn, Tm such that

           A7: for x be Element of Tn holds P[x, (F . x)] from FUNCT_2:sch 3( A6);

          take F;

          let f;

          (( @ f) is FinSequence of REAL ) & ( len f) = n by CARD_1:def 7;

          then f is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

          then f in ( REAL n);

          then f is Element of Tn by EUCLID: 22;

          hence (F . f) = ( 0. Tm) by A7;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let F1,F2 be Function of ( TOP-REAL n), ( TOP-REAL m);

         A8:

        now

          assume n <> 0 ;

          assume

           A9: (F1 . f) = ( Line ((( LineVec2Mx ( @ f)) * M),1));

          assume

           A10: (F2 . f) = ( Line ((( LineVec2Mx ( @ f)) * M),1));

          now

            let x be Element of ( TOP-REAL n);

            

            thus (F1 . x) = ( Line ((( LineVec2Mx ( @ x)) * M),1)) by A9

            .= (F2 . x) by A10;

          end;

          hence F1 = F2 by FUNCT_2: 63;

        end;

        now

          assume n = 0 ;

          assume

           A11: (F1 . f) = ( 0. ( TOP-REAL m));

          assume

           A12: (F2 . f) = ( 0. ( TOP-REAL m));

          now

            let x be Element of ( TOP-REAL n);

            

            thus (F1 . x) = ( 0. ( TOP-REAL m)) by A11

            .= (F2 . x) by A12;

          end;

          hence F1 = F2 by FUNCT_2: 63;

        end;

        hence thesis by A8;

      end;

      correctness ;

    end

     Lm3:

    now

      let n, m, M;

      let x be object;

      set T = ( Mx2Tran M);

      per cases ;

        suppose

         A1: x in ( dom T);

        

         A2: ( rng T) c= the carrier of ( TOP-REAL m) by RELAT_1:def 19;

        (T . x) in ( rng T) by A1, FUNCT_1:def 3;

        hence (T . x) is real-valued FinSequence by A2;

      end;

        suppose not x in ( dom T);

        hence (T . x) is real-valued FinSequence by FUNCT_1:def 2;

      end;

    end;

    registration

      let n, m, M;

      let x be object;

      cluster (( Mx2Tran M) . x) -> Function-like Relation-like;

      coherence by Lm3;

    end

    registration

      let n, m, M;

      let x be object;

      cluster (( Mx2Tran M) . x) -> real-valued FinSequence-like;

      coherence by Lm3;

    end

    registration

      let n, m, M, f;

      cluster (( Mx2Tran M) . f) -> m -element;

      coherence

      proof

        set T = ( Mx2Tran M);

        (( @ f) is FinSequence of REAL ) & ( len f) = n by CARD_1:def 7;

        then f is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

        then f in ( REAL n);

        then f in the carrier of ( TOP-REAL n) by EUCLID: 22;

        then f in ( dom T) by FUNCT_2:def 1;

        then

         A1: (T . f) in ( rng T) by FUNCT_1:def 3;

        ( rng T) c= the carrier of ( TOP-REAL m) by RELAT_1:def 19;

        hence thesis by A1;

      end;

    end

    theorem :: MATRTOP1:18

    

     Th18: 1 <= i & i <= m & n <> 0 implies ((( Mx2Tran M) . f) . i) = (( @ f) "*" ( Col (M,i)))

    proof

      assume that

       A1: 1 <= i & i <= m and

       A2: n <> 0 ;

      

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

      set Lf = ( LineVec2Mx ( @ f));

      set LfM = (Lf * M);

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

      then

       A4: ( width Lf) = n by MATRIX13: 1;

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

      then

       A5: ( width LfM) = m by A4, A3, MATRIX_3:def 4;

      ( len Lf) = 1 by MATRIX13: 1;

      then ( len LfM) = 1 by A4, A3, MATRIX_3:def 4;

      then

       A6: [1, i] in ( Indices LfM) by A1, A5, MATRIX_0: 30;

      set LM = ( Line (LfM,1));

      i in ( Seg m) & (( Mx2Tran M) . f) = LM by A1, A2, Def3;

      

      hence ((( Mx2Tran M) . f) . i) = (LfM * (1,i)) by A5, MATRIX_0:def 7

      .= (( Line (Lf,1)) "*" ( Col (M,i))) by A4, A3, A6, MATRIX_3:def 4

      .= (( @ f) "*" ( Col (M,i))) by MATRIX15: 25;

    end;

    theorem :: MATRTOP1:19

    

     Th19: ( len ( MX2FinS ( 1. (K,n)))) = n

    proof

      ( MX2FinS ( 1. (K,n))) is OrdBasis of (n -VectSp_over K) by MATRLIN2: 45;

      

      hence ( len ( MX2FinS ( 1. (K,n)))) = ( dim (n -VectSp_over K)) by MATRLIN2: 21

      .= n by MATRIX13: 112;

    end;

    theorem :: MATRTOP1:20

    

     Th20: for Bn be OrdBasis of (n -VectSp_over F_Real ), Bm be OrdBasis of (m -VectSp_over F_Real ) st Bn = ( MX2FinS ( 1. ( F_Real ,n))) & Bm = ( MX2FinS ( 1. ( F_Real ,m))) holds for M1 be Matrix of ( len Bn), ( len Bm), F_Real st M1 = M holds ( Mx2Tran M) = ( Mx2Tran (M1,Bn,Bm))

    proof

      let Bn be OrdBasis of (n -VectSp_over F_Real ), Bm be OrdBasis of (m -VectSp_over F_Real ) such that

       A1: Bn = ( MX2FinS ( 1. ( F_Real ,n))) and

       A2: Bm = ( MX2FinS ( 1. ( F_Real ,m)));

      set T = ( Mx2Tran M);

      let M1 be Matrix of ( len Bn), ( len Bm), F_Real such that

       A3: M1 = M;

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

      ( dom Tb) = the carrier of (n -VectSp_over F_Real ) by FUNCT_2:def 1;

      

      then

       A4: ( dom Tb) = ( REAL n) by MATRIX13: 102

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

      

       A5: for x be object st x in ( dom T) holds (T . x) = (Tb . x)

      proof

        let x be object;

        assume x in ( dom T);

        then

        reconsider v = x as Element of ( TOP-REAL n) by FUNCT_2:def 1;

        reconsider g = v as Vector of (n -VectSp_over F_Real ) by A4, FUNCT_2:def 1;

        set L = ( LineVec2Mx ( @ v));

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

        then

         A6: ( len L) = 1 & ( width L) = n by MATRIX13: 1;

        

         A7: ( len Bn) = n by A1, Th19;

        

         A8: ( len Bm) = m by A2, Th19;

        per cases ;

          suppose

           A9: n = 0 ;

          

          then (Tb . g) = ( 0. (m -VectSp_over F_Real )) by A1, Th19, MATRLIN2: 33

          .= (m |-> ( 0. F_Real )) by MATRIX13: 102

          .= ( 0* m)

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

          .= (T . v) by A9, Def3;

          hence thesis;

        end;

          suppose

           A10: n > 0 ;

          

           A11: ((Tb . g) |-- Bm) = (Tb . g) by A2, A8, MATRLIN2: 46;

          

           A12: (g |-- Bn) = g & ( AutMt (Tb,Bn,Bm)) = M by A1, A3, A7, MATRLIN2: 36, MATRLIN2: 46;

          1 in ( dom L) & ( len M) = ( width L) by A10, A6, FINSEQ_3: 25, MATRIX13: 1;

          

          then ( LineVec2Mx ( Line ((L * M),1))) = (( LineVec2Mx ( Line (L,1))) * M) by MATRLIN2: 35

          .= (L * M) by MATRIX15: 25

          .= ( LineVec2Mx ((Tb . g) |-- Bm)) by A7, A10, A12, MATRLIN2: 31;

          

          hence (Tb . x) = ( Line (( LineVec2Mx ( Line ((L * M),1))),1)) by A11, MATRIX15: 25

          .= ( Line ((L * M),1)) by MATRIX15: 25

          .= (T . x) by A10, Def3;

        end;

      end;

      ( dom T) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;

      hence thesis by A4, A5, FUNCT_1: 2;

    end;

    theorem :: MATRTOP1:21

    for P be Permutation of ( Seg n) holds (( Mx2Tran M) . f) = (( Mx2Tran (M * P)) . (f * P)) & (f * P) is n -element FinSequence of REAL

    proof

      let P be Permutation of ( Seg n);

      

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

      then

       A2: ( rng P) = ( Seg n) & ( dom f) = ( Seg n) by FINSEQ_1:def 3, FUNCT_2:def 3;

      ( dom P) = ( Seg n) by FUNCT_2: 52;

      then

       A3: ( dom (f * P)) = ( Seg n) by A2, RELAT_1: 27;

      then

      reconsider fP = (f * P) as FinSequence by FINSEQ_1:def 2;

      ( rng (f * P)) = ( rng f) by A2, RELAT_1: 28;

      then

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

      

       A4: ( len fP) = n by A1, A3, FINSEQ_1:def 3;

      then

       A5: fP is n -element by CARD_1:def 7;

      (( Mx2Tran M) . f) = (( Mx2Tran (M * P)) . (f * P))

      proof

        per cases ;

          suppose

           A6: n <> 0 ;

          then

           A7: ( width M) = m by MATRIX13: 1;

          set MP = (M * P);

          

           A8: ( len M) = n by A6, MATRIX13: 1;

           A9:

          now

            let i be Nat;

            assume

             A10: 1 <= i & i <= m;

            then i in ( Seg m);

            

            then

             A11: ( mlt (( @ fP),( Col (MP,i)))) = (the multF of F_Real .: (fP,(( Col (M,i)) * P))) by A7, Th15

            .= (( mlt (( @ f),( Col (M,i)))) * P) by FUNCOP_1: 25;

            ( len ( Col (M,i))) = n by A8, CARD_1:def 7;

            then ( len ( mlt (( @ f),( Col (M,i))))) = n by A1, MATRIX_3: 6;

            then

             A12: ( dom ( mlt (( @ f),( Col (M,i))))) = ( Seg n) by FINSEQ_1:def 3;

            ((( Mx2Tran MP) . fP) . i) = (( @ fP) "*" ( Col (MP,i))) by A6, A5, A10, Th18

            .= (the addF of F_Real "**" ( mlt (( @ fP),( Col (MP,i)))));

            

            hence ((( Mx2Tran MP) . fP) . i) = (( @ f) "*" ( Col (M,i))) by A12, A11, FINSOP_1: 7

            .= ((( Mx2Tran M) . f) . i) by A6, A10, Th18;

          end;

          ( len (( Mx2Tran M) . f)) = m & ( len (( Mx2Tran MP) . fP)) = m by A5, CARD_1:def 7;

          hence thesis by A9;

        end;

          suppose

           A13: n = 0 ;

          ( len fP) = n by A4;

          then ( card fP) = n;

          then

           A14: fP is n -element FinSequence by CARD_1:def 7;

          

          thus (( Mx2Tran M) . f) = ( 0. ( TOP-REAL m)) by Def3, A13

          .= (( Mx2Tran (M * P)) . fP) by A13, Def3, A14

          .= (( Mx2Tran (M * P)) . (f * P));

        end;

      end;

      hence thesis by A4, CARD_1:def 7;

    end;

    theorem :: MATRTOP1:22

    

     Th22: (( Mx2Tran M) . (f1 + f2)) = ((( Mx2Tran M) . f1) + (( Mx2Tran M) . f2))

    proof

      set f12 = (f1 + f2);

      set T = ( Mx2Tran M);

      per cases ;

        suppose

         A1: n <> 0 ;

        per cases ;

          suppose

           A2: m = 0 ;

          (T . f12) = ( 0.REAL 0 ) by A2;

          hence thesis by A2;

        end;

          suppose m > 0 ;

          then

           A3: m >= 1 by NAT_1: 14;

          

           A4: ( len M) = n by A1, MATRIX13: 1;

          set L2 = ( LineVec2Mx ( @ f2));

          set L1 = ( LineVec2Mx ( @ f1));

          

           A5: ( len L2) = 1 by MATRIX13: 1;

          

           A6: ( len f2) = n by CARD_1:def 7;

          then

           A7: ( width L2) = n by MATRIX13: 1;

          

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

          then

           A9: ( width (L2 * M)) = m by A7, A4, MATRIX_3:def 4;

          

           A10: ( len f1) = n by CARD_1:def 7;

          then

           A11: ( width L1) = n by MATRIX13: 1;

          then

           A12: ( width (L1 * M)) = m by A4, A8, MATRIX_3:def 4;

          

           A13: ( len L1) = 1 by MATRIX13: 1;

          then ( len (L1 * M)) = 1 by A11, A4, MATRIX_3:def 4;

          then

           A14: [1, 1] in ( Indices (L1 * M)) by A12, A3, MATRIX_0: 30;

          

           A15: ( @ (T . f1)) = ( Line ((L1 * M),1)) & ( @ (T . f2)) = ( Line ((L2 * M),1)) by A1, Def3;

          ( @ f12) = (( @ f1) + ( @ f2)) by RVSUM_1:def 4;

          

          then (( LineVec2Mx ( @ f12)) * M) = ((L1 + L2) * M) by A10, A6, MATRIX15: 27

          .= ((L1 * M) + (L2 * M)) by A1, A13, A5, A11, A7, A4, MATRIX_4: 63;

          

          hence (T . f12) = ( Line (((L1 * M) + (L2 * M)),1)) by A1, Def3

          .= (( Line ((L1 * M),1)) + ( Line ((L2 * M),1))) by A12, A9, A14, MATRIX_4: 59

          .= ((T . f1) + (T . f2)) by A15, RVSUM_1:def 4;

        end;

      end;

        suppose

         A16: n = 0 ;

        reconsider zz = 0 as Real;

        

         A17: ( 0. ( TOP-REAL m)) = ( 0* m) by EUCLID: 70

        .= (m |-> 0 );

        then

         A18: (T . f2) = (m |-> 0 ) by A16, Def3;

        

        thus (T . (f1 + f2)) = (m |-> (zz + zz)) by A16, A17, Def3

        .= ((m |-> zz) + (m |-> zz)) by RVSUM_1: 14

        .= ((T . f1) + (T . f2)) by A16, A18;

      end;

    end;

    reconsider zz = 0 as Real;

    theorem :: MATRTOP1:23

    

     Th23: (( Mx2Tran M) . (r * f)) = (r * (( Mx2Tran M) . f))

    proof

      set rf = (r * f);

      set T = ( Mx2Tran M);

      per cases ;

        suppose

         A1: n <> 0 ;

        per cases ;

          suppose

           A2: m = 0 ;

          then (T . rf) = ( 0.REAL 0 );

          hence thesis by A2;

        end;

          suppose m > 0 ;

          reconsider R = r as Element of F_Real by XREAL_0:def 1;

          set Lr = ( LineVec2Mx ( @ rf));

          set L = ( LineVec2Mx ( @ f));

          

           A3: (R * ( @ f)) = ( @ rf) by MATRIXR1: 17;

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

          then

           A4: ( width L) = n by MATRIX13: 1;

          

           A5: ( len M) = n by A1, MATRIX13: 1;

          ( len L) = 1 by MATRIX13: 1;

          then

           A6: ( len (L * M)) = 1 by A4, A5, MATRIX_3:def 4;

          (T . ( @ f)) = ( Line ((L * M),1)) by A1, Def3;

          

          hence (r * (T . f)) = (R * ( Line ((L * M),1))) by MATRIXR1: 17

          .= ( Line ((R * (L * M)),1)) by A6, MATRIXR1: 20

          .= ( Line (((R * L) * M),1)) by A4, A5, MATRIX15: 1

          .= ( Line ((Lr * M),1)) by A3, MATRIX15: 29

          .= (T . (r * f)) by A1, Def3;

        end;

      end;

        suppose

         A7: n = 0 ;

        

         A8: ( 0. ( TOP-REAL m)) = ( 0* m) by EUCLID: 70

        .= (m |-> 0 );

        

        hence (T . rf) = (m |-> (r * zz)) by A7, Def3

        .= (r * (m |-> zz)) by RVSUM_1: 48

        .= (r * (T . f)) by A7, A8, Def3;

      end;

    end;

    theorem :: MATRTOP1:24

    

     Th24: (( Mx2Tran M) . (f1 - f2)) = ((( Mx2Tran M) . f1) - (( Mx2Tran M) . f2))

    proof

      (f1 - f2) = (f1 + ( - f2)) by RVSUM_1: 31

      .= (f1 + (( - 1) * f2)) by RVSUM_1: 54;

      

      hence (( Mx2Tran M) . (f1 - f2)) = ((( Mx2Tran M) . f1) + (( Mx2Tran M) . (( - 1) * f2))) by Th22

      .= ((( Mx2Tran M) . f1) + (( - 1) * (( Mx2Tran M) . f2))) by Th23

      .= ((( Mx2Tran M) . f1) + ( - (( Mx2Tran M) . f2))) by RVSUM_1: 54

      .= ((( Mx2Tran M) . f1) - (( Mx2Tran M) . f2)) by RVSUM_1: 31;

    end;

    theorem :: MATRTOP1:25

    (( Mx2Tran (M1 + M2)) . f) = ((( Mx2Tran M1) . f) + (( Mx2Tran M2) . f))

    proof

      set T12 = ( Mx2Tran (M1 + M2));

      set T2 = ( Mx2Tran M2);

      set T1 = ( Mx2Tran M1);

      per cases ;

        suppose

         A1: n <> 0 ;

        per cases ;

          suppose

           A2: m = 0 ;

          then (T12 . f) = ( 0.REAL 0 );

          hence thesis by A2;

        end;

          suppose

           A3: m > 0 ;

          set L = ( LineVec2Mx ( @ f));

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

          then

           A4: ( width L) = n by MATRIX13: 1;

          

           A5: ( len M2) = n & ( width M2) = m by A1, MATRIX13: 1;

          then

           A6: ( width (L * M2)) = m by A4, MATRIX_3:def 4;

          

           A7: 1 <= m by A3, NAT_1: 14;

          

           A8: ( len M1) = n by A1, MATRIX13: 1;

          

           A9: ( width M1) = m by A1, MATRIX13: 1;

          then

           A10: ( width (L * M1)) = m by A4, A8, MATRIX_3:def 4;

          

           A11: ( len L) = 1 by MATRIX13: 1;

          then ( len (L * M1)) = 1 by A4, A8, MATRIX_3:def 4;

          then

           A12: [1, 1] in ( Indices (L * M1)) by A10, A7, MATRIX_0: 30;

          ( @ (T1 . f)) = ( Line ((L * M1),1)) & ( @ (T2 . f)) = ( Line ((L * M2),1)) by A1, Def3;

          

          hence ((T1 . f) + (T2 . f)) = (( Line ((L * M1),1)) + ( Line ((L * M2),1))) by RVSUM_1:def 4

          .= ( Line (((L * M1) + (L * M2)),1)) by A10, A6, A12, MATRIX_4: 59

          .= ( Line ((L * (M1 + M2)),1)) by A1, A11, A4, A8, A9, A5, MATRIX_4: 62

          .= (T12 . f) by A1, Def3;

        end;

      end;

        suppose

         A13: n = 0 ;

        

         A14: ( 0. ( TOP-REAL m)) = ( 0* m) by EUCLID: 70

        .= (m |-> 0 );

        then

         A15: (T2 . f) = (m |-> 0 ) by A13, Def3;

        

        thus (T12 . f) = (m |-> (zz + zz)) by A13, A14, Def3

        .= ((m |-> zz) + (m |-> zz)) by RVSUM_1: 14

        .= ((T1 . f) + (T2 . f)) by A13, A14, A15, Def3;

      end;

    end;

    theorem :: MATRTOP1:26

    r = R implies (r * (( Mx2Tran M) . f)) = (( Mx2Tran (R * M)) . f)

    proof

      set L = ( LineVec2Mx ( @ f));

      set RM = (R * M);

      set T = ( Mx2Tran M);

      set TR = ( Mx2Tran RM);

      assume that

       A1: r = R;

      per cases ;

        suppose

         A2: n <> 0 ;

        

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

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

        then

         A4: ( width L) = n by MATRIX13: 1;

        ( len L) = 1 by MATRIX13: 1;

        then

         A5: ( len (L * M)) = 1 by A4, A3, MATRIX_3:def 4;

        (T . f) = ( Line ((L * M),1)) by A2, Def3;

        

        hence (r * (T . f)) = (R * ( Line ((L * M),1))) by A1, MATRIXR1: 17

        .= ( Line ((R * (L * M)),1)) by A5, MATRIXR1: 20

        .= ( Line ((L * RM),1)) by A4, A3, MATRIXR1: 22

        .= (TR . f) by A2, Def3;

      end;

        suppose

         A6: n = 0 ;

        

         A7: ( 0. ( TOP-REAL m)) = ( 0* m) by EUCLID: 70

        .= (m |-> 0 );

        

        hence (r * (T . f)) = (r * (m |-> zz)) by A6, Def3

        .= (m |-> (r * zz)) by RVSUM_1: 48

        .= (TR . f) by A6, A7, Def3;

      end;

    end;

    theorem :: MATRTOP1:27

    

     Th27: (( Mx2Tran M) . (p1 + p2)) = ((( Mx2Tran M) . p1) + (( Mx2Tran M) . p2)) by Th22;

    theorem :: MATRTOP1:28

    

     Th28: (( Mx2Tran M) . (p1 - p2)) = ((( Mx2Tran M) . p1) - (( Mx2Tran M) . p2)) by Th24;

    theorem :: MATRTOP1:29

    

     Th29: (( Mx2Tran M) . ( 0. ( TOP-REAL n))) = ( 0. ( TOP-REAL m))

    proof

      set TRn = the Element of ( TOP-REAL n);

      set MT = ( Mx2Tran M);

      ( 0. ( TOP-REAL n)) = (TRn - TRn) by RLVECT_1: 5;

      

      hence (MT . ( 0. ( TOP-REAL n))) = ((MT . TRn) - (MT . TRn)) by Th28

      .= ( 0. ( TOP-REAL m)) by RLVECT_1: 5;

    end;

    theorem :: MATRTOP1:30

    for A be Subset of ( TOP-REAL n) holds (( Mx2Tran M) .: (p + A)) = ((( Mx2Tran M) . p) + (( Mx2Tran M) .: A))

    proof

      set TRn = ( TOP-REAL n);

      set TRm = ( TOP-REAL m);

      set MT = ( Mx2Tran M);

      let A be Subset of TRn;

      

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

      thus (MT .: (p + A)) c= ((MT . p) + (MT .: A))

      proof

        let y be object;

        assume y in (MT .: (p + A));

        then

        consider x be object such that x in ( dom MT) and

         A2: x in (p + A) and

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

        x in { (p + w) where w be Element of TRn : w in A } by A2, RUSUB_4:def 8;

        then

        consider w be Element of TRn such that

         A4: x = (p + w) & w in A;

        (MT . w) in (MT .: A) & (MT . x) = ((MT . p) + (MT . w)) by A1, A4, Th27, FUNCT_1:def 6;

        then (MT . x) in { ((MT . p) + u) where u be Element of TRm : u in (MT .: A) };

        hence thesis by A3, RUSUB_4:def 8;

      end;

      let y be object;

      assume y in ((MT . p) + (MT .: A));

      then y in { ((MT . p) + u) where u be Element of TRm : u in (MT .: A) } by RUSUB_4:def 8;

      then

      consider u be Element of TRm such that

       A5: y = ((MT . p) + u) and

       A6: u in (MT .: A);

      consider w be object such that w in ( dom MT) and

       A7: w in A and

       A8: (MT . w) = u by A6, FUNCT_1:def 6;

      reconsider w as Element of TRn by A7;

      (p + w) in { (p + L) where L be Element of TRn : L in A } by A7;

      then

       A9: (p + w) in (p + A) by RUSUB_4:def 8;

      y = (MT . (p + w)) by A5, A8, Th27;

      hence thesis by A1, A9, FUNCT_1:def 6;

    end;

    theorem :: MATRTOP1:31

    for A be Subset of ( TOP-REAL m) holds (( Mx2Tran M) " ((( Mx2Tran M) . p) + A)) = (p + (( Mx2Tran M) " A))

    proof

      set MT = ( Mx2Tran M);

      set TRn = ( TOP-REAL n);

      set TRm = ( TOP-REAL m);

      let A be Subset of TRm;

      set w = p;

      set MTw = (MT . w);

      

       A1: (w + (MT " A)) = { (w + v) where v be Element of TRn : v in (MT " A) } by RUSUB_4:def 8;

      

       A2: (MTw + A) = { (MTw + v) where v be Element of TRm : v in A } by RUSUB_4:def 8;

      

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

      hereby

        let x be object;

        assume

         A4: x in (MT " (MTw + A));

        then

        reconsider f = x as Element of TRn;

        (MT . x) in (MTw + A) by A4, FUNCT_1:def 7;

        then

        consider v be Element of TRm such that

         A5: (MT . x) = (MTw + v) and

         A6: v in A by A2;

        ((MT . f) - MTw) = ((v + MTw) - MTw) by A5

        .= (v + (MTw - MTw)) by RLVECT_1: 28

        .= (v + ( 0. TRm)) by RLVECT_1: 15

        .= v by RLVECT_1: 4;

        then v = (MT . (f - w)) by Th28;

        then

         A7: (f - w) in (MT " A) by A3, A6, FUNCT_1:def 7;

        (w + (f - w)) = ((f - w) + w)

        .= (f - (w - w)) by RLVECT_1: 29

        .= (f - ( 0. TRn)) by RLVECT_1: 15

        .= f by RLVECT_1: 13;

        hence x in (w + (MT " A)) by A1, A7;

      end;

      let x be object;

      assume x in (w + (MT " A));

      then

      consider v be Element of TRn such that

       A8: x = (w + v) and

       A9: v in (MT " A) by A1;

      

       A10: (MT . v) in A by A9, FUNCT_1:def 7;

      (MT . (w + v)) = (MTw + (MT . v)) by Th27;

      then (MT . x) in (MTw + A) by A2, A8, A10;

      hence thesis by A3, A8, FUNCT_1:def 7;

    end;

    theorem :: MATRTOP1:32

    

     Th32: for A be Matrix of n, m, F_Real , B be Matrix of ( width A), k, F_Real st (n = 0 implies m = 0 ) & (m = 0 implies k = 0 ) holds (( Mx2Tran B) * ( Mx2Tran A)) = ( Mx2Tran (A * B))

    proof

      let A be Matrix of n, m, F_Real , B be Matrix of ( width A), k, F_Real such that

       A1: n = 0 implies m = 0 and

       A2: m = 0 implies k = 0 ;

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

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

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

      

       A3: ( len A) = n by A1, MATRIX13: 1;

      

       A4: ( len Bk) = k by Th19;

      

       A5: ( len Bm) = m by Th19;

      

       A6: ( len Bn) = n by Th19;

      then

      reconsider A1 = A as Matrix of ( len Bn), ( len Bm), F_Real by A5;

      

       A7: ( Mx2Tran A) = ( Mx2Tran (A1,Bn,Bm)) by Th20;

      

       A8: ( width A) = m by A1, MATRIX13: 1;

      then

       A9: ( width B) = k by A2, MATRIX13: 1;

      then

      reconsider AB = (A * B) as Matrix of ( len Bn), ( len Bk), F_Real by A3, A6, A4;

      ( len Bm) = m by Th19;

      then

      reconsider B1 = B as Matrix of ( len Bm), ( len Bk), F_Real by A8, A4;

      

       A10: ( len B1) = m by A2, A8, MATRIX13: 1;

      ( Mx2Tran (A * B)) = ( Mx2Tran (AB,Bn,Bk)) by A3, A9, Th20;

      then ( Mx2Tran (A * B)) = (( Mx2Tran (B1,Bm,Bk)) * ( Mx2Tran (A1,Bn,Bm))) by A8, A10, MATRLIN2: 40;

      hence thesis by A8, A7, Th20;

    end;

    theorem :: MATRTOP1:33

    

     Th33: ( Mx2Tran ( 1. ( F_Real ,n))) = ( id ( TOP-REAL n))

    proof

      set V = (n -VectSp_over F_Real );

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

      

       A1: ( len Bn) = n by Th19;

      then

      reconsider ONE = ( 1. ( F_Real ,n)) as Matrix of ( len Bn), ( len Bn), F_Real ;

      

       A2: ( Mx2Tran ( 1. ( F_Real ,n))) = ( Mx2Tran (ONE,Bn,Bn)) by Th20;

      

       A3: ( [#] ( TOP-REAL n)) = ( dom ( Mx2Tran ( 1. ( F_Real ,n)))) by FUNCT_2:def 1

      .= ( [#] V) by A2, FUNCT_2:def 1;

      

      thus ( Mx2Tran ( 1. ( F_Real ,n))) = ( Mx2Tran (( AutMt (( id V),Bn,Bn)),Bn,Bn)) by A1, Th20, MATRLIN2: 28

      .= ( id ( TOP-REAL n)) by A3, MATRLIN2: 34;

    end;

    theorem :: MATRTOP1:34

    

     Th34: ( Mx2Tran M1) = ( Mx2Tran M2) implies M1 = M2

    proof

      assume that

       A1: ( Mx2Tran M1) = ( Mx2Tran M2);

      set Vn = (n -VectSp_over F_Real ), Vm = (m -VectSp_over F_Real );

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

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

      

       A2: ( len Bm) = m by Th19;

      ( len Bn) = n by Th19;

      then

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

      

       A3: ( Mx2Tran (A1,Bn,Bm)) = ( Mx2Tran M1) by Th20

      .= ( Mx2Tran (B1,Bn,Bm)) by A1, Th20;

      

      thus M1 = ( AutMt (( Mx2Tran (A1,Bn,Bm)),Bn,Bm)) by MATRLIN2: 36

      .= M2 by A3, MATRLIN2: 36;

    end;

    theorem :: MATRTOP1:35

    

     Th35: for A be Matrix of n, m, F_Real , B be Matrix of k, m, F_Real holds (( Mx2Tran (A ^ B)) . (f ^ (k |-> 0 ))) = (( Mx2Tran A) . f) & (( Mx2Tran (B ^ A)) . ((k |-> 0 ) ^ f)) = (( Mx2Tran A) . f)

    proof

      let A be Matrix of n, m, F_Real , B be Matrix of k, m, F_Real ;

      reconsider k0 = (k |-> ( In ( 0 , REAL ))) as k -element FinSequence of REAL ;

      

       A1: ( len B) = k by MATRIX_0:def 2;

      set kf = (k0 ^ f);

      per cases ;

        suppose

         A2: n <> 0 ;

        then

         A3: ( width A) = m by MATRIX13: 1;

        

         A4: ( len f) = n & ( len k0) = k by CARD_1:def 7;

        

         A5: ( len A) = n by A2, MATRIX13: 1;

        thus (( Mx2Tran (A ^ B)) . (f ^ (k |-> 0 ))) = (( Mx2Tran A) . f)

        proof

          set fk = (f ^ k0);

          per cases ;

            suppose

             A6: k = 0 ;

            then B is empty by A1;

            then

             A7: ( Mx2Tran (A ^ B)) = ( Mx2Tran A) by A6, FINSEQ_1: 34;

            k0 is empty by A6;

            hence thesis by A7, FINSEQ_1: 34;

          end;

            suppose

             A8: k <> 0 ;

            set Mab = ( Mx2Tran (A ^ B)), Ma = ( Mx2Tran A);

            

             A9: ( width B) = m by A8, MATRIX_0: 23;

             A10:

            now

              let i;

              reconsider S1 = ( Sum ( mlt (( @ k0),( Col (B,i))))), S2 = ( Sum ( mlt (( @ f),( Col (A,i))))) as Element of F_Real ;

              assume

               A11: 1 <= i & i <= m;

              then

               A12: i in ( Seg m);

              ( mlt (( @ k0),( Col (B,i)))) = (( 0. F_Real ) * ( Col (B,i))) by A1, FVSUM_1: 66

              .= (k |-> ( 0. F_Real )) by A1, FVSUM_1: 58;

              

              then

               A13: ( Sum ( mlt (( @ k0),( Col (B,i))))) = ( Sum (k |-> 0 )) by MATRPROB: 36

              .= ( 0. F_Real qua Field) by RVSUM_1: 81;

              

               A14: ( len ( Col (A,i))) = n & ( len ( Col (B,i))) = k by A5, A1, MATRIX_0:def 8;

              ( mlt (( @ fk),( Col ((A ^ B),i)))) = ( mlt ((( @ f) ^ ( @ k0)),(( Col (A,i)) ^ ( Col (B,i))))) by A3, A9, A12, MATRLIN: 26

              .= (( mlt (( @ f),( Col (A,i)))) ^ ( mlt (( @ k0),( Col (B,i))))) by A4, A14, MATRIX14: 7;

              

              then ( Sum ( mlt (( @ fk),( Col ((A ^ B),i))))) = ( addreal . (( Sum ( mlt (( @ f),( Col (A,i))))),( Sum ( mlt (( @ k0),( Col (B,i))))))) by FINSOP_1: 5

              .= (( Sum ( mlt (( @ f),( Col (A,i))))) + ( Sum ( mlt (( @ k0),( Col (B,i)))))) by BINOP_2:def 9

              .= (( @ f) "*" ( Col (A,i))) by A13;

              

              hence ((Ma . f) . i) = (( @ fk) "*" ( Col ((A ^ B),i))) by A2, A11, Th18

              .= ((Mab . fk) . i) by A2, A11, Th18;

            end;

            ( len (Mab . fk)) = m & ( len (Ma . f)) = m by CARD_1:def 7;

            hence thesis by A10;

          end;

        end;

        per cases ;

          suppose

           A15: k = 0 ;

          then B is empty by A1;

          then

           A16: ( Mx2Tran (B ^ A)) = ( Mx2Tran A) by A15, FINSEQ_1: 34;

          k0 is empty by A15;

          hence thesis by A16, FINSEQ_1: 34;

        end;

          suppose

           A17: k <> 0 ;

          set Mba = ( Mx2Tran (B ^ A)), Ma = ( Mx2Tran A);

          

           A18: ( width B) = m by A17, MATRIX_0: 23;

           A19:

          now

            let i;

            reconsider S1 = ( Sum ( mlt (( @ k0),( Col (B,i))))), S2 = ( Sum ( mlt (( @ f),( Col (A,i))))) as Element of F_Real ;

            assume

             A20: 1 <= i & i <= m;

            then

             A21: i in ( Seg m);

            ( mlt (( @ k0),( Col (B,i)))) = (( 0. F_Real ) * ( Col (B,i))) by A1, FVSUM_1: 66

            .= (k |-> ( 0. F_Real )) by A1, FVSUM_1: 58;

            

            then

             A22: ( Sum ( mlt (( @ k0),( Col (B,i))))) = ( Sum (k |-> 0 )) by MATRPROB: 36

            .= ( 0. F_Real qua Field) by RVSUM_1: 81;

            

             A23: ( len ( Col (A,i))) = n & ( len ( Col (B,i))) = k by A5, A1, MATRIX_0:def 8;

            ( mlt (( @ kf),( Col ((B ^ A),i)))) = ( mlt ((( @ k0) ^ ( @ f)),(( Col (B,i)) ^ ( Col (A,i))))) by A3, A18, A21, MATRLIN: 26

            .= (( mlt (( @ k0),( Col (B,i)))) ^ ( mlt (( @ f),( Col (A,i))))) by A4, A23, MATRIX14: 7;

            

            then ( Sum ( mlt (( @ kf),( Col ((B ^ A),i))))) = ( addreal . (( Sum ( mlt (( @ k0),( Col (B,i))))),( Sum ( mlt (( @ f),( Col (A,i))))))) by FINSOP_1: 5

            .= (( Sum ( mlt (( @ f),( Col (A,i))))) + ( 0. F_Real )) by A22, BINOP_2:def 9

            .= (( @ f) "*" ( Col (A,i)));

            

            hence ((Ma . f) . i) = (( @ kf) "*" ( Col ((B ^ A),i))) by A2, A20, Th18

            .= ((Mba . kf) . i) by A2, A20, Th18;

          end;

          ( len (Mba . kf)) = m & ( len (Ma . f)) = m by CARD_1:def 7;

          hence thesis by A19;

        end;

      end;

        suppose

         A24: n = 0 ;

        

         A25: ( 0. ( TOP-REAL k)) = ( 0* k) by EUCLID: 70

        .= (k |-> 0 );

        f = {} by A24;

        then

         A26: (f ^ (k |-> 0 )) = (k |-> 0 ) & ((k |-> 0 ) ^ f) = (k |-> 0 ) by FINSEQ_1: 34;

        

        thus (( Mx2Tran (A ^ B)) . (f ^ (k |-> 0 ))) = ( 0. ( TOP-REAL m)) by A25, A26, Th29, A24

        .= (( Mx2Tran A) . f) by A24, Def3;

        

        thus (( Mx2Tran (B ^ A)) . ((k |-> 0 ) ^ f)) = ( 0. ( TOP-REAL m)) by A25, A26, Th29, A24

        .= (( Mx2Tran A) . f) by A24, Def3;

      end;

    end;

    theorem :: MATRTOP1:36

    for A be Matrix of n, m, F_Real , B be Matrix of k, m, F_Real holds for g be k -element real-valued FinSequence holds (( Mx2Tran (A ^ B)) . (f ^ g)) = ((( Mx2Tran A) . f) + (( Mx2Tran B) . g))

    proof

      

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

      ( rng f) c= REAL ;

      then f is FinSequence of REAL by FINSEQ_1:def 4;

      then

      reconsider F = f, n0 = (n |-> ( In ( 0 , REAL ))) as Element of (n -tuples_on REAL ) by A1, FINSEQ_2: 92;

      let A be Matrix of n, m, F_Real , B be Matrix of k, m, F_Real ;

      let g be k -element real-valued FinSequence;

      

       A2: ( len g) = k by CARD_1:def 7;

      ( rng g) c= REAL ;

      then g is FinSequence of REAL by FINSEQ_1:def 4;

      then

      reconsider G = g, k0 = (k |-> ( In ( 0 , REAL ))) as Element of (k -tuples_on REAL ) by A2, FINSEQ_2: 92;

      f = (F + n0) by RVSUM_1: 16;

      then g = (G + k0) & f = ( addreal .: (f,n0)) by RVSUM_1: 16, RVSUM_1:def 4;

      

      then (f ^ g) = (( addreal .: (F,n0)) ^ ( addreal .: (k0,G))) by RVSUM_1:def 4

      .= ( addreal .: ((F ^ k0),(n0 ^ G))) by FINSEQOP: 11

      .= ((F ^ k0) + (n0 ^ G)) by RVSUM_1:def 4;

      

      hence (( Mx2Tran (A ^ B)) . (f ^ g)) = ((( Mx2Tran (A ^ B)) . (F ^ k0)) + (( Mx2Tran (A ^ B)) . (n0 ^ G))) by Th22

      .= ((( Mx2Tran A) . f) + (( Mx2Tran (A ^ B)) . (n0 ^ G))) by Th35

      .= ((( Mx2Tran A) . f) + (( Mx2Tran B) . g)) by Th35;

    end;

    theorem :: MATRTOP1:37

    for A be Matrix of n, k, F_Real , B be Matrix of n, m, F_Real st n = 0 implies (k + m) = 0 holds (( Mx2Tran (A ^^ B)) . f) = ((( Mx2Tran A) . f) ^ (( Mx2Tran B) . f))

    proof

      let A be Matrix of n, k, F_Real , B be Matrix of n, m, F_Real ;

      set L = ( LineVec2Mx ( @ f));

      set MAB = (( Mx2Tran (A ^^ B)) . f), MA = (( Mx2Tran A) . f), MB = (( Mx2Tran B) . f);

      

       A1: ( len MA) = k by CARD_1:def 7;

      assume

       A2: n = 0 implies (k + m) = 0 ;

      then n = 0 implies k = 0 ;

      then

       A3: ( width A) = k by MATRIX13: 1;

      n = 0 implies m = 0 by A2;

      then

       A4: ( width B) = m by MATRIX13: 1;

      

       A5: ( len MB) = m by CARD_1:def 7;

      then

       A6: ( len (MA ^ MB)) = (k + m) by A1, FINSEQ_1: 22;

      

       A7: for i st 1 <= i & i <= (k + m) holds ((MA ^ MB) . i) = (MAB . i)

      proof

        let i;

        assume that

         A8: 1 <= i and

         A9: i <= (k + m);

        

         A10: i in ( dom (MA ^ MB)) by A6, A8, A9, FINSEQ_3: 25;

        

         A11: (MAB . i) = (( @ f) "*" ( Col ((A ^^ B),i))) by A2, A3, A4, A8, A9, Th18;

        per cases by A10, FINSEQ_1: 25;

          suppose

           A12: i in ( dom MA);

          then i <= k by A1, FINSEQ_3: 25;

          then

           A13: (MA . i) = (( @ f) "*" ( Col (A,i))) by A2, A8, Th18;

          i in ( Seg ( width A)) & ((MA ^ MB) . i) = (MA . i) by A3, A1, A12, FINSEQ_1:def 3, FINSEQ_1:def 7;

          hence ((MA ^ MB) . i) = (MAB . i) by A11, A13, MATRIX15: 16;

        end;

          suppose ex j be Nat st j in ( dom MB) & i = (( len MA) + j);

          then

          consider j be Nat such that

           A14: j in ( dom MB) and

           A15: i = (( len MA) + j);

          1 <= j & j <= m by A5, A14, FINSEQ_3: 25;

          then

           A16: (MB . j) = (( @ f) "*" ( Col (B,j))) by A2, Th18;

          j in ( Seg ( width B)) & ((MA ^ MB) . i) = (MB . j) by A4, A5, A14, A15, FINSEQ_1:def 3, FINSEQ_1:def 7;

          hence ((MA ^ MB) . i) = (MAB . i) by A3, A1, A11, A15, A16, MATRIX15: 17;

        end;

      end;

      ( len MAB) = (k + m) by A3, A4, CARD_1:def 7;

      hence thesis by A6, A7;

    end;

    theorem :: MATRTOP1:38

    M = (( 1. ( F_Real ,m)) | n) implies ((( Mx2Tran M) . f) | n) = f

    proof

      set ONE = ( 1. ( F_Real ,m));

      assume

       A1: M = (ONE | n);

      per cases ;

        suppose

         A2: n = 0 ;

        then ((( Mx2Tran M) . f) | n) is empty;

        hence thesis by A2;

      end;

        suppose

         A3: n > 0 ;

        set TRm = ( TOP-REAL m);

        set V = (m -VectSp_over F_Real );

        

         A4: ( len ONE) = m by MATRIX_0: 24;

        

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

        consider A be FinSequence such that

         A6: ONE = (M ^ A) by A1, FINSEQ_1: 80;

        ONE = ( MX2FinS ONE);

        then

        reconsider A as FinSequence of V by A6, FINSEQ_1: 36;

        set L = ( len A);

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

        then (n + L) = m by A4, A6, FINSEQ_1: 22;

        then

         A7: (f ^ (L |-> 0 )) is Element of TRm by Lm2;

        set A1 = ( FinS2MX A);

        

         A8: ((f ^ (L |-> 0 )) | n) = ((f ^ (L |-> 0 )) | ( dom f)) by A5, FINSEQ_1:def 3

        .= f by FINSEQ_1: 21;

        (( Mx2Tran (M ^ A1)) . (f ^ (L |-> 0 ))) = (( Mx2Tran ONE) . (f ^ (L |-> 0 ))) by A3, A4, A6, MATRIX13: 1

        .= (( id TRm) . (f ^ (L |-> 0 ))) by Th33

        .= (f ^ (L |-> 0 )) by A7;

        hence thesis by A8, Th35;

      end;

    end;

    begin

    theorem :: MATRTOP1:39

    

     Th39: ( Mx2Tran M) is one-to-one iff ( the_rank_of M) = n

    proof

      set MM = ( Mx2Tran M);

      per cases ;

        suppose

         A1: n = 0 iff m = 0 ;

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

        

         A3: ( len Bn) = n by Th19;

        then

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

        

         A4: ( len M1) = n by A1, MATRIX13: 1;

        

         A5: ( len Bm) = m by Th19;

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

        

         A6: T is one-to-one iff ( ker T) = ( (0). nV) by MATRLIN2: 43;

        

         A7: ( width M1) = m by A1, MATRIX13: 1;

        per cases ;

          suppose

           A8: m = 0 ;

          

           A9: the carrier of ( TOP-REAL 0 ) = {( 0. ( TOP-REAL 0 ))} by EUCLID: 22, EUCLID: 77;

          then ( rng MM) c= {( 0. ( TOP-REAL 0 ))} by A8, RELAT_1:def 19;

          then ( rng MM) = {( 0. ( TOP-REAL 0 ))} by ZFMISC_1: 33;

          then ( card {( 0. ( TOP-REAL 0 ))}) = ( card {( 0. ( TOP-REAL 0 ))}) & MM is onto by A8, A9, FUNCT_2:def 3;

          hence thesis by A1, A4, A8, A9, MATRIX13: 74, FINSEQ_4: 63;

        end;

          suppose

           A10: m > 0 ;

          then

          reconsider SS = ( Space_of_Solutions_of (M1 @ )) as Subspace of nV by A4, A7, MATRIX_0: 54;

          

           A11: ( width (M1 @ )) = n by A4, A7, A10, MATRIX_0: 54;

          hereby

            assume

             A12: ( Mx2Tran M) is one-to-one;

            ( [#] SS) c= {( 0. nV)}

            proof

              let x be object;

              assume

               A13: x in ( [#] SS);

              then

              reconsider v = x as Vector of nV by VECTSP_4: 10;

              v = (v |-- Bn) by A3, MATRLIN2: 46;

              then (v |-- Bn) in SS by A13;

              then v in ( ker T) by A1, A3, A5, A10, MATRLIN2: 41;

              then v = ( 0. nV) by A6, A12, Th20, VECTSP_4: 35;

              hence thesis by TARSKI:def 1;

            end;

            then ( [#] SS) = {( 0. nV)} by ZFMISC_1: 33;

            then SS = ( (0). nV) by VECTSP_4:def 3;

            then ( dim SS) = 0 by RANKNULL: 16;

            then 0 = (n - ( the_rank_of (M1 @ ))) by A1, A10, A11, MATRIX15: 68;

            hence ( the_rank_of M) = n by MATRIX13: 84;

          end;

          

           A14: ( the_rank_of (M1 @ )) = ( the_rank_of M) by MATRIX13: 84;

          assume ( the_rank_of M) = n;

          then ( dim SS) = (n - n) by A1, A10, A11, A14, MATRIX15: 68;

          then

           A15: SS is trivial by MATRLIN2: 42;

          ( [#] ( ker T)) c= {( 0. nV)}

          proof

            let x be object;

            assume

             A16: x in ( [#] ( ker T));

            then

            reconsider v = x as Vector of nV by VECTSP_4: 10;

            v in ( ker T) by A16;

            then (v |-- Bn) in SS by A1, A3, A5, A10, MATRLIN2: 41;

            then v in SS by A3, MATRLIN2: 46;

            then v in the carrier of SS;

            then v = ( 0. SS) by A15;

            then v = ( 0. nV) by VECTSP_4: 11;

            hence thesis by TARSKI:def 1;

          end;

          then ( [#] ( ker T)) = {( 0. nV)} by ZFMISC_1: 33;

          hence thesis by A6, Th20, VECTSP_4:def 3;

        end;

      end;

        suppose

         A17: n = 0 & m <> 0 ;

         A18:

        now

          let x1,x2 be object such that

           A19: x1 in ( dom MM) & x2 in ( dom MM) & (MM . x1) = (MM . x2);

          

           A20: ( dom MM) = ( [#] ( TOP-REAL 0 )) by A17, FUNCT_2:def 1

          .= {( 0. ( TOP-REAL 0 ))} by EUCLID: 22, EUCLID: 77;

          

          hence x1 = ( 0. ( TOP-REAL 0 )) by A19, TARSKI:def 1

          .= x2 by A19, A20, TARSKI:def 1;

        end;

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

        hence thesis by A18, A17, FUNCT_1:def 4, MATRIX13: 74;

      end;

        suppose

         A21: n <> 0 & m = 0 ;

        reconsider x1 = (n |-> 1) as Point of ( TOP-REAL n) by Lm2;

        reconsider x2 = (n |-> 2) as Point of ( TOP-REAL n) by Lm2;

        

         A22: ( dom MM) = ( [#] ( TOP-REAL n)) by FUNCT_2:def 1;

        

         A23: (MM . x1) = ( 0. ( TOP-REAL 0 )) by A21

        .= (MM . x2) by A21;

        

         A24: x1 <> x2

        proof

          assume

           A25: x1 = x2;

          

           A26: x1 = (( Seg n) --> 1) by FINSEQ_2:def 2

          .= [:( Seg n), {1}:] by FUNCOP_1:def 2;

          x2 = (( Seg n) --> 2) by FINSEQ_2:def 2

          .= [:( Seg n), {2}:] by FUNCOP_1:def 2;

          then {1} = {2} by A25, A26, A21, ZFMISC_1: 110;

          then 2 in {1} by TARSKI:def 1;

          hence contradiction by TARSKI:def 1;

        end;

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

        hence thesis by A24, A21, A23, A22, FUNCT_1:def 4, MATRIX13: 74;

      end;

    end;

    theorem :: MATRTOP1:40

    

     Th40: ( Mx2Tran A) is one-to-one iff ( Det A) <> ( 0. F_Real )

    proof

      ( Mx2Tran A) is one-to-one iff ( the_rank_of A) = n by Th39;

      hence thesis by MATRIX13: 83;

    end;

    theorem :: MATRTOP1:41

    

     Th41: ( Mx2Tran M) is onto iff ( the_rank_of M) = m

    proof

      set MM = ( Mx2Tran M);

      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;

      

       A1: ( [#] mV) = ( REAL m) by MATRIX13: 102

      .= ( [#] ( TOP-REAL m)) by EUCLID: 22;

      

       A2: ( len Bm) = m by Th19;

      ( len Bn) = n by Th19;

      then

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

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

      

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

      

       A4: ( [#] ( im T)) = (T .: ( [#] nV)) by RANKNULL:def 2

      .= ( rng T) by A3, RELAT_1: 113;

      

       A5: MM = T by Th20;

      hereby

        assume MM is onto;

        then ( [#] ( im T)) = ( [#] ( (Omega). mV)) by A5, A1, A4, FUNCT_2:def 3;

        

        then ( rank T) = ( dim ( (Omega). mV)) by VECTSP_4: 29

        .= m by MATRIX13: 112;

        hence ( the_rank_of M) = m by MATRLIN2: 49;

      end;

      

       A6: ( dim mV) = m by MATRIX13: 112;

      assume ( the_rank_of M) = m;

      

      then m = ( rank T) by MATRLIN2: 49

      .= ( dim ( im T));

      then ( (Omega). ( im T)) = ( (Omega). mV) by A6, VECTSP_9: 28;

      hence thesis by A5, A1, A4, FUNCT_2:def 3;

    end;

    theorem :: MATRTOP1:42

    

     Th42: ( Mx2Tran A) is onto iff ( Det A) <> ( 0. F_Real )

    proof

      ( Mx2Tran A) is onto iff ( the_rank_of A) = n by Th41;

      hence thesis by MATRIX13: 83;

    end;

    theorem :: MATRTOP1:43

    

     Th43: for A, B st ( Det A) <> ( 0. F_Real ) holds (( Mx2Tran A) " ) = ( Mx2Tran B) iff (A ~ ) = B

    proof

      

       A1: n = 0 implies n = 0 ;

      let A, B such that

       A2: ( Det A) <> ( 0. F_Real );

      

       A3: A is invertible by A2, LAPLACE: 34;

      set MA = ( Mx2Tran A), MB = ( Mx2Tran B);

      

       A4: ( width B) = n by MATRIX_0: 24;

      reconsider ma = MA, mb = MB as Function;

      

       A5: ( width A) = n & ( len A) = n by MATRIX_0: 24;

      

       A6: MA is one-to-one by A2, Th40;

      hereby

        assume (MA " ) = MB;

        

        then

         A7: (mb * ma) = ( id ( dom ma)) by A6, FUNCT_1: 39

        .= ( id ( TOP-REAL n)) by FUNCT_2:def 1

        .= ( Mx2Tran ( 1. ( F_Real ,n))) by Th33;

        (MB * MA) = ( Mx2Tran (A * B)) by A5, A4, A1, Th32;

        then B is_reverse_of A by A3, A7, Th34, MATRIX_6: 38;

        hence (A ~ ) = B by A3, MATRIX_6:def 4;

      end;

      assume

       A8: (A ~ ) = B;

      MA is onto by A2, Th42;

      then

       A9: ( dom MB) = ( [#] ( TOP-REAL n)) & ( rng MA) = ( [#] ( TOP-REAL n)) by FUNCT_2:def 1, FUNCT_2:def 3;

      

       A10: n in NAT by ORDINAL1:def 12;

      (MB * MA) = ( Mx2Tran (A * B)) by A5, A4, A1, Th32

      .= ( Mx2Tran ( 1. ( F_Real ,n))) by A3, A10, A8, MATRIX14: 18

      .= ( id ( TOP-REAL n)) by Th33

      .= ( id ( dom MA)) by FUNCT_2:def 1;

      hence thesis by A6, A9, FUNCT_1: 41;

    end;

    

     Lm4: for f be n -element real-valued FinSequence holds ex L be m -element FinSequence of REAL st |.(( Mx2Tran M) . f).| <= (( Sum L) * |.f.|) & for i be Nat st i in ( dom L) holds (L . i) = |.( @ ( Col (M,i))).|

    proof

      let f be n -element real-valued FinSequence;

      set Lf = ( LineVec2Mx ( @ f));

      set LfM = (Lf * M);

      set LM = ( Line (LfM,1));

      deffunc L( Nat) = |.( @ ( Col (M,$1))).|;

      consider L be FinSequence such that

       A1: ( len L) = m & for k be Nat st k in ( dom L) holds (L . k) = L(k) from FINSEQ_1:sch 2;

      ( rng L) c= REAL

      proof

        let y be object;

        assume y in ( rng L);

        then

        consider x be object such that

         A2: x in ( dom L) and

         A3: (L . x) = y by FUNCT_1:def 3;

        reconsider x as Nat by A2;

        (L . x) = L(x) by A1, A2;

        hence thesis by A3, XREAL_0:def 1;

      end;

      then L is FinSequence of REAL by FINSEQ_1:def 4;

      then

      reconsider L1 = L as Element of (m -tuples_on REAL ) by A1, FINSEQ_2: 92;

      take L1;

      per cases ;

        suppose

         A4: n <> 0 ;

        then

         A5: ( len M) = n by MATRIX13: 1;

        (( Mx2Tran M) . f) = LM by A4, Def3;

        then

         A6: ( len LM) = m by CARD_1:def 7;

        

         A7: |.(( Mx2Tran M) . f).| = ( sqrt ( Sum ( sqr ( @ LM)))) by A4, Def3;

        reconsider LM as Element of (m -tuples_on REAL ) by A6, FINSEQ_2: 92;

        ( len ( abs LM)) = m by CARD_1:def 7;

        then

        reconsider aLM = ( abs LM) as Element of (m -tuples_on REAL ) by FINSEQ_2: 92;

        

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

        then

         A9: ( width Lf) = n by MATRIX13: 1;

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

        then

         A10: ( width LfM) = m by A5, A9, MATRIX_3:def 4;

        ( len Lf) = 1 by MATRIX13: 1;

        then

         A11: ( len LfM) = 1 by A5, A9, MATRIX_3:def 4;

        now

          let i be Nat;

          

           A12: ( len ( Col (M,i))) = n by A5, MATRIX_0:def 8;

          then

           A13: |. |(f, ( @ ( Col (M,i))))|.| <= ( |.f.| * L(i)) by A8, EUCLID_2: 15;

          assume

           A14: i in ( Seg m);

          then

           A15: 1 <= i & i <= m by FINSEQ_1: 1;

          then

           A16: [1, i] in ( Indices LfM) by A11, A10, MATRIX_0: 30;

          i in ( dom L) by A1, A15, FINSEQ_3: 25;

          then

           A17: (L . i) = L(i) by A1;

          (LM . i) = (LfM * (1,i)) by A10, A14, MATRIX_0:def 7

          .= (( Line (Lf,1)) "*" ( Col (M,i))) by A5, A9, A16, MATRIX_3:def 4

          .= ( Sum ( mlt (( @ f),( Col (M,i))))) by MATRIX15: 25

          .= ( Sum ( mlt (f,( @ ( Col (M,i)))))) by A8, A12, MATRPROB: 35, MATRPROB: 36

          .= |(f, ( @ ( Col (M,i))))| by RVSUM_1:def 16;

          then (aLM . i) <= ( |.f.| * L(i)) by A13, VALUED_1: 18;

          hence (aLM . i) <= (( |.f.| * L1) . i) by A17, RVSUM_1: 44;

        end;

        then

         A18: ( Sum aLM) <= ( Sum ( |.f.| * L1)) by RVSUM_1: 82;

        ( sqr LM) = (LM (#) LM) by VALUED_1:def 8;

        then ( sqrt ( Sum ( sqr LM))) <= ( Sum ( sqrt ( sqr LM))) by Th5;

        then ( Sum ( |.f.| * L1)) = ( |.f.| * ( Sum L1)) & ( sqrt ( Sum ( sqr LM))) <= ( Sum aLM) by Th4, RVSUM_1: 87;

        hence thesis by A7, A1, A18, XXREAL_0: 2;

      end;

        suppose

         A19: n = 0 ;

        now

          let i be Nat;

          assume i in ( dom L1);

          then (L1 . i) = |.( @ ( Col (M,i))).| by A1;

          hence 0 <= (L1 . i);

        end;

        then

         A20: ( Sum L1) >= 0 by RVSUM_1: 84;

         |.(( Mx2Tran M) . f).| = |.( 0. ( TOP-REAL m)).| by A19, Def3

        .= 0 by EUCLID_2: 39;

        hence thesis by A1, A20;

      end;

    end;

    theorem :: MATRTOP1:44

    

     Th44: ex L be m -element FinSequence of REAL st (for i st i in ( dom L) holds (L . i) = |.( @ ( Col (M,i))).|) & for f holds |.(( Mx2Tran M) . f).| <= (( Sum L) * |.f.|)

    proof

      set F = the n -element real-valued FinSequence;

      consider L be m -element FinSequence of REAL such that |.(( Mx2Tran M) . F).| <= (( Sum L) * |.F.|) and

       A1: for i be Nat st i in ( dom L) holds (L . i) = |.( @ ( Col (M,i))).| by Lm4;

      take L;

      thus for i st i in ( dom L) holds (L . i) = |.( @ ( Col (M,i))).| by A1;

      let f be n -element real-valued FinSequence;

      consider L1 be m -element FinSequence of REAL such that

       A2: |.(( Mx2Tran M) . f).| <= (( Sum L1) * |.f.|) and

       A3: for i be Nat st i in ( dom L1) holds (L1 . i) = |.( @ ( Col (M,i))).| by Lm4;

      ( len L1) = m & ( len L) = m by CARD_1:def 7;

      then

       A4: ( dom L) = ( dom L1) by FINSEQ_3: 29;

      now

        let i be Nat;

        assume

         A5: i in ( dom L);

        

        hence (L . i) = |.( @ ( Col (M,i))).| by A1

        .= (L1 . i) by A3, A4, A5;

      end;

      hence thesis by A2, A4, FINSEQ_1: 13;

    end;

    theorem :: MATRTOP1:45

    

     Th45: ex L be Real st L > 0 & for f holds |.(( Mx2Tran M) . f).| <= (L * |.f.|)

    proof

      consider L be m -element FinSequence of REAL such that

       A1: for i st i in ( dom L) holds (L . i) = |.( @ ( Col (M,i))).| and

       A2: for f be n -element real-valued FinSequence holds |.(( Mx2Tran M) . f).| <= (( Sum L) * |.f.|) by Th44;

      reconsider S1 = (1 + ( Sum L)) as Real;

      take S1;

      now

        let i;

        assume i in ( dom L);

        then (L . i) = |.( @ ( Col (M,i))).| by A1;

        hence 0 <= (L . i);

      end;

      then ( Sum L) >= 0 by RVSUM_1: 84;

      hence S1 > 0 ;

      let f;

      ( Sum L) <= S1 by XREAL_1: 29;

      then

       A3: (( Sum L) * |.f.|) <= (S1 * |.f.|) by XREAL_1: 64;

       |.(( Mx2Tran M) . f).| <= (( Sum L) * |.f.|) by A2;

      hence thesis by A3, XXREAL_0: 2;

    end;

    reconsider jj = 1 as Real;

    theorem :: MATRTOP1:46

    ( the_rank_of M) = n implies ex L be Real st L > 0 & for f holds |.f.| <= (L * |.(( Mx2Tran M) . f).|)

    proof

      assume that

       A1: ( the_rank_of M) = n;

      per cases ;

        suppose

         A2: n <> 0 ;

        consider N be Matrix of (m -' n), m, F_Real such that

         A3: ( the_rank_of (M ^ N)) = m by A1, Th16;

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

        then (m - n) >= 0 by A1, MATRIX13: 74, XREAL_1: 48;

        then

         A4: (m - n) = (m -' n) by XREAL_0:def 2;

        then

        reconsider MN = (M ^ N) as Matrix of m, F_Real ;

        

         A5: ( dom ( id ( TOP-REAL m))) = ( [#] ( TOP-REAL m));

        set mn = ((m -' n) |-> 0 );

        

         A6: m = 0 iff m = 0 ;

        ( sqr mn) = ((m -' n) |-> ( 0 qua Real ^2 )) by RVSUM_1: 56

        .= ((m -' n) |-> ( 0* 0 ));

        then

         A7: ( Sum ( sqr mn)) = ((m -' n) * 0 qua Nat) by RVSUM_1: 80;

        set MN1 = (MN ~ );

        consider L be Real such that

         A8: L > 0 and

         A9: for f be m -element real-valued FinSequence holds |.(( Mx2Tran MN1) . f).| <= (L * |.f.|) by Th45;

        take L;

        thus L > 0 by A8;

        let f be n -element real-valued FinSequence;

        set fm = (f ^ mn);

        set Mfm = (( Mx2Tran MN) . fm);

        

         A10: Mfm = (( Mx2Tran M) . f) by A4, Th35;

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

        then

         A11: MN is invertible by LAPLACE: 34;

        

         A12: ( width MN) = m by MATRIX_0: 24;

        reconsider MN2 = MN1 as Matrix of ( width MN), m, F_Real by A12;

        

         A13: ( width MN1) = m & ( len MN) = m by MATRIX_0: 24;

        

         A14: (( Mx2Tran MN1) * ( Mx2Tran MN)) = (( Mx2Tran MN2) * ( Mx2Tran MN)) by MATRIX_0: 24

        .= ( Mx2Tran (MN * MN2)) by A6, Th32

        .= ( Mx2Tran ( 1. ( F_Real ,m))) by A11, A13, MATRIX14: 18

        .= ( id ( TOP-REAL m)) by Th33;

        ( sqr fm) = (( sqr f) ^ ( sqr mn)) by RVSUM_1: 144;

        

        then ( Sum ( sqr fm)) = (( Sum ( sqr f)) + ( Sum ( sqr mn))) by RVSUM_1: 75

        .= ( Sum ( sqr f)) by A7;

        then

         A15: |.fm.| = |.f.|;

        

         A16: fm is Point of ( TOP-REAL m) by A4, Lm2;

        

        then fm = (( id ( TOP-REAL m)) . fm)

        .= (( Mx2Tran MN1) . Mfm) by A16, A14, A5, FUNCT_1: 12;

        hence thesis by A9, A10, A15;

      end;

        suppose

         A17: n = 0 ;

        

         A18: |.( 0* n).| = 0 by EUCLID: 7;

        take L = jj;

        thus thesis by A17, A18;

      end;

    end;

    theorem :: MATRTOP1:47

    

     Th47: ( Mx2Tran M) is continuous

    proof

      set Tn = ( TOP-REAL n);

      set Tm = ( TOP-REAL m);

      set TM = ( Mx2Tran M);

      consider L be Real such that

       A1: L > 0 and

       A2: for f be n -element real-valued FinSequence holds |.(TM . f).| <= (L * |.f.|) by Th45;

      let x be Point of Tn, U be a_neighborhood of (TM . x);

      reconsider TMx = (TM . x) as Point of Tm;

      reconsider tmx = TMx as Point of ( Euclid m) by EUCLID: 67;

      reconsider X = x as Point of ( Euclid n) by EUCLID: 67;

      tmx in ( Int U) by CONNSP_2:def 1;

      then

      consider r be Real such that

       A3: r > 0 and

       A4: ( Ball (tmx,r)) c= U by GOBOARD6: 5;

      reconsider B = ( Ball (X,(r / L))) as Subset of Tn by EUCLID: 67;

      (r / L) > 0 by A3, A1, XREAL_1: 139;

      then x in ( Int B) by GOBOARD6: 5;

      then

      reconsider Bx = B as a_neighborhood of x by CONNSP_2:def 1;

      take Bx;

      let y be object;

      assume y in (TM .: Bx);

      then

      consider p be object such that p in ( dom TM) and

       A5: p in Bx and

       A6: (TM . p) = y by FUNCT_1:def 6;

      reconsider p as Point of Tn by A5;

      

       A7: ((r / L) * L) = r by A1, XCMPLX_1: 87;

      reconsider TMp = (TM . p) as Point of Tm;

      reconsider tmp = TMp as Point of ( Euclid m) by EUCLID: 67;

      ( dist (tmx,tmp)) = |.((TM . x) - (TM . p)).| by SPPOL_1: 39

      .= |.(TM . (x - p)).| by Th28;

      then

       A8: ( dist (tmx,tmp)) <= (L * |.(x - p).|) by A2;

      reconsider P = p as Point of ( Euclid n) by EUCLID: 67;

      ( dist (X,P)) < (r / L) by A5, METRIC_1: 11;

      then

       A9: (( dist (X,P)) * L) < ((r / L) * L) by A1, XREAL_1: 68;

      ( dist (X,P)) = |.(x - p).| by SPPOL_1: 39;

      then ( dist (tmx,tmp)) < r by A9, A7, A8, XXREAL_0: 2;

      then tmp in ( Ball (tmx,r)) by METRIC_1: 11;

      hence thesis by A4, A6;

    end;

    registration

      let n, K;

      cluster invertible for Matrix of n, K;

      existence

      proof

        ( 1. (K,n)) is invertible;

        hence thesis;

      end;

    end

    registration

      let n;

      let A be invertible Matrix of n, F_Real ;

      cluster ( Mx2Tran A) -> being_homeomorphism;

      coherence

      proof

        set T = ( Mx2Tran A);

        

         A1: (T is continuous) & ( Mx2Tran (A ~ )) is continuous by Th47;

        

         A2: ( Det A) <> ( 0. F_Real ) by LAPLACE: 34;

        then

         A3: (T " ) = ( Mx2Tran (A ~ )) by Th43;

        

         A4: T is onto one-to-one by A2, Th40, Th42;

        then

         A5: ( rng T) = ( [#] ( TOP-REAL n)) by FUNCT_2:def 3;

        ( dom T) = ( [#] ( TOP-REAL n)) & (T /" ) = (T " ) by A4, FUNCT_2:def 1, TOPS_2:def 4;

        hence thesis by A4, A3, A1, A5, TOPS_2:def 5;

      end;

    end