matrprob.miz



    begin

    reserve D for non empty set,

i,j,k for Nat,

n,m for Nat,

r for Real,

e for real-valued FinSequence;

    definition

      let d be set, g be FinSequence of (d * ), n be Nat;

      :: original: .

      redefine

      func g . n -> FinSequence of d ;

      correctness

      proof

        per cases ;

          suppose

           A1: n in ( dom g);

          

           A2: ( rng g) c= (d * ) by FINSEQ_1:def 4;

          (g . n) in ( rng g) by A1, FUNCT_1: 3;

          then (g . n) is Element of (d * ) by A2;

          hence thesis;

        end;

          suppose not n in ( dom g);

          then (g . n) = ( <*> d) by FUNCT_1:def 2;

          hence thesis;

        end;

      end;

    end

    definition

      let x be Real;

      :: original: <*

      redefine

      func <*x*> -> FinSequence of REAL ;

      coherence

      proof

        ( rng <*x*>) c= REAL ;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: MATRPROB:1

    

     Th1: for a be Element of D, m be non zero Nat, g be FinSequence of D holds (( len g) = m & for i be Nat st i in ( dom g) holds (g . i) = a) iff g = (m |-> a)

    proof

      let a be Element of D, m be non zero Nat, g be FinSequence of D;

      hereby

        assume that

         A1: ( len g) = m and

         A2: for i be Nat st i in ( dom g) holds (g . i) = a;

        ( dom g) = ( dom (m |-> a)) & for i be Nat st i in ( dom g) holds (g . i) = ((m |-> a) . i)

        proof

          

          thus ( dom g) = ( Seg m) by A1, FINSEQ_1:def 3

          .= ( dom (m |-> a)) by FUNCOP_1: 13;

          let i be Nat such that

           A3: i in ( dom g);

          

           A4: i in ( Seg m) by A1, A3, FINSEQ_1:def 3;

          

          thus (g . i) = a by A2, A3

          .= ((m |-> a) . i) by A4, FINSEQ_2: 57;

        end;

        hence g = (m |-> a) by FINSEQ_1: 13;

      end;

      assume

       A5: g = (m |-> a);

      then ( dom g) = ( Seg m) by FUNCOP_1: 13;

      hence thesis by A5, CARD_1:def 7, FINSEQ_2: 57;

    end;

    theorem :: MATRPROB:2

    

     Th2: for a,b be Element of D holds ex g be FinSequence of D st ( len g) = n & for i be Nat st i in ( Seg n) holds (i in ( Seg k) implies (g . i) = a) & ( not i in ( Seg k) implies (g . i) = b)

    proof

      let a,b be Element of D;

      defpred c[ object] means $1 in ( Seg k);

      deffunc f( object) = a;

      deffunc g( object) = b;

      ex f be Function st ( dom f) = ( Seg n) & for x be object st x in ( Seg n) holds ( c[x] implies (f . x) = f(x)) & ( not c[x] implies (f . x) = g(x)) from PARTFUN1:sch 1;

      then

      consider f be Function such that

       A1: ( dom f) = ( Seg n) and

       A2: for x be object st x in ( Seg n) holds (x in ( Seg k) implies (f . x) = a) & ( not x in ( Seg k) implies (f . x) = b);

      reconsider p = f as FinSequence by A1, FINSEQ_1:def 2;

      ( rng p) c= D

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider j be object such that

         A3: j in ( dom p) and

         A4: y = (p . j) by FUNCT_1:def 3;

        

         A5: not j in ( Seg k) implies (p . j) = b by A1, A2, A3;

        j in ( Seg k) implies (p . j) = a by A1, A2, A3;

        hence thesis by A4, A5;

      end;

      then

      reconsider p as FinSequence of D by FINSEQ_1:def 4;

      take p;

      n in NAT by ORDINAL1:def 12;

      hence thesis by A1, A2, FINSEQ_1:def 3;

    end;

    theorem :: MATRPROB:3

    

     Th3: (for i be Nat st i in ( dom e) holds 0 <= (e . i)) implies for f be Real_Sequence st (for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1)))) holds for n,m be Nat st n in ( dom e) & m in ( dom e) & n <= m holds (f . n) <= (f . m)

    proof

      assume

       A1: for i be Nat st i in ( dom e) holds 0 <= (e . i);

      let f be Real_Sequence such that

       A2: for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1)));

      

       A3: for n st n <> 0 & n < ( len e) holds (f . n) <= (f . (n + 1))

      proof

        let n such that

         A4: n <> 0 and

         A5: n < ( len e);

        (n + 1) >= 1 & (n + 1) <= ( len e) by A5, NAT_1: 13, NAT_1: 14;

        then (n + 1) in ( dom e) by FINSEQ_3: 25;

        then ((f . n) + (e . (n + 1))) >= (f . n) by A1, XREAL_1: 31;

        hence thesis by A2, A4, A5;

      end;

      for n be Nat st n in ( dom e) holds for m holds m in ( dom e) & n <= m implies (f . n) <= (f . m)

      proof

        let n be Nat;

        assume n in ( dom e);

        then

         A6: n >= 1 by FINSEQ_3: 25;

        defpred p[ Nat] means $1 in ( dom e) & n <= $1 implies (f . $1) >= (f . n);

         A7:

        now

          let k such that

           A8: p[k];

          now

            assume that

             A9: (k + 1) in ( dom e) and

             A10: n <= (k + 1);

            

             A11: (k + 1) <= ( len e) by A9, FINSEQ_3: 25;

            per cases by A10, A11, NAT_1: 8, NAT_1: 13;

              suppose (k + 1) = n & k < ( len e);

              hence (f . (k + 1)) >= (f . n);

            end;

              suppose

               A12: k >= n & k < ( len e);

              then k >= 1 & (f . (k + 1)) >= (f . k) by A3, A6, NAT_1: 14;

              hence (f . (k + 1)) >= (f . n) by A8, A12, FINSEQ_3: 25, XXREAL_0: 2;

            end;

          end;

          hence p[(k + 1)];

        end;

        

         A13: p[ 0 ];

        for n be Nat holds p[n] from NAT_1:sch 2( A13, A7);

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MATRPROB:4

    

     Th4: ( len e) >= 1 & (for i be Nat st i in ( dom e) holds 0 <= (e . i)) implies for f be Real_Sequence st (f . 1) = (e . 1) & (for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1)))) holds for n be Nat st n in ( dom e) holds (e . n) <= (f . n)

    proof

      assume that

       A1: ( len e) >= 1 and

       A2: for i be Nat st i in ( dom e) holds 0 <= (e . i);

      let f be Real_Sequence such that

       A3: (f . 1) = (e . 1) and

       A4: for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1)));

      defpred p[ Nat] means $1 in ( dom e) implies (e . $1) <= (f . $1);

       A5:

      now

        let k be Nat such that p[k];

        now

          assume (k + 1) in ( dom e);

          then

           A6: (k + 1) <= ( len e) by FINSEQ_3: 25;

          per cases by A6, NAT_1: 13;

            suppose k = 0 & k < ( len e);

            hence (e . (k + 1)) <= (f . (k + 1)) by A3;

          end;

            suppose

             A7: k > 0 & k < ( len e);

            then 1 <= ( len e) by NAT_1: 14;

            then

             A8: 1 in ( dom e) by FINSEQ_3: 25;

            

             A9: 1 in ( dom e) by A1, FINSEQ_3: 25;

            

             A10: k >= 1 by A7, NAT_1: 14;

            then k in ( dom e) by A7, FINSEQ_3: 25;

            then (e . 1) <= (f . k) by A2, A3, A4, A10, A8, Th3;

            then (f . k) >= 0 by A2, A9;

            then ((f . k) + (e . (k + 1))) >= (e . (k + 1)) by XREAL_1: 31;

            hence (e . (k + 1)) <= (f . (k + 1)) by A4, A7;

          end;

        end;

        hence p[(k + 1)];

      end;

      

       A11: p[ 0 ] by FINSEQ_3: 25;

      for n holds p[n] from NAT_1:sch 2( A11, A5);

      hence thesis;

    end;

    theorem :: MATRPROB:5

    

     Th5: (for i be Nat st i in ( dom e) holds 0 <= (e . i)) implies for k be Nat st k in ( dom e) holds (e . k) <= ( Sum e)

    proof

      assume

       A1: for i be Nat st i in ( dom e) holds 0 <= (e . i);

      per cases ;

        suppose ( len e) = 0 ;

        then e = {} ;

        hence thesis;

      end;

        suppose

         A2: ( len e) <> 0 ;

        then ( len e) >= 1 by NAT_1: 14;

        then

         A3: ( len e) in ( dom e) by FINSEQ_3: 25;

        let n be Nat;

        assume

         A4: n in ( dom e);

        reconsider n as Nat;

        e is FinSequence of REAL by RVSUM_1: 145;

        then

        consider f be Real_Sequence such that

         A5: (f . 1) = (e . 1) and

         A6: for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1))) and

         A7: ( Sum e) = (f . ( len e)) by A2, NAT_1: 14, PROB_3: 63;

        

         A8: (e . n) <= (f . n) by A1, A2, A5, A6, A4, Th4, NAT_1: 14;

        n <= ( len e) by A4, FINSEQ_3: 25;

        then (f . n) <= (f . ( len e)) by A1, A6, A4, A3, Th3;

        hence thesis by A7, A8, XXREAL_0: 2;

      end;

    end;

    theorem :: MATRPROB:6

    

     Th6: for r1,r2 be Real, k be Nat, seq1 be Real_Sequence holds ex seq be Real_Sequence st (seq . 0 ) = r1 & for n holds (n <> 0 & n <= k implies (seq . n) = (seq1 . n)) & (n > k implies (seq . n) = r2)

    proof

      let r1,r2 be Real, k be Nat, seq1 be Real_Sequence;

      ex seq be Real_Sequence st for n holds (n = 0 implies (seq . n) = r1) & (n <> 0 & n <= k implies (seq . n) = (seq1 . n)) & (n <> 0 & n > k implies (seq . n) = r2)

      proof

        defpred P[ object, object] means ex n be Nat st (n = $1 & (n = 0 implies $2 = r1) & (n <> 0 & n <= k implies $2 = (seq1 . n)) & (n <> 0 & n > k implies $2 = r2));

        

         A1: for x be object st x in NAT holds ex y be object st P[x, y]

        proof

          let x be object;

          assume x in NAT ;

          then

          reconsider n = x as Nat;

          now

            per cases ;

              case n = 0 ;

              hence P[x, r1];

            end;

              case n <> 0 & n <= k;

              hence P[x, (seq1 . n)];

            end;

              case n <> 0 & not n <= k;

              hence P[x, r2];

            end;

          end;

          hence thesis;

        end;

        consider f1 be Function such that

         A2: ( dom f1) = NAT & for x be object st x in NAT holds P[x, (f1 . x)] from CLASSES1:sch 1( A1);

        now

          let x be object;

          assume x in NAT ;

          then ex n be Nat st n = x & (n = 0 implies (f1 . x) = r1) & (n <> 0 & n <= k implies (f1 . x) = (seq1 . n)) & (n <> 0 & n > k implies (f1 . x) = r2) by A2;

          hence (f1 . x) is real;

        end;

        then

        reconsider f1 as Real_Sequence by A2, SEQ_1: 1;

        take seq = f1;

        let n be Nat;

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

        ex k1 be Nat st k1 = n & (k1 = 0 implies (seq . n) = r1) & (k1 <> 0 & k1 <= k implies (seq . n) = (seq1 . k1)) & (k1 <> 0 & k1 > k implies (seq . n) = r2) by A2;

        hence thesis;

      end;

      then

      consider seq be Real_Sequence such that

       A3: for n holds (n = 0 implies (seq . n) = r1) & (n <> 0 & n <= k implies (seq . n) = (seq1 . n)) & (n <> 0 & n > k implies (seq . n) = r2);

      take seq;

      thus thesis by A3;

    end;

    theorem :: MATRPROB:7

    

     Th7: for F be FinSequence of REAL holds ex f be Real_Sequence st (f . 0 ) = 0 & (for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1)))) & ( Sum F) = (f . ( len F))

    proof

      let F be FinSequence of REAL ;

      per cases ;

        suppose

         A1: ( len F) = 0 ;

        set f = ( seq_const 0 );

        

         A2: for i be Nat st i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) by A1;

        

         A3: for i be Nat holds (f . i) = 0 by SEQ_1: 57;

        then

         A4: (f . 0 ) = 0 ;

        ( Sum F) = 0 by A1, PROB_3: 62

        .= (f . ( len F)) by A3;

        hence thesis by A2, A4;

      end;

        suppose

         A5: ( len F) > 0 ;

        then

        consider f be Real_Sequence such that

         A6: (f . 1) = (F . 1) and

         A7: for i be Nat st 0 <> i & i < ( len F) holds (f . (i + 1)) = ((f . i) + (F . (i + 1))) and

         A8: ( Sum F) = (f . ( len F)) by NAT_1: 14, PROB_3: 63;

        consider f1 be Real_Sequence such that

         A9: for n holds (f1 . 0 ) = 0 & (n <> 0 & n <= ( len F) implies (f1 . n) = (f . n)) & (n > ( len F) implies (f1 . n) = 0 ) by Th6;

        

         A10: ( len F) >= 1 by A5, NAT_1: 14;

        

         A11: for i be Nat st i < ( len F) holds (f1 . (i + 1)) = ((f1 . i) + (F . (i + 1)))

        proof

          let i be Nat such that

           A12: i < ( len F);

          set r = (F . (i + 1));

          per cases ;

            suppose i = 0 ;

            hence thesis by A10, A6, A9;

          end;

            suppose

             A13: i <> 0 ;

            (i + 1) <= ( len F) by A12, NAT_1: 13;

            

            hence (f1 . (i + 1)) = (f . (i + 1)) by A9

            .= ((f . i) + (F . (i + 1))) by A7, A12, A13

            .= ((f1 . i) + r) by A9, A12, A13;

          end;

        end;

        ( Sum F) = (f1 . ( len F)) by A5, A8, A9;

        hence thesis by A9, A11;

      end;

    end;

    theorem :: MATRPROB:8

    

     Th8: for D be set, e1 be FinSequence of D holds (n |-> e1) is FinSequence of (D * )

    proof

      let D be set, e1 be FinSequence of D;

      e1 in (D * ) by FINSEQ_1:def 11;

      hence thesis by FINSEQ_2: 63;

    end;

    theorem :: MATRPROB:9

    

     Th9: for D be set, e1,e2 be FinSequence of D holds ex e be FinSequence of (D * ) st ( len e) = n & for i be Nat st i in ( Seg n) holds (i in ( Seg k) implies (e . i) = e1) & ( not i in ( Seg k) implies (e . i) = e2)

    proof

      let D be set, e1,e2 be FinSequence of D;

      e1 in (D * ) & e2 in (D * ) by FINSEQ_1:def 11;

      hence thesis by Th2;

    end;

    theorem :: MATRPROB:10

    

     Th10: for D be set, s be FinSequence holds (s is Matrix of D iff ex n st for i st i in ( dom s) holds ex p be FinSequence of D st (s . i) = p & ( len p) = n)

    proof

      let D be set, s be FinSequence;

      thus s is Matrix of D implies ex n st for i st i in ( dom s) holds ex p be FinSequence of D st (s . i) = p & ( len p) = n

      proof

        assume

         A1: s is Matrix of D;

        then

        reconsider v = s as FinSequence of (D * );

        consider n be Nat such that

         A2: for x be object st x in ( rng v) holds ex t be FinSequence st t = x & ( len t) = n by A1, MATRIX_0:def 1;

        

         A3: for i st i in ( dom v) holds ex p be FinSequence of D st (v . i) = p & ( len p) = n

        proof

          let i;

          assume i in ( dom v);

          then

          consider t be FinSequence such that

           A4: t = (v . i) & ( len t) = n by A2, FUNCT_1: 3;

          take t;

          thus thesis by A4;

        end;

        reconsider n as Nat;

        take n;

        thus thesis by A3;

      end;

      given n such that

       A5: for i st i in ( dom s) holds ex p be FinSequence of D st (s . i) = p & ( len p) = n;

      

       A6: for x be set st x in ( rng s) holds (ex v be FinSequence st v = x & ( len v) = n) & x in (D * )

      proof

        let x be set;

        assume x in ( rng s);

        then

        consider i be object such that

         A7: i in ( dom s) and

         A8: x = (s . i) by FUNCT_1:def 3;

        

         A9: ex p be FinSequence of D st (s . i) = p & ( len p) = n by A5, A7;

        hence ex v be FinSequence st v = x & ( len v) = n by A8;

        thus thesis by A8, A9, FINSEQ_1:def 11;

      end;

      then for x be object st x in ( rng s) holds x in (D * );

      then

       A10: ( rng s) c= (D * );

      for x be object st x in ( rng s) holds ex v be FinSequence st v = x & ( len v) = n by A6;

      hence thesis by A10, FINSEQ_1:def 4, MATRIX_0:def 1;

    end;

    theorem :: MATRPROB:11

    

     Th11: for D be set, e be FinSequence of (D * ) holds (ex n st for i st i in ( dom e) holds ( len (e . i)) = n) iff e is Matrix of D

    proof

      let D be set, e be FinSequence of (D * );

      hereby

        given n such that

         A1: for i st i in ( dom e) holds ( len (e . i)) = n;

        for i st i in ( dom e) holds ex p be FinSequence of D st (e . i) = p & ( len p) = n

        proof

          let i;

          assume i in ( dom e);

          then ( len (e . i)) = n by A1;

          hence thesis;

        end;

        hence e is Matrix of D by Th10;

      end;

      assume e is Matrix of D;

      then

      consider n such that

       A2: for i st i in ( dom e) holds ex p be FinSequence of D st (e . i) = p & ( len p) = n by Th10;

      for i st i in ( dom e) holds ( len (e . i)) = n

      proof

        let i;

        assume i in ( dom e);

        then ex p be FinSequence of D st (e . i) = p & ( len p) = n by A2;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: MATRPROB:12

    

     Th12: for M be tabular FinSequence holds [i, j] in ( Indices M) iff i in ( Seg ( len M)) & j in ( Seg ( width M))

    proof

      let M be tabular FinSequence;

      hereby

        assume [i, j] in ( Indices M);

        then

         A1: [i, j] in [:( dom M), ( Seg ( width M)):] by MATRIX_0:def 4;

        then i in ( dom M) by ZFMISC_1: 87;

        hence i in ( Seg ( len M)) & j in ( Seg ( width M)) by A1, FINSEQ_1:def 3, ZFMISC_1: 87;

      end;

      assume that

       A2: i in ( Seg ( len M)) and

       A3: j in ( Seg ( width M));

      i in ( dom M) by A2, FINSEQ_1:def 3;

      then [i, j] in [:( dom M), ( Seg ( width M)):] by A3, ZFMISC_1: 87;

      hence thesis by MATRIX_0:def 4;

    end;

    theorem :: MATRPROB:13

    

     Th13: for D be non empty set, M be Matrix of D holds [i, j] in ( Indices M) iff i in ( dom M) & j in ( dom (M . i))

    proof

      let D be non empty set, M be Matrix of D;

      hereby

        assume

         A1: [i, j] in ( Indices M);

        then

         A2: j in ( Seg ( width M)) by Th12;

        

         A3: i in ( Seg ( len M)) by A1, Th12;

        then i in ( dom M) by FINSEQ_1:def 3;

        then j in ( Seg ( len (M . i))) by A2, MATRIX_0: 36;

        hence i in ( dom M) & j in ( dom (M . i)) by A3, FINSEQ_1:def 3;

      end;

      assume i in ( dom M) & j in ( dom (M . i));

      hence thesis by MATRIX_0: 37;

    end;

    theorem :: MATRPROB:14

    

     Th14: for D be non empty set, M be Matrix of D st [i, j] in ( Indices M) holds (M * (i,j)) = ((M . i) . j)

    proof

      let D be non empty set, M be Matrix of D;

      assume [i, j] in ( Indices M);

      then ex p be FinSequence of D st p = (M . i) & (M * (i,j)) = (p . j) by MATRIX_0:def 5;

      hence thesis;

    end;

    theorem :: MATRPROB:15

    

     Th15: for D be non empty set, M be Matrix of D holds [i, j] in ( Indices M) iff i in ( dom ( Col (M,j))) & j in ( dom ( Line (M,i)))

    proof

      let D be non empty set, M be Matrix of D;

      hereby

        assume

         A1: [i, j] in ( Indices M);

        then

         A2: i in ( dom M) by Th13;

        then i in ( Seg ( len M)) by FINSEQ_1:def 3;

        then i in ( Seg ( len ( Col (M,j)))) by MATRIX_0:def 8;

        hence i in ( dom ( Col (M,j))) by FINSEQ_1:def 3;

        j in ( dom (M . i)) by A1, Th13;

        hence j in ( dom ( Line (M,i))) by A2, MATRIX_0: 60;

      end;

      assume that

       A3: i in ( dom ( Col (M,j))) and

       A4: j in ( dom ( Line (M,i)));

      i in ( Seg ( len ( Col (M,j)))) by A3, FINSEQ_1:def 3;

      then i in ( Seg ( len M)) by MATRIX_0:def 8;

      then

       A5: i in ( dom M) by FINSEQ_1:def 3;

      then j in ( dom (M . i)) by A4, MATRIX_0: 60;

      hence thesis by A5, Th13;

    end;

    theorem :: MATRPROB:16

    

     Th16: for D1,D2 be non empty set, M1 be Matrix of D1, M2 be Matrix of D2 st M1 = M2 holds for i st i in ( dom M1) holds ( Line (M1,i)) = ( Line (M2,i))

    proof

      let D1,D2 be non empty set, M1 be Matrix of D1, M2 be Matrix of D2 such that

       A1: M1 = M2;

      hereby

        let i;

        assume

         A2: i in ( dom M1);

        then ( Line (M1,i)) = (M1 . i) by MATRIX_0: 60;

        hence ( Line (M1,i)) = ( Line (M2,i)) by A1, A2, MATRIX_0: 60;

      end;

    end;

    theorem :: MATRPROB:17

    

     Th17: for D1,D2 be non empty set, M1 be Matrix of D1, M2 be Matrix of D2 st M1 = M2 holds for j st j in ( Seg ( width M1)) holds ( Col (M1,j)) = ( Col (M2,j))

    proof

      let D1,D2 be non empty set, M1 be Matrix of D1, M2 be Matrix of D2 such that

       A1: M1 = M2;

      hereby

        let j such that

         A2: j in ( Seg ( width M1));

        

         A3: for k be Nat st k in ( dom ( Col (M1,j))) holds (( Col (M1,j)) . k) = (( Col (M2,j)) . k)

        proof

          let k be Nat;

          assume k in ( dom ( Col (M1,j)));

          then k in ( Seg ( len ( Col (M1,j)))) by FINSEQ_1:def 3;

          then

           A4: k in ( Seg ( len M1)) by MATRIX_0:def 8;

          then

           A5: [k, j] in ( Indices M1) by A2, Th12;

          

           A6: k in ( dom M1) by A4, FINSEQ_1:def 3;

          

          hence (( Col (M1,j)) . k) = (M1 * (k,j)) by MATRIX_0:def 8

          .= (M2 * (k,j)) by A1, A5, MATRIXR1: 23

          .= (( Col (M2,j)) . k) by A1, A6, MATRIX_0:def 8;

        end;

        ( dom ( Col (M1,j))) = ( Seg ( len ( Col (M1,j)))) by FINSEQ_1:def 3

        .= ( Seg ( len M1)) by MATRIX_0:def 8

        .= ( Seg ( len ( Col (M2,j)))) by A1, MATRIX_0:def 8

        .= ( dom ( Col (M2,j))) by FINSEQ_1:def 3;

        hence ( Col (M1,j)) = ( Col (M2,j)) by A3, FINSEQ_1: 13;

      end;

    end;

    theorem :: MATRPROB:18

    

     Th18: for e1 be FinSequence of D st ( len e1) = m holds (n |-> e1) is Matrix of n, m, D

    proof

      let e1 be FinSequence of D such that

       A1: ( len e1) = m;

      reconsider e = (n |-> e1) as FinSequence of (D * ) by Th8;

      

       A2: ( len e) = n by CARD_1:def 7;

      

       A3: for i st i in ( dom e) holds ( len (e . i)) = m

      proof

        let i;

        assume i in ( dom e);

        then i in ( Seg n) by A2, FINSEQ_1:def 3;

        hence thesis by A1, FUNCOP_1: 7;

      end;

      then

      reconsider e as Matrix of D by Th11;

      for p be FinSequence of D st p in ( rng e) holds ( len p) = m

      proof

        let p be FinSequence of D;

        assume p in ( rng e);

        then ex i be object st i in ( dom e) & p = (e . i) by FUNCT_1:def 3;

        hence thesis by A3;

      end;

      hence thesis by A2, MATRIX_0:def 2;

    end;

    theorem :: MATRPROB:19

    

     Th19: for e1,e2 be FinSequence of D st ( len e1) = m & ( len e2) = m holds ex M be Matrix of n, m, D st for i be Nat st i in ( Seg n) holds (i in ( Seg k) implies (M . i) = e1) & ( not i in ( Seg k) implies (M . i) = e2)

    proof

      let e1,e2 be FinSequence of D such that

       A1: ( len e1) = m & ( len e2) = m;

      consider e be FinSequence of (D * ) such that

       A2: ( len e) = n and

       A3: for i be Nat st i in ( Seg n) holds (i in ( Seg k) implies (e . i) = e1) & ( not i in ( Seg k) implies (e . i) = e2) by Th9;

      

       A4: for i st i in ( dom e) holds ( len (e . i)) = m

      proof

        let i;

        assume i in ( dom e);

        then i in ( Seg n) by A2, FINSEQ_1:def 3;

        hence thesis by A1, A3;

      end;

      then

      reconsider e as Matrix of D by Th11;

      for p be FinSequence of D st p in ( rng e) holds ( len p) = m

      proof

        let p be FinSequence of D;

        assume p in ( rng e);

        then ex i be object st i in ( dom e) & p = (e . i) by FUNCT_1:def 3;

        hence thesis by A4;

      end;

      then e is Matrix of n, m, D by A2, MATRIX_0:def 2;

      hence thesis by A3;

    end;

    

     Lm1: for m be Matrix of REAL holds (for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r) iff for i, j st i in ( dom m) & j in ( dom (m . i)) holds ((m . i) . j) >= r

    proof

      let m be Matrix of REAL ;

      hereby

        assume

         A1: for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r;

        hereby

          let i, j;

          assume i in ( dom m) & j in ( dom (m . i));

          then

           A2: [i, j] in ( Indices m) by Th13;

          then (m * (i,j)) >= r by A1;

          hence ((m . i) . j) >= r by A2, Th14;

        end;

      end;

      assume

       A3: for i, j st i in ( dom m) & j in ( dom (m . i)) holds ((m . i) . j) >= r;

      hereby

        let i, j such that

         A4: [i, j] in ( Indices m);

        i in ( dom m) & j in ( dom (m . i)) by A4, Th13;

        then ((m . i) . j) >= r by A3;

        hence (m * (i,j)) >= r by A4, Th14;

      end;

    end;

    

     Lm2: for m be Matrix of REAL holds (for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r) iff for i, j st i in ( dom m) & j in ( dom ( Line (m,i))) holds (( Line (m,i)) . j) >= r

    proof

      let m be Matrix of REAL ;

      hereby

        assume

         A1: for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r;

        hereby

          let i, j such that

           A2: i in ( dom m) and

           A3: j in ( dom ( Line (m,i)));

          (m . i) = ( Line (m,i)) by A2, MATRIX_0: 60;

          hence (( Line (m,i)) . j) >= r by A1, A2, A3, Lm1;

        end;

      end;

      assume

       A4: for i, j st i in ( dom m) & j in ( dom ( Line (m,i))) holds (( Line (m,i)) . j) >= r;

      now

        let i such that

         A5: i in ( dom m);

        (m . i) = ( Line (m,i)) by A5, MATRIX_0: 60;

        hence for j st j in ( dom (m . i)) holds ((m . i) . j) >= r by A4, A5;

      end;

      then for i, j st i in ( dom m) & j in ( dom (m . i)) holds ((m . i) . j) >= r;

      hence thesis by Lm1;

    end;

    

     Lm3: for m be Matrix of REAL holds (for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r) iff for i, j st j in ( Seg ( width m)) & i in ( dom ( Col (m,j))) holds (( Col (m,j)) . i) >= r

    proof

      let m be Matrix of REAL ;

      hereby

        assume

         A1: for i, j st [i, j] in ( Indices m) holds (m * (i,j)) >= r;

        hereby

          let i, j such that

           A2: j in ( Seg ( width m)) and

           A3: i in ( dom ( Col (m,j)));

          j in ( Seg ( len ( Line (m,i)))) by A2, MATRIX_0:def 7;

          then

           A4: j in ( dom ( Line (m,i))) by FINSEQ_1:def 3;

          then [i, j] in ( Indices m) by A3, Th15;

          then

           A5: i in ( dom m) by Th13;

          then (( Line (m,i)) . j) >= r by A1, A4, Lm2;

          hence (( Col (m,j)) . i) >= r by A2, A5, MATRIX_0: 42;

        end;

      end;

      assume

       A6: for i, j st j in ( Seg ( width m)) & i in ( dom ( Col (m,j))) holds (( Col (m,j)) . i) >= r;

      for i, j st i in ( dom m) & j in ( dom ( Line (m,i))) holds (( Line (m,i)) . j) >= r

      proof

        let i, j such that

         A7: i in ( dom m) and

         A8: j in ( dom ( Line (m,i)));

        j in ( Seg ( len ( Line (m,i)))) by A8, FINSEQ_1:def 3;

        then

         A9: j in ( Seg ( width m)) by MATRIX_0:def 7;

        i in ( Seg ( len m)) by A7, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Col (m,j)))) by MATRIX_0:def 8;

        then i in ( dom ( Col (m,j))) by FINSEQ_1:def 3;

        then (( Col (m,j)) . i) >= r by A6, A9;

        hence thesis by A7, A9, MATRIX_0: 42;

      end;

      hence thesis by Lm2;

    end;

    definition

      let e be FinSequence of ( REAL * );

      :: MATRPROB:def1

      func Sum e -> FinSequence of REAL means

      : Def1: ( len it ) = ( len e) & for k st k in ( dom it ) holds (it . k) = ( Sum (e . k));

      existence

      proof

        deffunc f( Nat) = ( In (( Sum (e . $1)), REAL ));

        consider e1 be FinSequence of REAL such that

         A1: ( len e1) = ( len e) & for k be Nat st k in ( dom e1) holds (e1 . k) = f(k) from FINSEQ_2:sch 1;

        take e1;

        thus ( len e1) = ( len e) by A1;

        let k;

        assume k in ( dom e1);

        then (e1 . k) = f(k) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let e1,e2 be FinSequence of REAL such that

         A2: ( len e1) = ( len e) and

         A3: for k st k in ( dom e1) holds (e1 . k) = ( Sum (e . k)) and

         A4: ( len e2) = ( len e) and

         A5: for k st k in ( dom e2) holds (e2 . k) = ( Sum (e . k));

        ( dom e1) = ( dom e2) & for k be Nat st k in ( dom e1) holds (e1 . k) = (e2 . k)

        proof

          

          thus

           A6: ( dom e1) = ( Seg ( len e)) by A2, FINSEQ_1:def 3

          .= ( dom e2) by A4, FINSEQ_1:def 3;

          let k be Nat such that

           A7: k in ( dom e1);

          

          thus (e1 . k) = ( Sum (e . k)) by A3, A7

          .= (e2 . k) by A5, A6, A7;

        end;

        hence thesis by FINSEQ_1: 13;

      end;

    end

    notation

      let m be Matrix of REAL ;

      synonym LineSum m for Sum m;

    end

    theorem :: MATRPROB:20

    

     Th20: for m be Matrix of REAL holds ( len ( Sum m)) = ( len m) & for i st i in ( Seg ( len m)) holds (( Sum m) . i) = ( Sum ( Line (m,i)))

    proof

      let m be Matrix of REAL ;

      thus ( len ( Sum m)) = ( len m) by Def1;

      thus for k st k in ( Seg ( len m)) holds (( Sum m) . k) = ( Sum ( Line (m,k)))

      proof

        let k such that

         A1: k in ( Seg ( len m));

        

         A2: k in ( dom m) by A1, FINSEQ_1:def 3;

        k in ( Seg ( len ( Sum m))) by A1, Def1;

        then k in ( dom ( Sum m)) by FINSEQ_1:def 3;

        

        hence (( Sum m) . k) = ( Sum (m . k)) by Def1

        .= ( Sum ( Line (m,k))) by A2, MATRIX_0: 60;

      end;

    end;

    definition

      let m be Matrix of REAL ;

      :: MATRPROB:def2

      func ColSum m -> FinSequence of REAL means

      : Def2: ( len it ) = ( width m) & for j be Nat st j in ( Seg ( width m)) holds (it . j) = ( Sum ( Col (m,j)));

      existence

      proof

        deffunc f( Nat) = ( In (( Sum ( Col (m,$1))), REAL ));

        consider e be FinSequence of REAL such that

         A1: ( len e) = ( width m) & for k be Nat st k in ( dom e) holds (e . k) = f(k) from FINSEQ_2:sch 1;

        take e;

        thus ( len e) = ( width m) by A1;

        let k be Nat such that

         A2: k in ( Seg ( width m));

        ( dom e) = ( Seg ( width m)) by A1, FINSEQ_1:def 3;

        then (e . k) = f(k) by A2, A1;

        hence thesis;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL such that

         A3: ( len p1) = ( width m) and

         A4: for i be Nat st i in ( Seg ( width m)) holds (p1 . i) = ( Sum ( Col (m,i))) and

         A5: ( len p2) = ( width m) and

         A6: for i be Nat st i in ( Seg ( width m)) holds (p2 . i) = ( Sum ( Col (m,i)));

        

         A7: ( dom p1) = ( Seg ( width m)) by A3, FINSEQ_1:def 3;

        for j be Nat st j in ( dom p1) holds (p1 . j) = (p2 . j)

        proof

          let j be Nat;

          assume

           A8: j in ( dom p1);

          then (p1 . j) = ( Sum ( Col (m,j))) by A4, A7;

          hence thesis by A6, A7, A8;

        end;

        hence thesis by A3, A5, FINSEQ_2: 9;

      end;

    end

    theorem :: MATRPROB:21

    for M be Matrix of REAL st ( width M) > 0 holds ( LineSum M) = ( ColSum (M @ ))

    proof

      let M be Matrix of REAL ;

      assume ( width M) > 0 ;

      then

       A1: ( len M) = ( width (M @ )) by MATRIX_0: 54;

      

       A2: ( len ( LineSum M)) = ( len M) by Th20;

      

       A3: ( len ( ColSum (M @ ))) = ( width (M @ )) by Def2;

       A4:

      now

        let i be Nat;

        assume that

         A5: 1 <= i and

         A6: i <= ( len ( ColSum (M @ )));

        i <= ( len ( LineSum M)) by A2, A1, A6, Def2;

        then i in ( Seg ( len ( LineSum M))) by A5;

        then

         A7: i in ( Seg ( len M)) by Th20;

        then

         A8: i in ( dom M) by FINSEQ_1:def 3;

        i in ( Seg ( width (M @ ))) by A3, A5, A6;

        

        hence (( ColSum (M @ )) . i) = ( Sum ( Col ((M @ ),i))) by Def2

        .= ( Sum ( Line (M,i))) by A8, MATRIX_0: 58

        .= (( LineSum M) . i) by A7, Th20;

      end;

      ( len ( ColSum (M @ ))) = ( len ( LineSum M)) by A2, A1, Def2;

      hence thesis by A4;

    end;

    theorem :: MATRPROB:22

    

     Th22: for M be Matrix of REAL holds ( ColSum M) = ( LineSum (M @ ))

    proof

      let M be Matrix of REAL ;

      

       A1: ( len ( ColSum M)) = ( width M) by Def2;

      

       A2: ( len ( LineSum (M @ ))) = ( len (M @ )) by Th20;

       A3:

      now

        let i be Nat;

        assume that

         A4: 1 <= i and

         A5: i <= ( len ( ColSum M));

        i <= ( len ( LineSum (M @ ))) by A2, A1, A5, MATRIX_0:def 6;

        then i in ( Seg ( len ( LineSum (M @ )))) by A4;

        then

         A6: i in ( Seg ( len (M @ ))) by Th20;

        

         A7: i in ( Seg ( width M)) by A1, A4, A5;

        

        hence (( ColSum M) . i) = ( Sum ( Col (M,i))) by Def2

        .= ( Sum ( Line ((M @ ),i))) by A7, MATRIX_0: 59

        .= (( LineSum (M @ )) . i) by A6, Th20;

      end;

      ( len ( ColSum M)) = ( len ( LineSum (M @ ))) by A2, A1, MATRIX_0:def 6;

      hence thesis by A3;

    end;

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def3

      func SumAll M -> Real equals ( Sum ( Sum M));

      coherence ;

    end

    theorem :: MATRPROB:23

    

     Th23: for M be Matrix of REAL st ( len M) = 0 holds ( SumAll M) = 0

    proof

      let M be Matrix of REAL ;

      assume ( len M) = 0 ;

      then ( len ( Sum M)) = 0 by Def1;

      then ( Sum M) = ( <*> REAL );

      hence thesis by RVSUM_1: 72;

    end;

    

     Lm4: 0 in REAL by XREAL_0:def 1;

    theorem :: MATRPROB:24

    

     Th24: for M be Matrix of m, 0 , REAL holds ( SumAll M) = 0

    proof

      let M be Matrix of m, 0 , REAL ;

      per cases ;

        suppose m = 0 ;

        then ( len M) = 0 by MATRIX_0:def 2;

        hence thesis by Th23;

      end;

        suppose

         A1: m > 0 ;

        ( len ( Sum M)) > 0 & for k be Nat st k in ( dom ( Sum M)) holds (( Sum M) . k) = 0

        proof

          ( len M) > 0 by A1, MATRIX_0:def 2;

          hence ( len ( Sum M)) > 0 by Def1;

          ( len M) = ( len ( Sum M)) by Def1;

          then

           A2: ( dom M) = ( dom ( Sum M)) by FINSEQ_3: 29;

          hereby

            let k be Nat such that

             A3: k in ( dom ( Sum M));

            (M . k) in ( rng M) by A2, A3, FUNCT_1:def 3;

            then ( len (M . k)) = 0 by MATRIX_0:def 2;

            then

             A4: (M . k) = ( <*> REAL );

            

            thus (( Sum M) . k) = ( Sum (M . k)) by A3, Def1

            .= 0 by A4, RVSUM_1: 72;

          end;

        end;

        

        hence ( SumAll M) = ( Sum (( len ( Sum M)) |-> 0 )) by Th1, Lm4

        .= (( len ( Sum M)) * 0 ) by RVSUM_1: 80

        .= 0 ;

      end;

    end;

    theorem :: MATRPROB:25

    

     Th25: for M1 be Matrix of n, k, REAL holds for M2 be Matrix of m, k, REAL holds ( Sum (M1 ^ M2)) = (( Sum M1) ^ ( Sum M2))

    proof

      let M1 be Matrix of n, k, REAL ;

      let M2 be Matrix of m, k, REAL ;

      

       A1: ( dom ( Sum (M1 ^ M2))) = ( Seg ( len ( Sum (M1 ^ M2)))) by FINSEQ_1:def 3;

       A2:

      now

        let i be Nat;

        assume

         A3: i in ( dom ( Sum (M1 ^ M2)));

        then i in ( Seg ( len (M1 ^ M2))) by A1, Def1;

        then

         A4: i in ( dom (M1 ^ M2)) by FINSEQ_1:def 3;

        now

          per cases by A4, FINSEQ_1: 25;

            suppose

             A5: i in ( dom M1);

            ( len M1) = ( len ( Sum M1)) by Def1;

            then

             A6: ( dom M1) = ( dom ( Sum M1)) by FINSEQ_3: 29;

            

            thus (( Sum (M1 ^ M2)) . i) = ( Sum ((M1 ^ M2) . i)) by A3, Def1

            .= ( Sum (M1 . i)) by A5, FINSEQ_1:def 7

            .= (( Sum M1) . i) by A5, A6, Def1

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A5, A6, FINSEQ_1:def 7;

          end;

            suppose

             A7: ex n be Nat st n in ( dom M2) & i = (( len M1) + n);

            

             A8: ( len M1) = ( len ( Sum M1)) by Def1;

            ( len M2) = ( len ( Sum M2)) by Def1;

            then

             A9: ( dom M2) = ( dom ( Sum M2)) by FINSEQ_3: 29;

            consider n be Nat such that

             A10: n in ( dom M2) and

             A11: i = (( len M1) + n) by A7;

            

            thus (( Sum (M1 ^ M2)) . i) = ( Sum ((M1 ^ M2) . i)) by A3, Def1

            .= ( Sum (M2 . n)) by A10, A11, FINSEQ_1:def 7

            .= (( Sum M2) . n) by A10, A9, Def1

            .= ((( Sum M1) ^ ( Sum M2)) . i) by A10, A11, A8, A9, FINSEQ_1:def 7;

          end;

        end;

        hence (( Sum (M1 ^ M2)) . i) = ((( Sum M1) ^ ( Sum M2)) . i);

      end;

      ( len ( Sum (M1 ^ M2))) = ( len (M1 ^ M2)) by Def1

      .= (( len M1) + ( len M2)) by FINSEQ_1: 22

      .= (( len ( Sum M1)) + ( len M2)) by Def1

      .= (( len ( Sum M1)) + ( len ( Sum M2))) by Def1

      .= ( len (( Sum M1) ^ ( Sum M2))) by FINSEQ_1: 22;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: MATRPROB:26

    

     Th26: for M1,M2 be Matrix of REAL holds (( Sum M1) + ( Sum M2)) = ( Sum (M1 ^^ M2))

    proof

      let M1,M2 be Matrix of REAL ;

      reconsider M = ( min (( len M1),( len M2))) as Nat;

      

       A1: ( Seg M) = (( Seg ( len M1)) /\ ( Seg ( len M2))) by FINSEQ_2: 2

      .= (( Seg ( len M1)) /\ ( dom M2)) by FINSEQ_1:def 3

      .= (( dom M1) /\ ( dom M2)) by FINSEQ_1:def 3

      .= ( dom (M1 ^^ M2)) by PRE_POLY:def 4

      .= ( Seg ( len (M1 ^^ M2))) by FINSEQ_1:def 3;

      

       A2: ( len (( Sum M1) + ( Sum M2))) = ( len ( addreal .: (( Sum M1),( Sum M2))))

      .= ( min (( len ( Sum M1)),( len ( Sum M2)))) by FINSEQ_2: 71

      .= ( min (( len M1),( len ( Sum M2)))) by Def1

      .= ( min (( len M1),( len M2))) by Def1

      .= ( len (M1 ^^ M2)) by A1, FINSEQ_1: 6

      .= ( len ( Sum (M1 ^^ M2))) by Def1;

      

       A3: ( dom (( Sum M1) + ( Sum M2))) = ( Seg ( len (( Sum M1) + ( Sum M2)))) by FINSEQ_1:def 3;

      now

        let i be Nat;

        assume

         A4: i in ( dom (( Sum M1) + ( Sum M2)));

        then

         A5: i in ( dom ( addreal .: (( Sum M1),( Sum M2))));

        i in ( Seg ( len (M1 ^^ M2))) by A2, A3, A4, Def1;

        then

         A6: i in ( dom (M1 ^^ M2)) by FINSEQ_1:def 3;

        then

         A7: i in (( dom M1) /\ ( dom M2)) by PRE_POLY:def 4;

        then i in ( dom M1) by XBOOLE_0:def 4;

        then i in ( Seg ( len M1)) by FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M1))) by Def1;

        then

         A8: i in ( dom ( Sum M1)) by FINSEQ_1:def 3;

        i in ( dom M2) by A7, XBOOLE_0:def 4;

        then i in ( Seg ( len M2)) by FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M2))) by Def1;

        then

         A9: i in ( dom ( Sum M2)) by FINSEQ_1:def 3;

        

         A10: i in ( dom ( Sum (M1 ^^ M2))) by A2, A3, A4, FINSEQ_1:def 3;

        

         A11: ((M1 . i) ^ (M2 . i)) = ((M1 ^^ M2) . i) by A6, PRE_POLY:def 4;

        

        thus ((( Sum M1) + ( Sum M2)) . i) = (( addreal .: (( Sum M1),( Sum M2))) . i)

        .= ( addreal . ((( Sum M1) . i),(( Sum M2) . i))) by A5, FUNCOP_1: 22

        .= ((( Sum M1) . i) + (( Sum M2) . i)) by BINOP_2:def 9

        .= (( Sum (M1 . i)) + (( Sum M2) . i)) by A8, Def1

        .= (( Sum (M1 . i)) + ( Sum (M2 . i))) by A9, Def1

        .= ( Sum ((M1 ^^ M2) . i)) by A11, RVSUM_1: 75

        .= (( Sum (M1 ^^ M2)) . i) by A10, Def1;

      end;

      hence thesis by A2, FINSEQ_2: 9;

    end;

    theorem :: MATRPROB:27

    

     Th27: for M1,M2 be Matrix of REAL st ( len M1) = ( len M2) holds (( SumAll M1) + ( SumAll M2)) = ( SumAll (M1 ^^ M2))

    proof

      let M1,M2 be Matrix of REAL such that

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

      ( len ( Sum M1)) = ( len M1) by Def1

      .= ( len ( Sum M2)) by A1, Def1;

      then

      reconsider p1 = ( Sum M1), p2 = ( Sum M2) as Element of (( len ( Sum M1)) -tuples_on REAL ) by FINSEQ_2: 92;

      

      thus (( SumAll M1) + ( SumAll M2)) = ( Sum (p1 + p2)) by RVSUM_1: 89

      .= ( SumAll (M1 ^^ M2)) by Th26;

    end;

    theorem :: MATRPROB:28

    

     Th28: for M be Matrix of REAL holds ( SumAll M) = ( SumAll (M @ ))

    proof

      let M be Matrix of REAL ;

      defpred x[ Nat] means for M be Matrix of REAL st ( len M) = $1 holds ( SumAll M) = ( SumAll (M @ ));

      

       A1: for p be FinSequence of REAL holds ( SumAll <*p*>) = ( SumAll ( <*p*> @ ))

      proof

        defpred x[ FinSequence of REAL ] means ( SumAll <*$1*>) = ( SumAll ( <*$1*> @ ));

        let p be FinSequence of REAL ;

        

         A2: for p be FinSequence of REAL , x be Element of REAL st x[p] holds x[(p ^ <*x*>)]

        proof

          let p be FinSequence of REAL , x be Element of REAL such that

           A3: ( SumAll <*p*>) = ( SumAll ( <*p*> @ ));

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

          .= (( dom <*p*>) /\ ( dom <* <*x*>*>)) by PRE_POLY:def 4

          .= (( Seg 1) /\ ( dom <* <*x*>*>)) by FINSEQ_1: 38

          .= (( Seg 1) /\ ( Seg 1)) by FINSEQ_1: 38

          .= ( Seg 1);

          

          then

           A4: ( len ( <*p*> ^^ <* <*x*>*>)) = 1 by FINSEQ_1: 6

          .= ( len <*(p ^ <*x*>)*>) by FINSEQ_1: 39;

          

           A5: ( dom <*(p ^ <*x*>)*>) = ( Seg ( len <*(p ^ <*x*>)*>)) by FINSEQ_1:def 3;

           A6:

          now

            let i be Nat;

            reconsider M1 = ( <*p*> . i), M2 = ( <* <*x*>*> . i) as FinSequence;

            assume

             A7: i in ( dom <*(p ^ <*x*>)*>);

            then i in {1} by A5, FINSEQ_1: 2, FINSEQ_1: 40;

            then

             A8: i = 1 by TARSKI:def 1;

            i in ( dom ( <*p*> ^^ <* <*x*>*>)) by A4, A5, A7, FINSEQ_1:def 3;

            

            hence (( <*p*> ^^ <* <*x*>*>) . i) = (M1 ^ M2) by PRE_POLY:def 4

            .= (p ^ M2) by A8, FINSEQ_1: 40

            .= (p ^ <*x*>) by A8, FINSEQ_1: 40

            .= ( <*(p ^ <*x*>)*> . i) by A8, FINSEQ_1: 40;

          end;

          per cases ;

            suppose ( len p) = 0 ;

            then

             A9: p = {} ;

            

            hence ( SumAll <*(p ^ <*x*>)*>) = ( SumAll <* <*x*>*>) by FINSEQ_1: 34

            .= ( SumAll ( <* <*x*>*> @ )) by MATRLIN: 15

            .= ( SumAll ( <*(p ^ <*x*>)*> @ )) by A9, FINSEQ_1: 34;

          end;

            suppose

             A10: ( len p) <> 0 ;

            

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

            

            then

             A12: ( width <* <*x*>*>) = ( len <*x*>) by MATRIX_0: 20

            .= 1 by FINSEQ_1: 40;

            then

             A13: ( len ( <* <*x*>*> @ )) = 1 by MATRIX_0:def 6;

            

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

            then

             A15: ( width <*p*>) = ( len p) by MATRIX_0: 20;

            then

             A16: ( len ( <*p*> @ )) = ( len p) by MATRIX_0:def 6;

            ( width ( <*p*> @ )) = 1 by A10, A14, A15, MATRIX_0: 54;

            then

            reconsider d1 = ( <*p*> @ ) as Matrix of ( len p), 1, REAL by A10, A16, MATRIX_0: 20;

            ( len <*(p ^ <*x*>)*>) = 1 by FINSEQ_1: 40;

            

            then

             A17: ( width <*(p ^ <*x*>)*>) = ( len (p ^ <*x*>)) by MATRIX_0: 20

            .= (( len p) + ( len <*x*>)) by FINSEQ_1: 22

            .= (( len p) + 1) by FINSEQ_1: 40;

            

             A18: (( <* <*x*>*> @ ) @ ) = <* <*x*>*> by A11, A12, MATRIX_0: 57;

            

             A19: ( width ( <*p*> @ )) = ( len <*p*>) by A10, A15, MATRIX_0: 54

            .= ( width ( <* <*x*>*> @ )) by A14, A11, A12, MATRIX_0: 54;

            then ( width ( <* <*x*>*> @ )) = 1 by A10, A14, A15, MATRIX_0: 54;

            then

            reconsider d2 = ( <* <*x*>*> @ ) as Matrix of 1, 1, REAL by A13, MATRIX_0: 20;

            

             A20: ((d1 ^ d2) @ ) = ((( <*p*> @ ) @ ) ^^ (( <* <*x*>*> @ ) @ )) by A19, MATRLIN: 28

            .= ( <*p*> ^^ <* <*x*>*>) by A10, A14, A15, A18, MATRIX_0: 57

            .= <*(p ^ <*x*>)*> by A4, A6, FINSEQ_2: 9

            .= (( <*(p ^ <*x*>)*> @ ) @ ) by A17, MATRIX_0: 57;

            

             A21: ( len (( <*p*> @ ) ^ ( <* <*x*>*> @ ))) = (( len ( <*p*> @ )) + ( len ( <* <*x*>*> @ ))) by FINSEQ_1: 22

            .= (( width <*p*>) + ( len ( <* <*x*>*> @ ))) by MATRIX_0:def 6

            .= (( width <*p*>) + ( width <* <*x*>*>)) by MATRIX_0:def 6

            .= ( len ( <*(p ^ <*x*>)*> @ )) by A15, A12, A17, MATRIX_0:def 6;

            

            thus ( SumAll <*(p ^ <*x*>)*>) = ( SumAll ( <*p*> ^^ <* <*x*>*>)) by A4, A6, FINSEQ_2: 9

            .= (( SumAll ( <*p*> @ )) + ( SumAll <* <*x*>*>)) by A3, A14, A11, Th27

            .= (( SumAll ( <*p*> @ )) + ( SumAll ( <* <*x*>*> @ ))) by MATRLIN: 15

            .= ( Sum (( Sum d1) ^ ( Sum d2))) by RVSUM_1: 75

            .= ( SumAll (d1 ^ d2)) by Th25

            .= ( SumAll ( <*(p ^ <*x*>)*> @ )) by A21, A20, MATRIX_0: 53;

          end;

        end;

        

         A22: x[( <*> REAL )]

        proof

          set M1 = <*( <*> REAL )*>;

          reconsider E = ( <*> REAL ) as Element of ( REAL * ) by FINSEQ_1:def 11;

          set M1 = <*E*>;

          reconsider M1 as Matrix of REAL by MATRIX_0: 3;

          

           A23: ( len M1) = 1 by FINSEQ_1: 39;

          for p be FinSequence of REAL st p in ( rng M1) holds ( len p) = 0

          proof

            let p be FinSequence of REAL such that

             A24: p in ( rng M1);

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

            then p = ( <*> REAL ) by A24, TARSKI:def 1;

            hence ( len p) = 0 ;

          end;

          then M1 is 1, 0 -size by A23, MATRIX_0:def 2;

          then

          reconsider M1 as Matrix of 1, 0 , REAL ;

          

           A25: ( width M1) = 0 by MATRIX_0: 20, A23;

          

           A26: ( len (M1 @ )) = 0 by MATRIX_0:def 6, A25;

          ( SumAll M1) = 0 by Th24

          .= ( SumAll (M1 @ )) by A26, Th23;

          hence thesis;

        end;

        for p be FinSequence of REAL holds x[p] from FINSEQ_2:sch 2( A22, A2);

        hence thesis;

      end;

      

       A27: for n st x[n] holds x[(n + 1)]

      proof

        let n such that

         A28: for M be Matrix of REAL st ( len M) = n holds ( SumAll M) = ( SumAll (M @ ));

        thus for M be Matrix of REAL st ( len M) = (n + 1) holds ( SumAll M) = ( SumAll (M @ ))

        proof

          let M be Matrix of REAL such that

           A29: ( len M) = (n + 1);

          

           a29: M <> {} by A29;

          

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

          per cases ;

            suppose

             A31: n = 0 ;

            reconsider g = (M . 1) as FinSequence of REAL ;

            M = <*g*> by A29, A31, FINSEQ_1: 40;

            hence thesis by A1;

          end;

            suppose

             A32: n > 0 ;

            reconsider M9 = M as Matrix of (n + 1), ( width M), REAL by A29, MATRIX_0: 20;

            reconsider M1 = (M . (n + 1)) as FinSequence of REAL ;

            reconsider w = ( Del (M9,(n + 1))) as Matrix of n, ( width M), REAL by MATRLIN: 3;

            (M . (n + 1)) = ( Line (M,(n + 1))) by A29, A30, FINSEQ_1: 4, MATRIX_0: 60;

            then ( len M1) = ( width M) by MATRIX_0:def 7;

            then

            reconsider r = <*M1*> as Matrix of 1, ( width M), REAL ;

            

             A33: ( width w) = ( width M9) by A32, MATRLIN: 2

            .= ( width r) by MATRLIN: 2;

            

             A34: ( len (w @ )) = ( width w) by MATRIX_0:def 6

            .= ( len (r @ )) by A33, MATRIX_0:def 6;

            

             A35: ( len ( Del (M,(n + 1)))) = n by A29, PRE_POLY: 12;

            

            thus ( SumAll M) = ( SumAll (w ^ r)) by a29, A29, PRE_POLY: 13

            .= ( Sum (( Sum w) ^ ( Sum r))) by Th25

            .= (( SumAll ( Del (M,(n + 1)))) + ( SumAll r)) by RVSUM_1: 75

            .= (( SumAll (( Del (M,(n + 1))) @ )) + ( SumAll r)) by A28, A35

            .= (( SumAll (( Del (M,(n + 1))) @ )) + ( SumAll (r @ ))) by A1

            .= ( SumAll ((w @ ) ^^ (r @ ))) by A34, Th27

            .= ( SumAll ((w ^ r) @ )) by A33, MATRLIN: 28

            .= ( SumAll (M @ )) by a29, PRE_POLY: 13, A29;

          end;

        end;

      end;

      

       A36: x[ 0 ]

      proof

        let M be Matrix of REAL ;

        assume

         A37: ( len M) = 0 ;

        then ( width M) = 0 by MATRIX_0:def 3;

        then

         A38: ( len (M @ )) = 0 by MATRIX_0:def 6;

        

        thus ( SumAll M) = 0 by A37, Th23

        .= ( SumAll (M @ )) by A38, Th23;

      end;

      for n holds x[n] from NAT_1:sch 2( A36, A27);

      then x[( len M)];

      hence thesis;

    end;

    theorem :: MATRPROB:29

    

     Th29: for M be Matrix of REAL holds ( SumAll M) = ( Sum ( ColSum M))

    proof

      let M be Matrix of REAL ;

      

      thus ( Sum ( ColSum M)) = ( SumAll (M @ )) by Th22

      .= ( SumAll M) by Th28;

    end;

    theorem :: MATRPROB:30

    

     Th30: for x,y be FinSequence of REAL st ( len x) = ( len y) holds ( len ( mlt (x,y))) = ( len x) by FINSEQ_2: 72;

    theorem :: MATRPROB:31

    

     Th31: for i holds for R be Element of (i -tuples_on REAL ) holds ( mlt ((i |-> 1),R)) = R

    proof

      let i;

      let R be Element of (i -tuples_on REAL );

      

      thus ( mlt ((i |-> 1),R)) = (1 * R) by RVSUM_1: 63

      .= R by RVSUM_1: 52;

    end;

    theorem :: MATRPROB:32

    

     Th32: for x be FinSequence of REAL holds ( mlt ((( len x) |-> 1),x)) = x

    proof

      let x be FinSequence of REAL ;

      reconsider y = x as Element of (( len x) -tuples_on REAL ) by FINSEQ_2: 92;

      ( mlt ((( len x) |-> 1),y)) = y by Th31;

      hence thesis;

    end;

    theorem :: MATRPROB:33

    

     Th33: for x,y be FinSequence of REAL st (for i st i in ( dom x) holds (x . i) >= 0 ) & (for i st i in ( dom y) holds (y . i) >= 0 ) holds for k st k in ( dom ( mlt (x,y))) holds (( mlt (x,y)) . k) >= 0

    proof

      

       A1: for z be FinSequence of REAL st (for i st i in ( dom z) holds (z . i) >= 0 ) holds for i holds (z . i) >= 0

      proof

        let z be FinSequence of REAL such that

         A2: for i st i in ( dom z) holds (z . i) >= 0 ;

        hereby

          let i;

          per cases ;

            suppose not i in ( dom z);

            hence (z . i) >= 0 by FUNCT_1:def 2;

          end;

            suppose i in ( dom z);

            hence (z . i) >= 0 by A2;

          end;

        end;

      end;

      let x,y be FinSequence of REAL such that

       A3: (for i st i in ( dom x) holds (x . i) >= 0 ) & for i st i in ( dom y) holds (y . i) >= 0 ;

      hereby

        let k;

        assume k in ( dom ( mlt (x,y)));

        

         A4: (( mlt (x,y)) . k) = ((x . k) * (y . k)) by RVSUM_1: 59;

        (x . k) >= 0 & (y . k) >= 0 by A3, A1;

        hence (( mlt (x,y)) . k) >= 0 by A4;

      end;

    end;

    theorem :: MATRPROB:34

    

     Th34: for i holds for e1,e2 be Element of (i -tuples_on REAL ) holds for f1,f2 be Element of (i -tuples_on the carrier of F_Real ) st e1 = f1 & e2 = f2 holds ( mlt (e1,e2)) = ( mlt (f1,f2))

    proof

      let i;

      let e1,e2 be Element of (i -tuples_on REAL );

      let f1,f2 be Element of (i -tuples_on the carrier of F_Real ) such that

       A1: e1 = f1 & e2 = f2;

      

       A2: ( dom ( mlt (e1,e2))) = ( Seg ( len ( mlt (e1,e2)))) by FINSEQ_1:def 3

      .= ( Seg i) by CARD_1:def 7

      .= ( Seg ( len ( mlt (f1,f2)))) by CARD_1:def 7

      .= ( dom ( mlt (f1,f2))) by FINSEQ_1:def 3;

      for i be Nat st i in ( dom ( mlt (e1,e2))) holds (( mlt (e1,e2)) . i) = (( mlt (f1,f2)) . i)

      proof

        let i be Nat such that

         A3: i in ( dom ( mlt (e1,e2)));

        (e1 . i) in REAL & (e2 . i) in REAL by XREAL_0:def 1;

        then

        reconsider a1 = (e1 . i), a2 = (e2 . i) as Element of F_Real by VECTSP_1:def 5;

        

        thus (( mlt (e1,e2)) . i) = (a1 * a2) by RVSUM_1: 59

        .= (( mlt (f1,f2)) . i) by A1, A2, A3, FVSUM_1: 60;

      end;

      hence thesis by A2, FINSEQ_1: 13;

    end;

    theorem :: MATRPROB:35

    

     Th35: for e1,e2 be FinSequence of REAL holds for f1,f2 be FinSequence of F_Real st ( len e1) = ( len e2) & e1 = f1 & e2 = f2 holds ( mlt (e1,e2)) = ( mlt (f1,f2))

    proof

      let e1,e2 be FinSequence of REAL ;

      let f1,f2 be FinSequence of F_Real such that

       A1: ( len e1) = ( len e2) and

       A2: e1 = f1 and

       A3: e2 = f2;

      set l = ( len e1);

      set Z = { f where f be Element of (the carrier of F_Real * ) : ( len f) = l };

      f1 is Element of (the carrier of F_Real * ) by FINSEQ_1:def 11;

      then f1 in Z by A2;

      then

      reconsider f3 = f1 as Element of (l -tuples_on the carrier of F_Real );

      f2 is Element of (the carrier of F_Real * ) by FINSEQ_1:def 11;

      then f2 in Z by A1, A3;

      then

      reconsider f4 = f2 as Element of (l -tuples_on the carrier of F_Real );

      set Y = { e where e be Element of ( REAL * ) : ( len e) = l };

      e2 is Element of ( REAL * ) by FINSEQ_1:def 11;

      then e2 in Y by A1;

      then

      reconsider e4 = e2 as Element of (l -tuples_on REAL );

      reconsider e3 = e1 as Element of (l -tuples_on REAL ) by FINSEQ_2: 92;

      ( mlt (e3,e4)) = ( mlt (f3,f4)) by A2, A3, Th34;

      hence thesis;

    end;

    theorem :: MATRPROB:36

    

     Th36: for e be FinSequence of REAL holds for f be FinSequence of F_Real st e = f holds ( Sum e) = ( Sum f)

    proof

      let e be FinSequence of REAL ;

      let f be FinSequence of F_Real such that

       A1: e = f;

      consider e1 be sequence of REAL such that

       A2: (e1 . 0 ) = 0 and

       A3: for i be Nat st i < ( len e) holds (e1 . (i + 1)) = ((e1 . i) + (e . (i + 1))) and

       A4: ( Sum e) = (e1 . ( len e)) by Th7;

      consider f1 be sequence of the carrier of F_Real such that

       A5: ( Sum f) = (f1 . ( len f)) and

       A6: (f1 . 0 ) = ( 0. F_Real ) and

       A7: for j be Nat holds for v be Element of F_Real st j < ( len f) & v = (f . (j + 1)) holds (f1 . (j + 1)) = ((f1 . j) + v) by RLVECT_1:def 12;

      for n holds n <= ( len e) implies (e1 . n) = (f1 . n)

      proof

        defpred p[ Nat] means $1 <= ( len e) implies (e1 . $1) = (f1 . $1);

        let n;

         A8:

        now

          let k be Nat such that

           A9: p[k];

          now

            reconsider k9 = k as Element of NAT by ORDINAL1:def 12;

            (e . (k + 1)) in REAL by XREAL_0:def 1;

            then

            reconsider a = (e . (k + 1)) as Element of F_Real by VECTSP_1:def 5;

            assume (k + 1) <= ( len e);

            then

             A10: k < ( len e) by NAT_1: 13;

            

            then (e1 . (k + 1)) = ((f1 . k9) + a) by A3, A9

            .= (f1 . (k + 1)) by A1, A7, A10;

            hence (e1 . (k + 1)) = (f1 . (k + 1));

          end;

          hence p[(k + 1)];

        end;

        

         A11: p[ 0 ] by A2, A6, STRUCT_0:def 6, VECTSP_1:def 5;

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

        hence thesis;

      end;

      hence thesis by A1, A4, A5;

    end;

    notation

      let e1,e2 be FinSequence of REAL ;

      synonym e1 "*" e2 for |(e1,e2)|;

    end

    theorem :: MATRPROB:37

    for i holds for e1,e2 be Element of (i -tuples_on REAL ) holds for f1,f2 be Element of (i -tuples_on the carrier of F_Real ) st e1 = f1 & e2 = f2 holds (e1 "*" e2) = (f1 "*" f2)

    proof

      let i;

      let e1,e2 be Element of (i -tuples_on REAL );

      let f1,f2 be Element of (i -tuples_on the carrier of F_Real );

      assume e1 = f1 & e2 = f2;

      

      hence (e1 "*" e2) = ( Sum ( mlt (f1,f2))) by Th34, Th36

      .= (f1 "*" f2) by FVSUM_1:def 9;

    end;

    theorem :: MATRPROB:38

    

     Th38: for e1,e2 be FinSequence of REAL holds for f1,f2 be FinSequence of F_Real st ( len e1) = ( len e2) & e1 = f1 & e2 = f2 holds (e1 "*" e2) = (f1 "*" f2)

    proof

      let e1,e2 be FinSequence of REAL ;

      let f1,f2 be FinSequence of F_Real ;

      assume ( len e1) = ( len e2) & e1 = f1 & e2 = f2;

      

      hence (e1 "*" e2) = ( Sum ( mlt (f1,f2))) by Th35, Th36

      .= (f1 "*" f2) by FVSUM_1:def 9;

    end;

    theorem :: MATRPROB:39

    

     Th39: for M,M1,M2 be Matrix of REAL st ( width M1) = ( len M2) holds M = (M1 * M2) iff ( len M) = ( len M1) & ( width M) = ( width M2) & for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j)))

    proof

      let M,M1,M2 be Matrix of REAL such that

       A1: ( width M1) = ( len M2);

      set MM = ( MXR2MXF M);

      set M4 = ( MXR2MXF M2);

      set M3 = ( MXR2MXF M1);

      

       A2: M3 = M1 by MATRIXR1:def 1;

      

       A3: M4 = M2 by MATRIXR1:def 1;

      ( MXF2MXR (M3 * M4)) = (M1 * M2) by MATRIXR1:def 6;

      then

       A4: (M3 * M4) = (M1 * M2) by MATRIXR1:def 2;

      hereby

        assume

         A5: M = (M1 * M2);

        hence

         A6: ( len M) = ( len M1) by A1, A2, A3, A4, MATRIX_3:def 4;

        thus

         A7: ( width M) = ( width M2) by A1, A2, A3, A4, A5, MATRIX_3:def 4;

        thus for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j)))

        proof

          let i, j such that

           A8: [i, j] in ( Indices M);

          j in ( Seg ( width M2)) by A7, A8, Th12;

          then

           A9: ( Col (M4,j)) = ( Col (M2,j)) by A3, Th17;

          i in ( Seg ( len M1)) by A6, A8, Th12;

          then i in ( dom M1) by FINSEQ_1:def 3;

          then

           A10: ( Line (M3,i)) = ( Line (M1,i)) by A2, Th16;

          

           A11: ( len ( Line (M1,i))) = ( width M1) by MATRIX_0:def 7

          .= ( len ( Col (M2,j))) by A1, MATRIX_0:def 8;

          M = ( MXF2MXR (M3 * M4)) by A5, MATRIXR1:def 6;

          then [i, j] in ( Indices (M3 * M4)) & (M * (i,j)) = ((M3 * M4) * (i,j)) by A8, MATRIXR1: 23, MATRIXR1:def 2;

          

          hence (M * (i,j)) = (( Line (M3,i)) "*" ( Col (M4,j))) by A1, A2, A3, MATRIX_3:def 4

          .= (( Line (M1,i)) "*" ( Col (M2,j))) by A10, A9, A11, Th38;

        end;

      end;

      assume that

       A12: ( len M) = ( len M1) and

       A13: ( width M) = ( width M2) and

       A14: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j)));

      

       A15: ( width MM) = ( width M) by MATRIXR1:def 1

      .= ( width M4) by A13, MATRIXR1:def 1;

      

       A16: ( len MM) = ( len M) by MATRIXR1:def 1

      .= ( len M3) by A12, MATRIXR1:def 1;

      for i,j be Nat st [i, j] in ( Indices MM) holds (MM * (i,j)) = (( Line (M3,i)) "*" ( Col (M4,j)))

      proof

        let i,j be Nat such that

         A17: [i, j] in ( Indices MM);

        j in ( Seg ( width M4)) by A15, A17, Th12;

        then

         A18: ( Col (M4,j)) = ( Col (M2,j)) by Th17, MATRIXR1:def 1;

        i in ( Seg ( len M3)) by A16, A17, Th12;

        then i in ( dom M3) by FINSEQ_1:def 3;

        then

         A19: ( Line (M3,i)) = ( Line (M1,i)) by Th16, MATRIXR1:def 1;

        

         A20: ( len ( Line (M1,i))) = ( width M1) by MATRIX_0:def 7

        .= ( len ( Col (M2,j))) by A1, MATRIX_0:def 8;

         [i, j] in ( Indices M) & (MM * (i,j)) = (M * (i,j)) by A17, MATRIXR1: 23, MATRIXR1:def 1;

        

        hence (MM * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j))) by A14

        .= (( Line (M3,i)) "*" ( Col (M4,j))) by A19, A18, A20, Th38;

      end;

      then MM = M & MM = (M3 * M4) by A1, A2, A3, A16, A15, MATRIXR1:def 1, MATRIX_3:def 4;

      then M = ( MXF2MXR (M3 * M4)) by MATRIXR1:def 2;

      hence thesis by MATRIXR1:def 6;

    end;

    theorem :: MATRPROB:40

    

     Th40: for M be Matrix of REAL holds for p be FinSequence of REAL st ( len M) = ( len p) holds for i st i in ( Seg ( len (p * M))) holds ((p * M) . i) = (p "*" ( Col (M,i)))

    proof

      let M be Matrix of REAL ;

      let p be FinSequence of REAL such that

       A1: ( len M) = ( len p);

      

       A2: ( len (p * M)) = ( len ( Line ((( LineVec2Mx p) * M),1))) by MATRIXR1:def 12

      .= ( width (( LineVec2Mx p) * M)) by MATRIX_0:def 7;

      hereby

        let i such that

         A3: i in ( Seg ( len (p * M)));

        

         A4: ( width ( LineVec2Mx p)) = ( len M) by A1, MATRIXR1:def 10;

        then ( len (( LineVec2Mx p) * M)) = ( len ( LineVec2Mx p)) by Th39;

        then ( len (( LineVec2Mx p) * M)) = 1 by MATRIXR1: 48;

        then 1 in ( Seg ( len (( LineVec2Mx p) * M)));

        then [1, i] in ( Indices (( LineVec2Mx p) * M)) by A2, A3, Th12;

        

        then

         A5: ((( LineVec2Mx p) * M) * (1,i)) = (( Line (( LineVec2Mx p),1)) "*" ( Col (M,i))) by A4, Th39

        .= (p "*" ( Col (M,i))) by MATRIXR1: 48;

        (( Line ((( LineVec2Mx p) * M),1)) . i) = ((( LineVec2Mx p) * M) * (1,i)) by A2, A3, MATRIX_0:def 7;

        hence (p "*" ( Col (M,i))) = ((p * M) . i) by A5, MATRIXR1:def 12;

      end;

    end;

    theorem :: MATRPROB:41

    

     Th41: for M be Matrix of REAL holds for p be FinSequence of REAL st ( width M) = ( len p) & ( width M) > 0 holds for i st i in ( Seg ( len (M * p))) holds ((M * p) . i) = (( Line (M,i)) "*" p)

    proof

      let M be Matrix of REAL ;

      let p be FinSequence of REAL such that

       A1: ( width M) = ( len p) & ( width M) > 0 ;

      

       A2: ( len (M * p)) = ( len ( Col ((M * ( ColVec2Mx p)),1))) by MATRIXR1:def 11

      .= ( len (M * ( ColVec2Mx p))) by MATRIX_0:def 8;

      hereby

        let i such that

         A3: i in ( Seg ( len (M * p)));

        i in ( dom (M * ( ColVec2Mx p))) by A2, A3, FINSEQ_1:def 3;

        then

         A4: (( Col ((M * ( ColVec2Mx p)),1)) . i) = ((M * ( ColVec2Mx p)) * (i,1)) by MATRIX_0:def 8;

        

         A5: ( len ( ColVec2Mx p)) = ( width M) by A1, MATRIXR1:def 9;

        then ( width (M * ( ColVec2Mx p))) = ( width ( ColVec2Mx p)) by Th39;

        then ( width (M * ( ColVec2Mx p))) = 1 by A1, MATRIXR1:def 9;

        then 1 in ( Seg ( width (M * ( ColVec2Mx p))));

        then [i, 1] in ( Indices (M * ( ColVec2Mx p))) by A2, A3, Th12;

        

        then ((M * ( ColVec2Mx p)) * (i,1)) = (( Line (M,i)) "*" ( Col (( ColVec2Mx p),1))) by A5, Th39

        .= (( Line (M,i)) "*" p) by A1, MATRIXR1: 45;

        hence (( Line (M,i)) "*" p) = ((M * p) . i) by A4, MATRIXR1:def 11;

      end;

    end;

    theorem :: MATRPROB:42

    

     Th42: for M,M1,M2 be Matrix of REAL st ( width M1) = ( len M2) holds M = (M1 * M2) iff ( len M) = ( len M1) & ( width M) = ( width M2) & for i st i in ( Seg ( len M)) holds ( Line (M,i)) = (( Line (M1,i)) * M2)

    proof

      let M,M1,M2 be Matrix of REAL such that

       A1: ( width M1) = ( len M2);

      hereby

        assume

         A2: M = (M1 * M2);

        hence

         A3: ( len M) = ( len M1) & ( width M) = ( width M2) by A1, Th39;

        thus for i st i in ( Seg ( len M)) holds ( Line (M,i)) = (( Line (M1,i)) * M2)

        proof

          let i such that

           A4: i in ( Seg ( len M));

          

           A5: ( len ( Line (M1,i))) = ( len M2) by A1, MATRIX_0:def 7;

          then

           A6: ( len (( Line (M1,i)) * M2)) = ( width M2) by MATRIXR1: 62;

          ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7;

          

          then

           A7: ( dom ( Line (M,i))) = ( Seg ( width M2)) by A3, FINSEQ_1:def 3

          .= ( dom (( Line (M1,i)) * M2)) by A6, FINSEQ_1:def 3;

          

           A8: i in ( dom M) by A4, FINSEQ_1:def 3;

          for j be Nat st j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) = ((( Line (M1,i)) * M2) . j)

          proof

            let j be Nat such that

             A9: j in ( dom ( Line (M,i)));

            

             A10: j in ( Seg ( len (( Line (M1,i)) * M2))) by A7, A9, FINSEQ_1:def 3;

            j in ( Seg ( len ( Line (M,i)))) by A9, FINSEQ_1:def 3;

            then j in ( Seg ( width M)) by MATRIX_0:def 7;

            then

             A11: [i, j] in ( Indices M) by A4, Th12;

            

             A12: ((M . i) . j) in REAL by XREAL_0:def 1;

            

            thus (( Line (M,i)) . j) = ((M . i) . j) by A8, MATRIX_0: 60

            .= (M * (i,j)) by A11, MATRIX_0:def 5, A12

            .= (( Line (M1,i)) "*" ( Col (M2,j))) by A1, A2, A11, Th39

            .= ((( Line (M1,i)) * M2) . j) by A5, A10, Th40;

          end;

          hence thesis by A7, FINSEQ_1: 13;

        end;

      end;

      assume that

       A13: ( len M) = ( len M1) and

       A14: ( width M) = ( width M2) and

       A15: for i st i in ( Seg ( len M)) holds ( Line (M,i)) = (( Line (M1,i)) * M2);

      for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j)))

      proof

        let i, j such that

         A16: [i, j] in ( Indices M);

        

         A17: i in ( Seg ( len M)) by A16, Th12;

        then

         A18: i in ( dom M) by FINSEQ_1:def 3;

        

         A19: ( len ( Line (M1,i))) = ( len M2) by A1, MATRIX_0:def 7;

        j in ( Seg ( width M)) by A16, Th12;

        then

         A20: j in ( Seg ( len (( Line (M1,i)) * M2))) by A14, A19, MATRIXR1: 62;

        ((M . i) . j) in REAL by XREAL_0:def 1;

        

        hence (M * (i,j)) = ((M . i) . j) by A16, MATRIX_0:def 5

        .= (( Line (M,i)) . j) by A18, MATRIX_0: 60

        .= ((( Line (M1,i)) * M2) . j) by A15, A17

        .= (( Line (M1,i)) "*" ( Col (M2,j))) by A19, A20, Th40;

      end;

      hence thesis by A1, A13, A14, Th39;

    end;

    definition

      let x,y be FinSequence of REAL , M be Matrix of REAL ;

      assume that

       A1: ( len x) = ( len M) and

       A2: ( len y) = ( width M);

      :: MATRPROB:def4

      func QuadraticForm (x,M,y) -> Matrix of REAL means

      : Def4: ( len it ) = ( len x) & ( width it ) = ( len y) & for i,j be Nat st [i, j] in ( Indices M) holds (it * (i,j)) = (((x . i) * (M * (i,j))) * (y . j));

      existence

      proof

        deffunc F( Nat, Nat) = ( In ((((x . $1) * (M * ($1,$2))) * (y . $2)), REAL ));

        consider M1 be Matrix of ( len M), ( width M), REAL such that

         A3: for i,j be Nat st [i, j] in ( Indices M1) holds (M1 * (i,j)) = F(i,j) from MATRIX_0:sch 1;

        take M1;

        thus

         A4: ( len M1) = ( len x) by A1, MATRIX_0:def 2;

         A5:

        now

          per cases ;

            case

             A6: ( len M) = 0 ;

            then ( width M1) = 0 by A1, A4, MATRIX_0:def 3;

            hence ( width M1) = ( len y) by A2, A6, MATRIX_0:def 3;

          end;

            case ( len M) > 0 ;

            hence ( width M1) = ( len y) by A2, MATRIX_0: 23;

          end;

        end;

        

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

        ( dom M) = ( dom M1) by A1, A4, FINSEQ_3: 29;

        then

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

        thus ( width M1) = ( len y) by A5;

        let i,j be Nat;

        assume [i, j] in ( Indices M);

        

        hence (M1 * (i,j)) = F(i,j) by A3, A7, A8

        .= (((x . i) * (M * (i,j))) * (y . j));

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of REAL ;

        assume that

         A9: ( len M1) = ( len x) and

         A10: ( width M1) = ( len y) and

         A11: for i,j be Nat st [i, j] in ( Indices M) holds (M1 * (i,j)) = (((x . i) * (M * (i,j))) * (y . j)) and

         A12: ( len M2) = ( len x) & ( width M2) = ( len y) and

         A13: for i,j be Nat st [i, j] in ( Indices M) holds (M2 * (i,j)) = (((x . i) * (M * (i,j))) * (y . j));

        now

          let i,j be Nat;

          

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

          ( dom M1) = ( dom M) by A1, A9, FINSEQ_3: 29;

          then

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

          assume

           A16: [i, j] in ( Indices M1);

          

          hence (M1 * (i,j)) = (((x . i) * (M * (i,j))) * (y . j)) by A11, A15, A14

          .= (M2 * (i,j)) by A13, A16, A15, A14;

        end;

        hence thesis by A9, A10, A12, MATRIX_0: 21;

      end;

    end

    theorem :: MATRPROB:43

    for x,y be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( len M) & ( len y) = ( width M) & ( len y) > 0 holds (( QuadraticForm (x,M,y)) @ ) = ( QuadraticForm (y,(M @ ),x))

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL ;

      assume that

       A1: ( len x) = ( len M) and

       A2: ( len y) = ( width M) and

       A3: ( len y) > 0 ;

      

       A4: ( len (M @ )) = ( len y) by A2, MATRIX_0:def 6;

      

       A5: ( width (M @ )) = ( len x) by A1, A2, A3, MATRIX_0: 54;

      then

       A6: ( len ( QuadraticForm (y,(M @ ),x))) = ( len y) & ( width ( QuadraticForm (y,(M @ ),x))) = ( len x) by A4, Def4;

      

       A7: ( len (( QuadraticForm (x,M,y)) @ )) = ( width ( QuadraticForm (x,M,y))) by MATRIX_0:def 6;

      

       A8: ( width ( QuadraticForm (x,M,y))) = ( len y) by A1, A2, Def4;

      then

       A9: ( width (( QuadraticForm (x,M,y)) @ )) = ( len ( QuadraticForm (x,M,y))) by A3, MATRIX_0: 54;

      

       A10: for i,j be Nat st [i, j] in ( Indices (( QuadraticForm (x,M,y)) @ )) holds (( QuadraticForm (y,(M @ ),x)) * (i,j)) = ((( QuadraticForm (x,M,y)) @ ) * (i,j))

      proof

        let i,j be Nat;

        assume

         A11: [i, j] in ( Indices (( QuadraticForm (x,M,y)) @ ));

        reconsider i, j as Nat;

        

         A12: 1 <= j by A11, MATRIXC1: 1;

        

         A13: j <= ( len ( QuadraticForm (x,M,y))) by A9, A11, MATRIXC1: 1;

        then

         A14: j <= ( len M) by A1, A2, Def4;

        

         A15: 1 <= i by A11, MATRIXC1: 1;

        

         A16: i <= ( width ( QuadraticForm (x,M,y))) by A7, A11, MATRIXC1: 1;

        then i <= ( width M) by A1, A2, Def4;

        then

         A17: [j, i] in ( Indices M) by A12, A15, A14, MATRIXC1: 1;

        

         A18: j <= ( width (M @ )) by A1, A2, A5, A13, Def4;

        

         A19: 1 <= i by A11, MATRIXC1: 1;

        1 <= i by A11, MATRIXC1: 1;

        then

         A20: [j, i] in ( Indices ( QuadraticForm (x,M,y))) by A16, A12, A13, MATRIXC1: 1;

        i <= ( len (M @ )) by A1, A2, A4, A16, Def4;

        then [i, j] in ( Indices (M @ )) by A12, A19, A18, MATRIXC1: 1;

        

        then (( QuadraticForm (y,(M @ ),x)) * (i,j)) = (((y . i) * ((M @ ) * (i,j))) * (x . j)) by A4, A5, Def4

        .= (((y . i) * (M * (j,i))) * (x . j)) by A17, MATRIX_0:def 6

        .= (((x . j) * (M * (j,i))) * (y . i))

        .= (( QuadraticForm (x,M,y)) * (j,i)) by A1, A2, A17, Def4

        .= ((( QuadraticForm (x,M,y)) @ ) * (i,j)) by A20, MATRIX_0:def 6;

        hence thesis;

      end;

      

       A21: ( len (( QuadraticForm (x,M,y)) @ )) = ( width ( QuadraticForm (x,M,y))) by MATRIX_0:def 6

      .= ( len y) by A1, A2, Def4;

      ( width (( QuadraticForm (x,M,y)) @ )) = ( len ( QuadraticForm (x,M,y))) by A3, A8, MATRIX_0: 54

      .= ( len x) by A1, A2, Def4;

      hence thesis by A21, A6, A10, MATRIX_0: 21;

    end;

    theorem :: MATRPROB:44

    

     Th44: for x,y be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( len M) & ( len y) = ( width M) & ( len y) > 0 holds |(x, (M * y))| = ( SumAll ( QuadraticForm (x,M,y)))

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL ;

      set Z = ( QuadraticForm (x,M,y));

      assume that

       A1: ( len x) = ( len M) and

       A2: ( len y) = ( width M) and

       A3: ( len y) > 0 ;

      

       A4: ( width Z) = ( len y) by A1, A2, Def4;

      

       A5: ( len ( LineSum Z)) = ( len Z) by Th20;

      ( len (M * y)) = ( len x) by A1, A2, A3, MATRIXR1: 61;

      

      then

       A6: ( len ( mlt (x,(M * y)))) = ( len x) by Th30

      .= ( len ( LineSum Z)) by A1, A2, A5, Def4;

      for i be Nat st 1 <= i & i <= ( len ( LineSum Z)) holds (( LineSum Z) . i) = (( mlt (x,(M * y))) . i)

      proof

        let i be Nat;

        assume that

         A7: 1 <= i and

         A8: i <= ( len ( LineSum Z));

        

         A9: i in ( Seg ( len ( LineSum Z))) by A7, A8;

        then

         A10: i in ( Seg ( len M)) by A1, A2, A5, Def4;

        then

         A11: i in ( Seg ( len (M * y))) by A2, A3, MATRIXR1: 61;

        

         A12: ( len ( Line (M,i))) = ( len y) by A2, MATRIX_0:def 7;

        

         A13: i <= ( len M) by A10, FINSEQ_1: 1;

        

         A14: for j be Nat st 1 <= j & j <= ( len ( Line (Z,i))) holds (((x . i) * ( mlt (( Line (M,i)),y))) . j) = (( Line (Z,i)) . j)

        proof

          let j be Nat such that

           A15: 1 <= j and

           A16: j <= ( len ( Line (Z,i)));

          j <= ( width M) by A2, A4, A16, MATRIX_0:def 7;

          then

           A17: [i, j] in ( Indices M) by A7, A13, A15, MATRIXC1: 1;

          j in ( Seg ( len ( Line (Z,i)))) by A15, A16;

          then

           A18: j in ( Seg ( width Z)) by MATRIX_0:def 7;

          

          thus (((x . i) * ( mlt (( Line (M,i)),y))) . j) = ((x . i) * (( mlt (( Line (M,i)),y)) . j)) by RVSUM_1: 44

          .= ((x . i) * ((( Line (M,i)) . j) * (y . j))) by RVSUM_1: 59

          .= ((x . i) * ((M * (i,j)) * (y . j))) by A2, A4, A18, MATRIX_0:def 7

          .= (((x . i) * (M * (i,j))) * (y . j))

          .= (Z * (i,j)) by A1, A2, A17, Def4

          .= (( Line (Z,i)) . j) by A18, MATRIX_0:def 7;

        end;

        

         A19: ( len ( Line (Z,i))) = ( len y) by A4, MATRIX_0:def 7;

        ( len ( mlt (( Line (M,i)),y))) = ( len y) by A12, Th30;

        then ( len ((x . i) * ( mlt (( Line (M,i)),y)))) = ( len ( Line (Z,i))) by A19, RVSUM_1: 117;

        then

         A20: ((x . i) * ( mlt (( Line (M,i)),y))) = ( Line (Z,i)) by A14;

        (( mlt (x,(M * y))) . i) = ((x . i) * ((M * y) . i)) by RVSUM_1: 59

        .= ((x . i) * (( Line (M,i)) "*" y)) by A2, A3, A11, Th41

        .= ( Sum ((x . i) * ( mlt (( Line (M,i)),y)))) by RVSUM_1: 87;

        hence thesis by A5, A9, A20, Th20;

      end;

      hence thesis by A6, FINSEQ_1: 14;

    end;

    theorem :: MATRPROB:45

    for x be FinSequence of REAL holds |(x, (( len x) |-> 1))| = ( Sum x) by Th32;

    theorem :: MATRPROB:46

    

     Th46: for x,y be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( len M) & ( len y) = ( width M) holds |((x * M), y)| = ( SumAll ( QuadraticForm (x,M,y)))

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL ;

      set Z = ( QuadraticForm (x,M,y));

      assume that

       A1: ( len x) = ( len M) and

       A2: ( len y) = ( width M);

      

       A3: ( len Z) = ( len x) by A1, A2, Def4;

      

       A4: ( len ( ColSum Z)) = ( width Z) by Def2;

      ( len (x * M)) = ( len y) by A1, A2, MATRIXR1: 62;

      

      then

       A5: ( len ( mlt ((x * M),y))) = ( len y) by Th30

      .= ( len ( ColSum Z)) by A1, A2, A4, Def4;

      for i be Nat st 1 <= i & i <= ( len ( ColSum Z)) holds (( ColSum Z) . i) = (( mlt ((x * M),y)) . i)

      proof

        let i be Nat;

        assume that

         A6: 1 <= i and

         A7: i <= ( len ( ColSum Z));

        

         A8: i in ( Seg ( len ( ColSum Z))) by A6, A7;

        then

         A9: i in ( Seg ( width M)) by A1, A2, A4, Def4;

        then

         A10: i in ( Seg ( len (x * M))) by A1, MATRIXR1: 62;

        

         A11: ( len ( Col (M,i))) = ( len x) by A1, MATRIX_0:def 8;

        

         A12: i <= ( width M) by A9, FINSEQ_1: 1;

        

         A13: for j be Nat st 1 <= j & j <= ( len ( Col (Z,i))) holds (((y . i) * ( mlt (x,( Col (M,i))))) . j) = (( Col (Z,i)) . j)

        proof

          let j be Nat such that

           A14: 1 <= j and

           A15: j <= ( len ( Col (Z,i)));

          j <= ( len M) by A1, A3, A15, MATRIX_0:def 8;

          then

           A16: [j, i] in ( Indices M) by A6, A12, A14, MATRIXC1: 1;

          j in ( Seg ( len ( Col (Z,i)))) by A14, A15;

          then

           A17: j in ( Seg ( len Z)) by MATRIX_0:def 8;

          then

           A18: j in ( dom Z) by FINSEQ_1:def 3;

          

           A19: j in ( dom M) by A1, A3, A17, FINSEQ_1:def 3;

          

          thus (((y . i) * ( mlt (x,( Col (M,i))))) . j) = ((y . i) * (( mlt (x,( Col (M,i)))) . j)) by RVSUM_1: 44

          .= ((y . i) * ((x . j) * (( Col (M,i)) . j))) by RVSUM_1: 59

          .= ((y . i) * ((x . j) * (M * (j,i)))) by A19, MATRIX_0:def 8

          .= (Z * (j,i)) by A1, A2, A16, Def4

          .= (( Col (Z,i)) . j) by A18, MATRIX_0:def 8;

        end;

        

         A20: ( len ( Col (Z,i))) = ( len x) by A3, MATRIX_0:def 8;

        ( len ( mlt (x,( Col (M,i))))) = ( len x) by A11, Th30;

        then ( len ((y . i) * ( mlt (x,( Col (M,i)))))) = ( len ( Col (Z,i))) by A20, RVSUM_1: 117;

        then

         A21: ((y . i) * ( mlt (x,( Col (M,i))))) = ( Col (Z,i)) by A13;

        (( mlt ((x * M),y)) . i) = (((x * M) . i) * (y . i)) by RVSUM_1: 59

        .= ((x "*" ( Col (M,i))) * (y . i)) by A1, A10, Th40

        .= ( Sum ((y . i) * ( mlt (x,( Col (M,i)))))) by RVSUM_1: 87;

        hence thesis by A4, A8, A21, Def2;

      end;

      

      hence |((x * M), y)| = ( Sum ( ColSum Z)) by A5, FINSEQ_1: 14

      .= ( SumAll Z) by Th29;

    end;

    theorem :: MATRPROB:47

    

     Th47: for x,y be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( len M) & ( len y) = ( width M) & ( len y) > 0 holds |((x * M), y)| = |(x, (M * y))|

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL such that

       A1: ( len x) = ( len M) & ( len y) = ( width M) and

       A2: ( len y) > 0 ;

      

      thus |((x * M), y)| = ( SumAll ( QuadraticForm (x,M,y))) by A1, Th46

      .= |(x, (M * y))| by A1, A2, Th44;

    end;

    theorem :: MATRPROB:48

    for x,y be FinSequence of REAL , M be Matrix of REAL st ( len y) = ( len M) & ( len x) = ( width M) & ( len x) > 0 & ( len y) > 0 holds |((M * x), y)| = |(x, ((M @ ) * y))|

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL such that

       A1: ( len y) = ( len M) and

       A2: ( len x) = ( width M) and

       A3: ( len x) > 0 and

       A4: ( len y) > 0 ;

      

       A5: ( len (M @ )) = ( width M) & ( width (M @ )) = ( len M) by A2, A3, MATRIX_0: 54;

      

      thus |((M * x), y)| = |((x * (M @ )), y)| by A1, A2, A3, A4, MATRIXR1: 53

      .= |(x, ((M @ ) * y))| by A1, A2, A4, A5, Th47;

    end;

    theorem :: MATRPROB:49

    

     Th49: for x,y be FinSequence of REAL , M be Matrix of REAL st ( len y) = ( len M) & ( len x) = ( width M) & ( len x) > 0 & ( len y) > 0 holds |(x, (y * M))| = |((x * (M @ )), y)|

    proof

      let x,y be FinSequence of REAL , M be Matrix of REAL such that

       A1: ( len y) = ( len M) and

       A2: ( len x) = ( width M) and

       A3: ( len x) > 0 and

       A4: ( len y) > 0 ;

      

       A5: ( len (M @ )) = ( width M) & ( width (M @ )) = ( len M) by A2, A3, MATRIX_0: 54;

      

      thus |(x, (y * M))| = |(x, ((M @ ) * y))| by A1, A2, A3, A4, MATRIXR1: 52

      .= |((x * (M @ )), y)| by A1, A2, A4, A5, Th47;

    end;

    theorem :: MATRPROB:50

    

     Th50: for x be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( len M) & x = (( len x) |-> 1) holds for k st k in ( Seg ( len (x * M))) holds ((x * M) . k) = ( Sum ( Col (M,k)))

    proof

      let x be FinSequence of REAL , M be Matrix of REAL such that

       A1: ( len x) = ( len M) and

       A2: x = (( len x) |-> 1);

      hereby

        let k such that

         A3: k in ( Seg ( len (x * M)));

        

         A4: ( len ( Col (M,k))) = ( len x) by A1, MATRIX_0:def 8;

        

        thus ((x * M) . k) = (x "*" ( Col (M,k))) by A1, A3, Th40

        .= ( Sum ( Col (M,k))) by A2, A4, Th32;

      end;

    end;

    theorem :: MATRPROB:51

    for x be FinSequence of REAL , M be Matrix of REAL st ( len x) = ( width M) & ( width M) > 0 & x = (( len x) |-> 1) holds for k st k in ( Seg ( len (M * x))) holds ((M * x) . k) = ( Sum ( Line (M,k)))

    proof

      let x be FinSequence of REAL , M be Matrix of REAL such that

       A1: ( len x) = ( width M) and

       A2: ( width M) > 0 and

       A3: x = (( len x) |-> 1);

      hereby

        let k such that

         A4: k in ( Seg ( len (M * x)));

        

         A5: ( len ( Line (M,k))) = ( len x) by A1, MATRIX_0:def 7;

        

        thus ((M * x) . k) = (( Line (M,k)) "*" x) by A1, A2, A4, Th41

        .= ( Sum ( Line (M,k))) by A3, A5, Th32;

      end;

    end;

    reconsider jj = 1, zz = 0 as Element of REAL by XREAL_0:def 1;

    theorem :: MATRPROB:52

    

     Th52: for n be non zero Nat holds ex P be FinSequence of REAL st ( len P) = n & (for i st i in ( dom P) holds (P . i) >= 0 ) & ( Sum P) = 1

    proof

      let n be non zero Nat;

      reconsider n as non zero Nat;

      consider e be FinSequence of REAL such that

       A1: ( len e) = n and

       A2: for i be Nat st i in ( Seg n) holds (i in ( Seg 1) implies (e . i) = jj) & ( not i in ( Seg 1) implies (e . i) = zz) by Th2;

      

       A3: n >= 1 by NAT_1: 14;

      

       A4: ( Sum e) = 1

      proof

        consider f be Real_Sequence such that

         A5: (f . 1) = (e . 1) and

         A6: for n be Nat st 0 <> n & n < ( len e) holds (f . (n + 1)) = ((f . n) + (e . (n + 1))) and

         A7: ( Sum e) = (f . ( len e)) by A1, NAT_1: 14, PROB_3: 63;

        for n st n <> 0 & n <= ( len e) holds (f . n) = 1

        proof

          defpred p[ Nat] means $1 <> 0 & $1 <= ( len e) implies (f . $1) = 1;

           A8:

          now

            let k be Nat such that

             A9: p[k];

            now

              assume that (k + 1) <> 0 and

               A10: (k + 1) <= ( len e);

              per cases by A10, NAT_1: 13;

                suppose

                 A11: k = 0 & k < ( len e);

                1 in ( Seg 1) & 1 in ( Seg n) by A3;

                hence (f . (k + 1)) = 1 by A2, A5, A11;

              end;

                suppose

                 A12: k > 0 & k < ( len e);

                then k >= 1 by NAT_1: 14;

                then (k + 1) > 1 by NAT_1: 13;

                then

                 A13: (k + 1) in ( Seg n) & not (k + 1) in ( Seg 1) by A1, A10, FINSEQ_1: 1;

                

                thus (f . (k + 1)) = (1 + (e . (k + 1))) by A6, A9, A12

                .= (1 + 0 ) by A2, A13

                .= 1;

              end;

            end;

            hence p[(k + 1)];

          end;

          

           A14: p[ 0 ];

          for n holds p[n] from NAT_1:sch 2( A14, A8);

          hence thesis;

        end;

        hence thesis by A1, A7;

      end;

      take e;

      for i st i in ( dom e) holds (e . i) >= 0

      proof

        let i;

        assume i in ( dom e);

        then i in ( Seg n) by A1, FINSEQ_1:def 3;

        hence thesis by A2;

      end;

      hence thesis by A1, A4;

    end;

    definition

      let p be real-valued FinSequence;

      :: MATRPROB:def5

      attr p is ProbFinS means

      : Def5: (for i st i in ( dom p) holds (p . i) >= 0 ) & ( Sum p) = 1;

    end

    registration

      cluster non empty ProbFinS for FinSequence of REAL ;

      existence

      proof

        consider p be FinSequence of REAL such that

         A1: (( len p) = 1 & for i st i in ( dom p) holds (p . i) >= 0 ) & ( Sum p) = 1 by Th52;

        take p;

        thus thesis by A1;

      end;

    end

    registration

      cluster non empty ProbFinS for real-valued FinSequence;

      existence

      proof

        take the non empty ProbFinS FinSequence of REAL ;

        thus thesis;

      end;

    end

    theorem :: MATRPROB:53

    for p be non empty ProbFinS real-valued FinSequence holds for k st k in ( dom p) holds (p . k) <= 1

    proof

      let p be non empty ProbFinS real-valued FinSequence;

      ( Sum p) = 1 & for i be Nat st i in ( dom p) holds (p . i) >= 0 by Def5;

      hence thesis by Th5;

    end;

    theorem :: MATRPROB:54

    

     Th54: for M be non empty-yielding Matrix of D holds 1 <= ( len M) & 1 <= ( width M)

    proof

      let M be non empty-yielding Matrix of D;

      ( not ( len M) = 0 ) & not ( width M) = 0 by MATRIX_0:def 10;

      hence thesis by NAT_1: 14;

    end;

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def6

      attr M is m-nonnegative means

      : Def6: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 ;

    end

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def7

      attr M is with_sum=1 means

      : Def7: ( SumAll M) = 1;

    end

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def8

      attr M is Joint_Probability means M is m-nonnegative with_sum=1;

    end

    registration

      cluster Joint_Probability -> m-nonnegative with_sum=1 for Matrix of REAL ;

      coherence ;

      cluster m-nonnegative with_sum=1 -> Joint_Probability for Matrix of REAL ;

      coherence ;

    end

    theorem :: MATRPROB:55

    

     Th55: for n,m be non zero Nat holds ex M be Matrix of n, m, REAL st M is m-nonnegative & ( SumAll M) = 1

    proof

      let n,m be non zero Nat;

      consider m1 be Nat such that

       A1: m = (m1 + 1) by NAT_1: 6;

      consider n1 be Nat such that

       A2: n = (n1 + 1) by NAT_1: 6;

      reconsider n, m as non zero Nat;

      reconsider m1, n1 as Nat;

      consider e1 be FinSequence of REAL such that

       A3: ( len e1) = m and

       A4: for i be Nat st i in ( Seg m) holds (i in ( Seg m1) implies (e1 . i) = zz) & ( not i in ( Seg m1) implies (e1 . i) = jj) by Th2;

      (m1 + 1) > m1 by NAT_1: 13;

      then

       A5: not (m1 + 1) in ( Seg m1) by FINSEQ_1: 1;

      (m1 + 1) in ( Seg m) by A1, FINSEQ_1: 4;

      then (e1 . (m1 + 1)) = 1 by A4, A5;

      then

       A6: e1 = ((e1 | m1) ^ <*1*>) by A1, A3, RFINSEQ: 7;

      reconsider e3 = (e1 | m1) as FinSequence of REAL ;

      m > m1 by A1, NAT_1: 13;

      then

       A7: ( len e3) = m1 by A3, FINSEQ_1: 59;

      

       A8: ( dom e1) = ( Seg m) by A3, FINSEQ_1:def 3;

      

       A9: ( Sum e1) = 1

      proof

        per cases ;

          suppose m1 = 0 ;

          then

           A10: ( Sum e3) = 0 by RVSUM_1: 72;

          

          thus ( Sum e1) = (( Sum (e1 | m1)) + 1) by A6, RVSUM_1: 74

          .= 1 by A10;

        end;

          suppose

           A11: m1 <> 0 ;

          for i be Nat st i in ( dom e3) holds (e3 . i) = 0

          proof

            let i be Nat;

            assume i in ( dom e3);

            then

             A12: i in ( Seg m1) by A7, FINSEQ_1:def 3;

            (m1 + 1) in ( Seg (m1 + 1)) by FINSEQ_1: 4;

            then m1 in ( Seg m) by A1, A11, FINSEQ_1: 61;

            then m1 in ( dom e1) by A3, FINSEQ_1:def 3;

            then (e3 . i) = (e1 . i) & i in ( dom e1) by A12, RFINSEQ: 6;

            hence thesis by A4, A8, A12;

          end;

          then e3 = (m1 |-> 0 ) by A7, A11, Th1, Lm4;

          

          then

           A13: ( Sum e3) = (m1 * 0 ) by RVSUM_1: 80

          .= 0 ;

          

          thus ( Sum e1) = (( Sum (e1 | m1)) + 1) by A6, RVSUM_1: 74

          .= 1 by A13;

        end;

      end;

      reconsider e2 = (m |-> ( In ( 0 , REAL ))) as FinSequence of REAL ;

      ( len e2) = m by CARD_1:def 7;

      then

      consider M1 be Matrix of n, m, REAL such that

       A14: for i be Nat st i in ( Seg n) holds (i in ( Seg n1) implies (M1 . i) = e2) & ( not i in ( Seg n1) implies (M1 . i) = e1) by A3, Th19;

      

       A15: ( Sum e2) = (m * 0 ) by RVSUM_1: 80

      .= 0 ;

      

       A16: ( len ( Sum M1)) = n & for i st i in ( Seg n) holds (i in ( Seg n1) implies (( Sum M1) . i) = 0 ) & ( not i in ( Seg n1) implies (( Sum M1) . i) = 1)

      proof

        

        thus

         A17: ( len ( Sum M1)) = ( len M1) by Def1

        .= n by MATRIX_0:def 2;

        let i such that

         A18: i in ( Seg n);

        

         A19: i in ( dom ( Sum M1)) by A17, A18, FINSEQ_1:def 3;

        thus i in ( Seg n1) implies (( Sum M1) . i) = 0

        proof

          assume

           A20: i in ( Seg n1);

          

          thus (( Sum M1) . i) = ( Sum (M1 . i)) by A19, Def1

          .= 0 by A14, A15, A18, A20;

        end;

        assume

         A21: not i in ( Seg n1);

        

        thus (( Sum M1) . i) = ( Sum (M1 . i)) by A19, Def1

        .= 1 by A14, A9, A18, A21;

      end;

      

       A22: ( SumAll M1) = 1

      proof

        reconsider e4 = ( Sum M1) as FinSequence of REAL ;

        reconsider e5 = (e4 | n1) as FinSequence of REAL ;

        (n1 + 1) > n1 by NAT_1: 13;

        then

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

        (n1 + 1) in ( Seg n) by A2, FINSEQ_1: 4;

        then

         A24: (e4 . (n1 + 1)) = 1 by A16, A23;

        n > n1 by A2, NAT_1: 13;

        then

         A25: ( len e5) = n1 by A16, FINSEQ_1: 59;

        

         A26: ( dom e4) = ( Seg n) by A16, FINSEQ_1:def 3;

        ( Sum e4) = 1

        proof

          per cases ;

            suppose n1 = 0 ;

            then

             A27: e5 = ( <*> REAL );

            

            thus ( Sum e4) = ( Sum ((e4 | n1) ^ <*1*>)) by A2, A16, A24, RFINSEQ: 7

            .= (( Sum (e4 | n1)) + 1) by RVSUM_1: 74

            .= 1 by A27, RVSUM_1: 72;

          end;

            suppose

             A28: n1 <> 0 ;

            for i be Nat st i in ( dom e5) holds (e5 . i) = 0

            proof

              let i be Nat;

              assume i in ( dom e5);

              then

               A29: i in ( Seg n1) by A25, FINSEQ_1:def 3;

              (n1 + 1) in ( Seg (n1 + 1)) by FINSEQ_1: 4;

              then n1 in ( Seg n) by A2, A28, FINSEQ_1: 61;

              then n1 in ( dom e4) by A16, FINSEQ_1:def 3;

              then (e5 . i) = (e4 . i) & i in ( dom e4) by A29, RFINSEQ: 6;

              hence thesis by A16, A26, A29;

            end;

            then e5 = (n1 |-> 0 ) by A25, A28, Th1, Lm4;

            

            then

             A30: ( Sum e5) = (n1 * 0 ) by RVSUM_1: 80

            .= 0 ;

            

            thus ( Sum e4) = ( Sum ((e4 | n1) ^ <*1*>)) by A2, A16, A24, RFINSEQ: 7

            .= (( Sum (e4 | n1)) + 1) by RVSUM_1: 74

            .= 1 by A30;

          end;

        end;

        hence thesis;

      end;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) >= 0

      proof

        let i, j such that

         A31: [i, j] in ( Indices M1);

        consider p1 be FinSequence of REAL such that

         A32: p1 = (M1 . i) and

         A33: (M1 * (i,j)) = (p1 . j) by A31, MATRIX_0:def 5;

        

         A34: ( len M1) = n by MATRIX_0:def 2;

        

         A35: [i, j] in [:( dom M1), ( Seg ( width M1)):] by A31, MATRIX_0:def 4;

        then i in ( dom M1) by ZFMISC_1: 87;

        then

         A36: i in ( Seg n) by A34, FINSEQ_1:def 3;

        j in ( Seg ( width M1)) by A35, ZFMISC_1: 87;

        then

         A37: j in ( Seg m) by A34, MATRIX_0: 20;

        per cases by A14, A32, A36;

          suppose p1 = e2;

          hence thesis by A33;

        end;

          suppose p1 = e1;

          hence thesis by A4, A33, A37;

        end;

      end;

      then M1 is m-nonnegative;

      hence thesis by A22;

    end;

    registration

      cluster non empty-yielding Joint_Probability for Matrix of REAL ;

      existence

      proof

        set n = 1, m = 1;

        consider M be Matrix of n, m, REAL such that

         A1: M is m-nonnegative and

         A2: ( SumAll M) = 1 by Th55;

        take M;

        

         A3: M is with_sum=1 by A2;

        

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

        then ( width M) = 1 by MATRIX_0: 20;

        hence thesis by A1, A4, A3, MATRIX_0:def 10;

      end;

    end

    theorem :: MATRPROB:56

    

     Th56: for M be non empty-yielding Joint_Probability Matrix of REAL holds (M @ ) is non empty-yielding Joint_Probability Matrix of REAL

    proof

      let M be non empty-yielding Joint_Probability Matrix of REAL ;

      set n = ( len M);

      set m = ( width M);

      

       A1: n > 0 by Th54;

      

       A2: m > 0 by Th54;

      then

       A3: ( len (M @ )) = m & ( width (M @ )) = n by MATRIX_0: 54;

      then

      reconsider M1 = (M @ ) as Matrix of m, n, REAL by MATRIX_0: 51;

      for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) >= 0

      proof

        let i, j;

        assume [i, j] in ( Indices M1);

        then

         A4: [j, i] in ( Indices M) by MATRIX_0:def 6;

        then (M1 * (i,j)) = (M * (j,i)) by MATRIX_0:def 6;

        hence thesis by A4, Def6;

      end;

      then

       A5: M1 is m-nonnegative;

      ( SumAll M1) = ( SumAll M) by Th28

      .= 1 by Def7;

      then M1 is with_sum=1;

      hence thesis by A1, A2, A3, A5, MATRIX_0:def 10;

    end;

    theorem :: MATRPROB:57

    for M be non empty-yielding Joint_Probability Matrix of REAL holds for i, j st [i, j] in ( Indices M) holds (M * (i,j)) <= 1

    proof

      let M be non empty-yielding Joint_Probability Matrix of REAL ;

      

       A1: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by Def6;

      

       A2: for i be Nat st i in ( dom ( Sum M)) holds (( Sum M) . i) >= 0

      proof

        let i be Nat such that

         A3: i in ( dom ( Sum M));

        i in ( Seg ( len ( Sum M))) by A3, FINSEQ_1:def 3;

        then i in ( Seg ( len M)) by Def1;

        then i in ( dom M) by FINSEQ_1:def 3;

        then for j be Nat st j in ( dom (M . i)) holds ((M . i) . j) >= 0 by A1, Lm1;

        then ( Sum (M . i)) >= 0 by RVSUM_1: 84;

        hence thesis by A3, Def1;

      end;

      

       A4: for i st i in ( dom ( Sum M)) holds (( Sum M) . i) <= 1

      proof

        let i;

        assume i in ( dom ( Sum M));

        then (( Sum M) . i) <= ( SumAll M) by A2, Th5;

        hence thesis by Def7;

      end;

      

       A5: for i st i in ( dom M) holds for j st j in ( dom (M . i)) holds ((M . i) . j) <= ( Sum (M . i))

      proof

        let i;

        assume i in ( dom M);

        then for j be Nat st j in ( dom (M . i)) holds ((M . i) . j) >= 0 by A1, Lm1;

        hence thesis by Th5;

      end;

      

       A6: for i st i in ( dom M) holds for j st j in ( dom (M . i)) holds ((M . i) . j) <= 1

      proof

        let i such that

         A7: i in ( dom M);

        i in ( Seg ( len M)) by A7, FINSEQ_1:def 3;

        then i in ( Seg ( len ( Sum M))) by Def1;

        then

         A8: i in ( dom ( Sum M)) by FINSEQ_1:def 3;

        then (( Sum M) . i) <= 1 by A4;

        then

         A9: ( Sum (M . i)) <= 1 by A8, Def1;

        let j;

        assume j in ( dom (M . i));

        then ((M . i) . j) <= ( Sum (M . i)) by A5, A7;

        hence thesis by A9, XXREAL_0: 2;

      end;

      let i, j such that

       A10: [i, j] in ( Indices M);

      

       A11: ex p1 be FinSequence of REAL st p1 = (M . i) & (M * (i,j)) = (p1 . j) by A10, MATRIX_0:def 5;

      i in ( Seg ( len M)) by A10, Th12;

      then

       A12: i in ( dom M) by FINSEQ_1:def 3;

      j in ( Seg ( width M)) by A10, Th12;

      then j in ( Seg ( len (M . i))) by A12, MATRIX_0: 36;

      then j in ( dom (M . i)) by FINSEQ_1:def 3;

      hence thesis by A6, A12, A11;

    end;

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def9

      attr M is with_line_sum=1 means

      : Def9: for k st k in ( dom M) holds ( Sum (M . k)) = 1;

    end

    theorem :: MATRPROB:58

    

     Th58: for n,m be non zero Nat holds ex M be Matrix of n, m, REAL st M is m-nonnegative with_line_sum=1

    proof

      let n,m be non zero Nat;

      consider m1 be Nat such that

       A1: m = (m1 + 1) by NAT_1: 6;

      reconsider m1 as Nat;

      consider e1 be FinSequence of REAL such that

       A2: ( len e1) = m and

       A3: for i be Nat st i in ( Seg m) holds (i in ( Seg m1) implies (e1 . i) = zz) & ( not i in ( Seg m1) implies (e1 . i) = jj) by Th2;

      (m1 + 1) > m1 by NAT_1: 13;

      then

       A4: not (m1 + 1) in ( Seg m1) by FINSEQ_1: 1;

      (m1 + 1) in ( Seg m) by A1, FINSEQ_1: 4;

      then (e1 . (m1 + 1)) = 1 by A3, A4;

      then

       A5: e1 = ((e1 | m1) ^ <*1*>) by A1, A2, RFINSEQ: 7;

      reconsider M1 = (n |-> e1) as Matrix of n, m, REAL by A2, Th18;

      

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

      

       A7: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) >= 0

      proof

        let i, j such that

         A8: [i, j] in ( Indices M1);

        consider p1 be FinSequence of REAL such that

         A9: p1 = (M1 . i) and

         A10: (M1 * (i,j)) = (p1 . j) by A8, MATRIX_0:def 5;

        

         A11: [i, j] in [:( dom M1), ( Seg ( width M1)):] by A8, MATRIX_0:def 4;

        then j in ( Seg ( width M1)) by ZFMISC_1: 87;

        then

         A12: j in ( Seg m) by A6, MATRIX_0: 20;

        i in ( dom M1) by A11, ZFMISC_1: 87;

        then i in ( Seg n) by A6, FINSEQ_1:def 3;

        then p1 = e1 by A9, FUNCOP_1: 7;

        hence thesis by A3, A10, A12;

      end;

      reconsider e3 = (e1 | m1) as FinSequence of REAL ;

      m > m1 by A1, NAT_1: 13;

      then

       A13: ( len e3) = m1 by A2, FINSEQ_1: 59;

      take M1;

      

       A14: ( dom e1) = ( Seg m) by A2, FINSEQ_1:def 3;

      

       A15: ( Sum e1) = 1

      proof

        per cases ;

          suppose m1 = 0 ;

          then

           A16: e3 = ( <*> REAL );

          

          thus ( Sum e1) = (( Sum (e1 | m1)) + 1) by A5, RVSUM_1: 74

          .= 1 by A16, RVSUM_1: 72;

        end;

          suppose

           A17: m1 <> 0 ;

          for i be Nat st i in ( dom e3) holds (e3 . i) = 0

          proof

            let i be Nat;

            assume i in ( dom e3);

            then

             A18: i in ( Seg m1) by A13, FINSEQ_1:def 3;

            (m1 + 1) in ( Seg (m1 + 1)) by FINSEQ_1: 4;

            then m1 in ( Seg m) by A1, A17, FINSEQ_1: 61;

            then m1 in ( dom e1) by A2, FINSEQ_1:def 3;

            then (e3 . i) = (e1 . i) & i in ( dom e1) by A18, RFINSEQ: 6;

            hence thesis by A3, A14, A18;

          end;

          then e3 = (m1 |-> 0 ) by A13, A17, Th1, Lm4;

          

          then

           A19: ( Sum e3) = (m1 * 0 ) by RVSUM_1: 80

          .= 0 ;

          

          thus ( Sum e1) = (( Sum (e1 | m1)) + 1) by A5, RVSUM_1: 74

          .= 1 by A19;

        end;

      end;

      for i st i in ( dom M1) holds ( Sum (M1 . i)) = 1

      proof

        let i;

        assume i in ( dom M1);

        then i in ( Seg n) by A6, FINSEQ_1:def 3;

        hence thesis by A15, FUNCOP_1: 7;

      end;

      hence thesis by A7;

    end;

    definition

      let M be Matrix of REAL ;

      :: MATRPROB:def10

      attr M is Conditional_Probability means M is m-nonnegative with_line_sum=1;

    end

    registration

      cluster Conditional_Probability -> m-nonnegative with_line_sum=1 for Matrix of REAL ;

      coherence ;

      cluster m-nonnegative with_line_sum=1 -> Conditional_Probability for Matrix of REAL ;

      coherence ;

    end

    registration

      cluster non empty-yielding Conditional_Probability for Matrix of REAL ;

      existence

      proof

        set n = 1, m = 1;

        consider M be Matrix of n, m, REAL such that

         A1: M is m-nonnegative with_line_sum=1 by Th58;

        take M;

        

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

        then ( width M) = 1 by MATRIX_0: 20;

        hence thesis by A1, A2, MATRIX_0:def 10;

      end;

    end

    theorem :: MATRPROB:59

    for M be non empty-yielding Conditional_Probability Matrix of REAL holds for i, j st [i, j] in ( Indices M) holds (M * (i,j)) <= 1

    proof

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      

       A1: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by Def6;

      

       A2: for i st i in ( dom M) holds for j st j in ( dom (M . i)) holds ((M . i) . j) <= 1

      proof

        let i such that

         A3: i in ( dom M);

        

         A4: for j be Nat st j in ( dom (M . i)) holds ((M . i) . j) >= 0 by A1, A3, Lm1;

        let j;

        assume j in ( dom (M . i));

        then ((M . i) . j) <= ( Sum (M . i)) by A4, Th5;

        hence thesis by A3, Def9;

      end;

      let i, j such that

       A5: [i, j] in ( Indices M);

      

       A6: ex p1 be FinSequence of REAL st p1 = (M . i) & (M * (i,j)) = (p1 . j) by A5, MATRIX_0:def 5;

      i in ( Seg ( len M)) by A5, Th12;

      then

       A7: i in ( dom M) by FINSEQ_1:def 3;

      j in ( Seg ( width M)) by A5, Th12;

      then j in ( Seg ( len (M . i))) by A7, MATRIX_0: 36;

      then j in ( dom (M . i)) by FINSEQ_1:def 3;

      hence thesis by A2, A7, A6;

    end;

    theorem :: MATRPROB:60

    

     Th60: for M be non empty-yielding Matrix of REAL holds M is non empty-yielding Conditional_Probability Matrix of REAL iff for i st i in ( dom M) holds ( Line (M,i)) is non empty ProbFinS FinSequence of REAL

    proof

      let M be non empty-yielding Matrix of REAL ;

      hereby

        assume

         A1: M is non empty-yielding Conditional_Probability Matrix of REAL ;

        hereby

          set m = ( width M);

          let i such that

           A2: i in ( dom M);

          for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by A1, Def6;

          then

           A3: ( len ( Line (M,i))) = m & for j st j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) >= 0 by A2, Lm2, MATRIX_0:def 7;

          ( Sum ( Line (M,i))) = ( Sum (M . i)) by A2, MATRIX_0: 60

          .= 1 by A1, A2, Def9;

          hence ( Line (M,i)) is non empty ProbFinS FinSequence of REAL by A3, Def5, Th54;

        end;

      end;

      assume

       A4: for i st i in ( dom M) holds ( Line (M,i)) is non empty ProbFinS FinSequence of REAL ;

      now

        let k such that

         A5: k in ( dom M);

        ( Line (M,k)) is ProbFinS by A4, A5;

        then ( Sum ( Line (M,k))) = 1;

        hence ( Sum (M . k)) = 1 by A5, MATRIX_0: 60;

      end;

      then

       A6: M is with_line_sum=1;

      for i, j st i in ( dom M) & j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) >= 0

      proof

        let i, j such that

         A7: i in ( dom M) and

         A8: j in ( dom ( Line (M,i)));

        ( Line (M,i)) is ProbFinS by A4, A7;

        hence thesis by A8;

      end;

      then for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by Lm2;

      then M is m-nonnegative;

      hence thesis by A6;

    end;

    theorem :: MATRPROB:61

    for M be non empty-yielding with_line_sum=1 Matrix of REAL holds ( SumAll M) = ( len M)

    proof

      let M be non empty-yielding with_line_sum=1 Matrix of REAL ;

      set n = ( len M);

      

       A1: ( len ( Sum M)) = n & for i be Nat st i in ( dom ( Sum M)) holds (( Sum M) . i) = 1

      proof

        thus ( len ( Sum M)) = n by Def1;

        hereby

          let i be Nat;

          assume

           A2: i in ( dom ( Sum M));

          then i in ( Seg ( len ( Sum M))) by FINSEQ_1:def 3;

          then i in ( Seg ( len M)) by Def1;

          then i in ( dom M) by FINSEQ_1:def 3;

          then ( Sum (M . i)) = 1 by Def9;

          hence (( Sum M) . i) = 1 by A2, Def1;

        end;

      end;

      n > 0 by Th54;

      then ( Sum M) = (n |-> jj) by A1, Th1;

      

      hence ( SumAll M) = (n * 1) by RVSUM_1: 80

      .= n;

    end;

    notation

      let M be Matrix of REAL ;

      synonym Row_Marginal M for LineSum M;

      synonym Column_Marginal M for ColSum M;

    end

    registration

      let M be non empty-yielding Joint_Probability Matrix of REAL ;

      cluster ( Row_Marginal M) -> non empty ProbFinS;

      coherence

      proof

        set n = ( len M);

        set e = ( LineSum M);

        

         A1: ( len e) = ( len M) by Th20;

        

         A2: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by Def6;

        

         A3: for i st i in ( dom e) holds (e . i) >= 0

        proof

          let i;

          assume i in ( dom e);

          then

           A4: i in ( Seg ( len M)) by A1, FINSEQ_1:def 3;

          then i in ( dom M) by FINSEQ_1:def 3;

          then for j be Nat st j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) >= 0 by A2, Lm2;

          then ( Sum ( Line (M,i))) >= 0 by RVSUM_1: 84;

          hence thesis by A4, Th20;

        end;

        

         A5: ( Sum e) = ( SumAll M)

        .= 1 by Def7;

        ( len e) = n by Th20;

        hence thesis by A3, A5, Th54;

      end;

      cluster ( Column_Marginal M) -> non empty ProbFinS;

      coherence

      proof

        set e = ( ColSum M);

        set m = ( width M);

        

         A6: ( len e) = ( width M) by Def2;

        

         A7: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) >= 0 by Def6;

        

         A8: for i st i in ( dom e) holds (e . i) >= 0

        proof

          let i;

          assume i in ( dom e);

          then

           A9: i in ( Seg ( width M)) by A6, FINSEQ_1:def 3;

          then for j be Nat st j in ( dom ( Col (M,i))) holds (( Col (M,i)) . j) >= 0 by A7, Lm3;

          then ( Sum ( Col (M,i))) >= 0 by RVSUM_1: 84;

          hence thesis by A9, Def2;

        end;

        

         A10: ( len e) = m by Def2;

        ( Sum e) = ( SumAll M) by Th29

        .= 1 by Def7;

        hence thesis by A10, A8, Th54;

      end;

    end

    registration

      let M be non empty-yielding Matrix of REAL ;

      cluster (M @ ) -> non empty-yielding;

      coherence

      proof

        

         A1: ( width M) <> 0 by MATRIX_0:def 10;

        then ( width (M @ )) = ( len M) by MATRIX_0: 54;

        then

         A2: ( width (M @ )) <> 0 by MATRIX_0:def 10;

        ( len (M @ )) <> 0 by A1, MATRIX_0: 54;

        hence thesis by A2, MATRIX_0:def 10;

      end;

    end

    registration

      let M be non empty-yielding Joint_Probability Matrix of REAL ;

      cluster (M @ ) -> Joint_Probability;

      coherence by Th56;

    end

    theorem :: MATRPROB:62

    

     Th62: for p be non empty ProbFinS FinSequence of REAL holds for P be non empty-yielding Conditional_Probability Matrix of REAL st ( len p) = ( len P) holds (p * P) is non empty ProbFinS FinSequence of REAL & ( len (p * P)) = ( width P)

    proof

      let p be non empty ProbFinS FinSequence of REAL ;

      set n = ( len p);

      let P be non empty-yielding Conditional_Probability Matrix of REAL such that

       A1: ( len p) = ( len P);

      

       A2: ( len (p * P)) = ( width P) by A1, MATRIXR1: 62;

      

       A3: for i st i in ( dom (p * P)) holds ((p * P) . i) >= 0

      proof

        let i such that

         A4: i in ( dom (p * P));

        i in ( Seg ( len (p * P))) by A4, FINSEQ_1:def 3;

        

        then

         A5: ((p * P) . i) = (p "*" ( Col (P,i))) by A1, Th40

        .= ( Sum ( mlt (p,( Col (P,i)))));

        

         A6: for i, j st [i, j] in ( Indices P) holds (P * (i,j)) >= 0 by Def6;

        i in ( Seg ( width P)) by A2, A4, FINSEQ_1:def 3;

        then

         A7: for j st j in ( dom ( Col (P,i))) holds (( Col (P,i)) . j) >= 0 by A6, Lm3;

        for i st i in ( dom p) holds (p . i) >= 0 by Def5;

        then for k be Nat st k in ( dom ( mlt (p,( Col (P,i))))) holds (( mlt (p,( Col (P,i)))) . k) >= 0 by A7, Th33;

        hence thesis by A5, RVSUM_1: 84;

      end;

      set m = ( width P);

      set e = (m |-> jj);

      

       A8: ( len e) = m by CARD_1:def 7;

      

       A9: m > 0 by Th54;

      then

       A10: ( len (P @ )) = ( width P) by MATRIX_0: 54;

      ( width (P @ )) = ( len P) by A9, MATRIX_0: 54;

      then

       A11: ( len (e * (P @ ))) = n by A1, A8, A10, MATRIXR1: 62;

      for k be Nat st k in ( dom (e * (P @ ))) holds ((e * (P @ )) . k) = 1

      proof

        let k be Nat;

        assume k in ( dom (e * (P @ )));

        then

         A12: k in ( Seg ( len (e * (P @ )))) by FINSEQ_1:def 3;

        then

         A13: k in ( dom P) by A1, A11, FINSEQ_1:def 3;

        

        thus ((e * (P @ )) . k) = ( Sum ( Col ((P @ ),k))) by A8, A10, A12, Th50

        .= ( Sum ( Line (P,k))) by A13, MATRIX_0: 58

        .= ( Sum (P . k)) by A13, MATRIX_0: 60

        .= 1 by A13, Def9;

      end;

      then

       A14: (e * (P @ )) = (n |-> jj) by A11, Th1;

      ( Sum (p * P)) = |((p * P), e)| by A2, Th32

      .= |(p, (e * (P @ )))| by A1, A9, A8, Th49

      .= ( Sum p) by A14, Th32

      .= 1 by Def5;

      hence thesis by A2, A3, Def5, Th54;

    end;

    theorem :: MATRPROB:63

    for P1,P2 be non empty-yielding Conditional_Probability Matrix of REAL st ( width P1) = ( len P2) holds (P1 * P2) is non empty-yielding Conditional_Probability Matrix of REAL & ( len (P1 * P2)) = ( len P1) & ( width (P1 * P2)) = ( width P2)

    proof

      let P1,P2 be non empty-yielding Conditional_Probability Matrix of REAL such that

       A1: ( width P1) = ( len P2);

      set n2 = ( width P2);

      set m = ( len P2);

      set n1 = ( len P1);

      

       A2: ( len (P1 * P2)) = n1 by A1, Th42;

      

       A3: ( width (P1 * P2)) = n2 by A1, Th42;

      then

      reconsider P = (P1 * P2) as Matrix of n1, n2, REAL by A2, MATRIX_0: 51;

      

       A4: for i st i in ( dom P) holds ( Line (P,i)) is non empty ProbFinS FinSequence of REAL

      proof

        let i;

        assume i in ( dom P);

        then

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

        then i in ( dom P1) by A2, FINSEQ_1:def 3;

        then

        reconsider p = ( Line (P1,i)) as non empty ProbFinS FinSequence of REAL by Th60;

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

        then (p * P2) is non empty ProbFinS FinSequence of REAL by Th62;

        hence thesis by A1, A5, Th42;

      end;

      n1 > 0 & n2 > 0 by Th54;

      then P is non empty-yielding Matrix of REAL by A2, A3, MATRIX_0:def 10;

      hence thesis by A1, A4, Th42, Th60;

    end;