entropy1.miz



    begin

    reserve D for non empty set,

i,j,k,l for Nat,

n for Nat,

x for set,

a,b,c,r,r1,r2 for Real,

p,q for FinSequence of REAL ,

MR,MR1 for Matrix of REAL ;

    theorem :: ENTROPY1:1

    

     Th1: k <> 0 & i < l & l <= j & k divides l implies (i div k) < (j div k)

    proof

      assume that

       A1: k <> 0 and

       A2: i < l and

       A3: l <= j and

       A4: k divides l;

      

       A5: (l mod k) = 0 by A1, A4, PEPIN: 6;

      (i + (i mod k)) >= i by NAT_1: 11;

      then (i - (i mod k)) <= ((i + (i mod k)) - (i mod k)) by XREAL_1: 9;

      then (i - (i mod k)) < l by A2, XXREAL_0: 2;

      then

       A6: ((i - (i mod k)) / k) < (l / k) by A1, XREAL_1: 74;

      i = ((k * (i div k)) + (i mod k)) by A1, NAT_D: 2;

      then ((k / k) * (i div k)) = ((i - (i mod k)) / k);

      then

       A7: (1 * (i div k)) = ((i - (i mod k)) / k) by A1, XCMPLX_1: 60;

      l = ((k * (l div k)) + (l mod k)) by A1, NAT_D: 2

      .= (k * (l div k)) by A5;

      then ((k / k) * (l div k)) = (l / k);

      then

       A8: (1 * (l div k)) = (l / k) by A1, XCMPLX_1: 60;

      (l div k) <= (j div k) by A3, NAT_2: 24;

      hence thesis by A8, A7, A6, XXREAL_0: 2;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    theorem :: ENTROPY1:2

    

     Th2: r > 0 implies ( ln . r) <= (r - 1) & (r = 1 iff ( ln . r) = (r - 1)) & (r <> 1 iff ( ln . r) < (r - 1))

    proof

      set Z2 = ]. 0 , 1.[;

      set Z1 = ( right_open_halfline 1);

      reconsider f2 = ( log_ number_e ) as PartFunc of REAL , REAL ;

      deffunc G( Real) = ( In (($1 - 1), REAL ));

      defpred P[ object] means $1 in REAL ;

      set Z = ( right_open_halfline 0 );

      

       A1: 1 in Z by XXREAL_1: 235;

      1 in { g where g be Real : 0 < g };

      then

       A2: 1 in Z by XXREAL_1: 230;

      consider f1 be PartFunc of REAL , REAL such that

       A3: (for r be Element of REAL holds r in ( dom f1) iff P[r]) & for r be Element of REAL st r in ( dom f1) holds (f1 . r) = G(r) from SEQ_1:sch 3;

      

       A4: for r be Real holds r in ( dom f1) iff P[r] by XREAL_0:def 1, A3;

      ( dom f1) is Subset of REAL by RELAT_1:def 18;

      then

       A5: ( dom f1) = REAL by A4, FDIFF_1: 1;

      

       A6: for r st r in Z holds (f1 . r) = ((1 * r) + ( - 1))

      proof

        let r such that r in Z;

        reconsider r as Element of REAL by XREAL_0:def 1;

        (f1 . r) = G(r) by A3;

        hence thesis;

      end;

      then

       A7: f1 is_differentiable_on Z by A5, FDIFF_1: 23;

      set f = (f1 - f2);

      

       A8: number_e <> 1 by TAYLOR_1: 11;

      assume

       A9: r > 0 ;

      ( dom f2) = Z by TAYLOR_1:def 2;

      

      then

       A10: ( dom f) = (Z /\ REAL ) by A5, VALUED_1: 12

      .= Z by XBOOLE_1: 28;

      

       A11: for x be Element of REAL st x > 0 holds (f . x) = ((x - 1) - ( ln . x))

      proof

        let x be Element of REAL ;

        assume x > 0 ;

        then x in { g where g be Real : 0 < g };

        then

         A12: x in ( dom f) by A10, XXREAL_1: 230;

        (f . x) = ((f1 . x) - (f2 . x)) by A12, VALUED_1: 13

        .= ( G(x) - (f2 . x)) by A3;

        hence thesis;

      end;

      

      then

       A13: (f . 1) = ((1 - 1) - ( ln . jj))

      .= ( - ( log ( number_e ,1))) by A2, TAYLOR_1:def 2

      .= ( - 0 ) by A8, POWER: 51, TAYLOR_1: 11

      .= 0 ;

      

       A14: f1 is_differentiable_on Z by A5, A6, FDIFF_1: 23;

       A15:

      now

        let r such that

         A16: r in Z;

        

        thus ( diff (f1,r)) = ((f1 `| Z) . r) by A14, A16, FDIFF_1:def 7

        .= 1 by A5, A6, A16, FDIFF_1: 23;

      end;

      

       A17: f is_differentiable_on Z & for r st r in Z holds ( diff (f,r)) = (1 - (1 / r))

      proof

        thus

         A18: f is_differentiable_on Z by A10, A7, FDIFF_1: 19, TAYLOR_1: 18;

        hereby

          let r such that

           A19: r in Z;

          (((f1 - f2) `| Z) . r) = (( diff (f1,r)) - ( diff (f2,r))) by A10, A7, A19, FDIFF_1: 19, TAYLOR_1: 18

          .= (1 - ( diff (f2,r))) by A15, A19

          .= (1 - (1 / r)) by A19, TAYLOR_1: 18;

          hence ( diff (f,r)) = (1 - (1 / r)) by A18, A19, FDIFF_1:def 7;

        end;

      end;

      then

       A20: (f | Z) is continuous by FDIFF_1: 25;

      

       A21: Z1 c= Z by XXREAL_1: 46;

      

       A22: for r st r in Z1 holds ( diff (f,r)) > 0

      proof

        let r such that

         A23: r in Z1;

        r in { g where g be Real : 1 < g } by A23, XXREAL_1: 230;

        then

         A24: ex g1 be Real st g1 = r & 1 < g1;

        ( diff (f,r)) = (1 - (1 / r)) by A17, A21, A23;

        hence thesis by A24, XREAL_1: 50, XREAL_1: 212;

      end;

      

       A25: for r st r in Z1 holds (f . r) > 0

      proof

        assume not for r st r in Z1 holds (f . r) > 0 ;

        then

        consider r1 such that

         A26: r1 in Z1 and

         A27: (f . r1) <= 0 ;

        

         A28: [.1, r1.] c= ( dom f) by A1, A10, A21, A26, XXREAL_2:def 12;

        r1 in { g where g be Real : 1 < g } by A26, XXREAL_1: 230;

        then

         A29: ex g1 be Real st g1 = r1 & 1 < g1;

        

         A30: f is_differentiable_on ].1, r1.[ by A17, FDIFF_1: 26, XXREAL_1: 247;

        

         A31: (f | [.1, r1.]) is continuous by A20, FCONT_1: 16, XXREAL_1: 249;

        per cases by A27;

          suppose (f . r1) = 0 ;

          then

          consider r2 be Real such that

           A32: r2 in ].1, r1.[ and

           A33: ( diff (f,r2)) = 0 by A13, A29, A31, A30, A28, ROLLE: 1;

          ex g1 be Real st g1 = r2 & 1 < g1 & g1 < r1 by A32;

          then r2 in { g where g be Real : 1 < g };

          then r2 in Z1 by XXREAL_1: 230;

          hence contradiction by A22, A33;

        end;

          suppose

           A34: (f . r1) < 0 ;

          consider r3 be Real such that

           A35: r3 in ].1, r1.[ and

           A36: ( diff (f,r3)) = (((f . r1) - (f . 1)) / (r1 - 1)) by A29, A31, A30, A28, ROLLE: 3;

          ex g1 be Real st g1 = r3 & 1 < g1 & g1 < r1 by A35;

          then r3 in { g where g be Real : 1 < g };

          then

           A37: r3 in Z1 by XXREAL_1: 230;

          (r1 - 1) > 0 by A29, XREAL_1: 50;

          hence contradiction by A13, A22, A34, A36, A37;

        end;

      end;

      

       A38: for r st r > 1 holds (f . r) > 0

      proof

        let r;

        assume r > 1;

        then r in { g where g be Real : 1 < g };

        then r in Z1 by XXREAL_1: 230;

        hence thesis by A25;

      end;

      

       A39: Z2 c= Z by XXREAL_1: 247;

      

       A40: for r st r in Z2 holds ( diff (f,r)) < 0

      proof

        let r;

        assume

         A41: r in Z2;

        then ex g1 be Real st g1 = r & 0 < g1 & g1 < 1;

        then

         A42: 1 < (1 / r) by XREAL_1: 187;

        ( diff (f,r)) = (1 - (1 / r)) by A17, A39, A41;

        hence thesis by A42, XREAL_1: 49;

      end;

      

       A43: for r st r in Z2 holds (f . r) > 0

      proof

        assume not for r st r in Z2 holds (f . r) > 0 ;

        then

        consider r1 such that

         A44: r1 in Z2 and

         A45: (f . r1) <= 0 ;

        

         A46: [.r1, 1.] c= ( dom f) by A1, A10, A39, A44, XXREAL_2:def 12;

        

         A47: ex g1 be Real st g1 = r1 & 0 < g1 & g1 < 1 by A44;

        then

         A48: (f | [.r1, 1.]) is continuous by A20, FCONT_1: 16, XXREAL_1: 249;

        

         A49: f is_differentiable_on ].r1, 1.[ by A17, A47, FDIFF_1: 26, XXREAL_1: 247;

        per cases by A45;

          suppose (f . r1) = 0 ;

          then

          consider r2 be Real such that

           A50: r2 in ].r1, 1.[ and

           A51: ( diff (f,r2)) = 0 by A13, A47, A48, A46, A49, ROLLE: 1;

          ex g1 be Real st g1 = r2 & r1 < g1 & g1 < 1 by A50;

          then r2 in { g where g be Real : 0 < g & g < 1 } by A47;

          hence contradiction by A40, A51;

        end;

          suppose

           A52: (f . r1) < 0 ;

          

           A53: (1 - r1) > 0 by A47, XREAL_1: 50;

          consider r3 be Real such that

           A54: r3 in ].r1, 1.[ and

           A55: ( diff (f,r3)) = (((f . 1) - (f . r1)) / (1 - r1)) by A47, A48, A46, A49, ROLLE: 3;

          ex g1 be Real st g1 = r3 & r1 < g1 & g1 < 1 by A54;

          then r3 in Z2 by A47;

          hence contradiction by A13, A40, A52, A55, A53;

        end;

      end;

      

       A56: for r st r > 0 & r < 1 holds (f . r) > 0

      proof

        let r such that

         A57: r > 0 and

         A58: r < 1;

        r in { g where g be Real : 0 < g & g < 1 } by A57, A58;

        hence thesis by A43;

      end;

      reconsider rr = r as Element of REAL by XREAL_0:def 1;

      for r st r > 0 holds (f . r) >= 0

      proof

        let r such that

         A59: r > 0 ;

        per cases by XXREAL_0: 1;

          suppose r < 1;

          hence thesis by A56, A59;

        end;

          suppose r = 1;

          hence thesis by A13;

        end;

          suppose r > 1;

          hence thesis by A38;

        end;

      end;

      then (f . r) >= 0 by A9;

      then ((r - 1) - ( ln . rr)) >= 0 by A11, A9;

      then ((r - 1) - 0 ) >= ( ln . r) by XREAL_1: 11;

      hence ( ln . r) <= (r - 1);

      thus

       A60: r = 1 iff ( ln . r) = (r - 1)

      proof

        hereby

          assume r = 1;

          then ((r - 1) - ( ln . rr)) = 0 by A11, A13;

          hence ( ln . r) = (r - 1);

        end;

        assume ( ln . r) = (r - 1);

        then

         A61: ((r - 1) - ( ln . r)) = 0 ;

        assume

         A62: r <> 1;

        per cases by A62, XXREAL_0: 1;

          suppose r < 1;

          then (f . rr) > 0 by A56, A9;

          hence contradiction by A11, A9, A61;

        end;

          suppose

           A63: r > 1;

          then (f . rr) > 0 by A38;

          hence contradiction by A11, A61, A63;

        end;

      end;

      thus r <> 1 iff ( ln . r) < (r - 1)

      proof

        hereby

          assume r <> 1;

          then

           A64: (r - 1) > 0 or (1 - r) > 0 by XREAL_1: 55;

          per cases by A64, XREAL_1: 47;

            suppose r < 1;

            then (f . r) > 0 by A56, A9;

            then ((r - 1) - ( ln . rr)) > 0 by A11, A9;

            hence ( ln . r) < (r - 1) by XREAL_1: 47;

          end;

            suppose

             A65: r > 1;

            then (f . r) > 0 by A38;

            then ((r - 1) - ( ln . rr)) > 0 by A11, A65;

            hence ( ln . r) < (r - 1) by XREAL_1: 47;

          end;

        end;

        assume

         A66: ( ln . r) < (r - 1);

        assume r = 1;

        hence contradiction by A60, A66;

      end;

    end;

    theorem :: ENTROPY1:3

    

     Th3: r > 0 implies ( log ( number_e ,r)) <= (r - 1) & (r = 1 iff ( log ( number_e ,r)) = (r - 1)) & (r <> 1 iff ( log ( number_e ,r)) < (r - 1))

    proof

      assume

       A1: r > 0 ;

      then r in { g where g be Real : 0 < g };

      then r in ( right_open_halfline 0 ) by XXREAL_1: 230;

      then ( log ( number_e ,r)) = ( ln . r) by TAYLOR_1:def 2;

      hence thesis by A1, Th2;

    end;

    theorem :: ENTROPY1:4

    

     Th4: a > 1 & b > 1 implies ( log (a,b)) > 0

    proof

      assume that

       A1: a > 1 and

       A2: b > 1;

      

       A3: (a to_power ( log (a,b))) > 1 by A1, A2, POWER:def 3;

      assume

       A4: ( log (a,b)) <= 0 ;

      per cases by A4;

        suppose ( log (a,b)) = 0 ;

        hence contradiction by A3, POWER: 24;

      end;

        suppose ( log (a,b)) < 0 ;

        hence contradiction by A1, A3, POWER: 36;

      end;

    end;

    theorem :: ENTROPY1:5

    

     Th5: a > 0 & a <> 1 & b > 0 implies ( - ( log (a,b))) = ( log (a,(1 / b)))

    proof

      assume that

       A1: a > 0 and

       A2: a <> 1 and

       A3: b > 0 ;

      

      thus ( - ( log (a,b))) = ( 0 - ( log (a,b)))

      .= (( log (a,1)) - ( log (a,b))) by A1, A2, POWER: 51

      .= ( log (a,(1 / b))) by A1, A2, A3, POWER: 54;

    end;

    theorem :: ENTROPY1:6

    

     Th6: a > 0 & a <> 1 & b >= 0 & c >= 0 implies ((b * c) * ( log (a,(b * c)))) = (((b * c) * ( log (a,b))) + ((b * c) * ( log (a,c))))

    proof

      assume that

       A1: a > 0 and

       A2: a <> 1 and

       A3: b >= 0 and

       A4: c >= 0 ;

      per cases by A3, A4;

        suppose b > 0 & c = 0 ;

        hence thesis;

      end;

        suppose b = 0 & c = 0 ;

        hence thesis;

      end;

        suppose b = 0 & c > 0 ;

        hence thesis;

      end;

        suppose b > 0 & c > 0 ;

        

        hence ((b * c) * ( log (a,(b * c)))) = ((b * c) * (( log (a,b)) + ( log (a,c)))) by A1, A2, POWER: 53

        .= (((b * c) * ( log (a,b))) + ((b * c) * ( log (a,c))));

      end;

    end;

    theorem :: ENTROPY1:7

    

     Th7: for q,q1,q2 be FinSequence of REAL st ( len q1) = ( len q) & ( len q1) = ( len q2) & (for k st k in ( dom q1) holds (q . k) = ((q1 . k) + (q2 . k))) holds ( Sum q) = (( Sum q1) + ( Sum q2))

    proof

      let q,q1,q2 be FinSequence of REAL such that

       A1: ( len q1) = ( len q) and

       A2: ( len q1) = ( len q2) and

       A3: for k st k in ( dom q1) holds (q . k) = ((q1 . k) + (q2 . k));

      for k be Element of NAT st k in ( dom q1) holds (q . k) = ((q1 /. k) + (q2 /. k))

      proof

        let k be Element of NAT such that

         A4: k in ( dom q1);

        

         A5: k in ( dom q2) by A2, A4, FINSEQ_3: 29;

        

        thus (q . k) = ((q1 . k) + (q2 . k)) by A3, A4

        .= ((q1 /. k) + (q2 . k)) by A4, PARTFUN1:def 6

        .= ((q1 /. k) + (q2 /. k)) by A5, PARTFUN1:def 6;

      end;

      hence thesis by A1, A2, INTEGRA1: 21;

    end;

    theorem :: ENTROPY1:8

    

     Th8: for q,q1,q2 be FinSequence of REAL st ( len q1) = ( len q) & ( len q1) = ( len q2) & (for k st k in ( dom q1) holds (q . k) = ((q1 . k) - (q2 . k))) holds ( Sum q) = (( Sum q1) - ( Sum q2))

    proof

      let q,q1,q2 be FinSequence of REAL such that

       A1: ( len q1) = ( len q) and

       A2: ( len q1) = ( len q2) and

       A3: for k st k in ( dom q1) holds (q . k) = ((q1 . k) - (q2 . k));

      for k be Element of NAT st k in ( dom q1) holds (q . k) = ((q1 /. k) - (q2 /. k))

      proof

        let k be Element of NAT such that

         A4: k in ( dom q1);

        

         A5: k in ( dom q2) by A2, A4, FINSEQ_3: 29;

        

        thus (q . k) = ((q1 . k) - (q2 . k)) by A3, A4

        .= ((q1 /. k) - (q2 . k)) by A4, PARTFUN1:def 6

        .= ((q1 /. k) - (q2 /. k)) by A5, PARTFUN1:def 6;

      end;

      hence thesis by A1, A2, INTEGRA1: 22;

    end;

    theorem :: ENTROPY1:9

    

     Th9: ( len p) >= 1 implies ex q st ( len q) = ( len p) & (q . 1) = (p . 1) & (for k st 0 <> k & k < ( len p) holds (q . (k + 1)) = ((q . k) + (p . (k + 1)))) & ( Sum p) = (q . ( len p))

    proof

      assume

       A1: ( len p) >= 1;

      then

      consider r be Real_Sequence such that

       A2: (r . 1) = (p . 1) and

       A3: for n st 0 <> n & n < ( len p) holds (r . (n + 1)) = ((r . n) + (p . (n + 1))) and

       A4: ( Sum p) = (r . ( len p)) by PROB_3: 63;

      

       A5: 1 in ( dom p) by A1, FINSEQ_3: 25;

      deffunc F( Nat) = (r . $1);

      consider q be FinSequence such that

       A6: ( len q) = ( len p) & for k be Nat st k in ( dom q) holds (q . k) = F(k) from FINSEQ_1:sch 2;

      

       A7: ( rng q) c= REAL

      proof

        let x be object;

        assume x in ( rng q);

        then

        consider j be Nat such that

         A8: j in ( dom q) and

         A9: (q . j) = x by FINSEQ_2: 10;

         F(j) = (q . j) by A6, A8;

        hence thesis by A9, XREAL_0:def 1;

      end;

      

       A10: ( dom q) = ( dom p) by A6, FINSEQ_3: 29;

      reconsider q as FinSequence of REAL by A7, FINSEQ_1:def 4;

       A11:

      now

        let k such that

         A12: 0 <> k and

         A13: k < ( len p);

        k >= 1 by A12, NAT_1: 14;

        then

         A14: k in ( dom q) by A6, A13, FINSEQ_3: 25;

        

         A15: (k + 1) >= 1 by NAT_1: 14;

        (k + 1) <= ( len p) by A13, NAT_1: 13;

        then (k + 1) in ( dom q) by A6, A15, FINSEQ_3: 25;

        

        hence (q . (k + 1)) = (r . (k + 1)) by A6

        .= ((r . k) + (p . (k + 1))) by A3, A12, A13

        .= ((q . k) + (p . (k + 1))) by A6, A14;

      end;

      take q;

      ( len p) in ( dom q) by A1, A6, FINSEQ_3: 25;

      hence thesis by A2, A4, A6, A10, A5, A11;

    end;

    notation

      let p;

      synonym p is nonnegative for p is nonnegative-yielding;

    end

    definition

      let p;

      :: original: nonnegative

      redefine

      :: ENTROPY1:def1

      attr p is nonnegative means

      : Def1: for i st i in ( dom p) holds (p . i) >= 0 ;

      compatibility

      proof

        thus p is nonnegative implies for i st i in ( dom p) holds (p . i) >= 0 by FUNCT_1: 3;

        assume

         A1: for i st i in ( dom p) holds (p . i) >= 0 ;

        let r be Real;

        assume r in ( rng p);

        then ex j be Nat st j in ( dom p) & r = (p . j) by FINSEQ_2: 10;

        hence thesis by A1;

      end;

    end

    registration

      cluster nonnegative for FinSequence of REAL ;

      existence

      proof

        take <*1*>;

        thus thesis;

      end;

    end

    theorem :: ENTROPY1:10

    

     Th10: p is nonnegative & r >= 0 implies (r * p) is nonnegative

    proof

      assume that

       A1: p is nonnegative and

       A2: r >= 0 ;

      now

        let k;

        assume k in ( dom (r * p));

        then k in ( dom p) by VALUED_1:def 5;

        then

         A3: (p . k) >= 0 by A1;

        ((r * p) . k) = (r * (p . k)) by RVSUM_1: 44;

        hence ((r * p) . k) >= 0 by A2, A3;

      end;

      hence thesis;

    end;

    definition

      let p, k;

      :: ENTROPY1:def2

      pred p has_onlyone_value_in k means k in ( dom p) & for i st i in ( dom p) & i <> k holds (p . i) = 0 ;

    end

    theorem :: ENTROPY1:11

    p has_onlyone_value_in k & i <> k implies (p . i) = 0

    proof

      assume that

       A1: p has_onlyone_value_in k and

       A2: i <> k;

      per cases ;

        suppose not i in ( dom p);

        hence thesis by FUNCT_1:def 2;

      end;

        suppose i in ( dom p);

        hence thesis by A1, A2;

      end;

    end;

    theorem :: ENTROPY1:12

    

     Th12: ( len p) = ( len q) & p has_onlyone_value_in k implies ( mlt (p,q)) has_onlyone_value_in k & (( mlt (p,q)) . k) = ((p . k) * (q . k))

    proof

      assume that

       A1: ( len p) = ( len q) and

       A2: p has_onlyone_value_in k;

      ( len ( mlt (p,q))) = ( len p) by A1, MATRPROB: 30;

      then

       A3: ( dom ( mlt (p,q))) = ( dom p) by FINSEQ_3: 29;

       A4:

      now

        let i such that

         A5: i in ( dom ( mlt (p,q))) and

         A6: i <> k;

        

        thus (( mlt (p,q)) . i) = ((p . i) * (q . i)) by RVSUM_1: 59

        .= ( 0 * (q . i)) by A2, A3, A5, A6

        .= 0 ;

      end;

      k in ( dom ( mlt (p,q))) by A2, A3;

      hence thesis by A4, RVSUM_1: 59;

    end;

    theorem :: ENTROPY1:13

    

     Th13: p has_onlyone_value_in k implies ( Sum p) = (p . k)

    proof

      assume that

       A1: k in ( dom p) and

       A2: for i st i in ( dom p) & i <> k holds (p . i) = 0 ;

      reconsider a = (p . k) as Element of REAL by XREAL_0:def 1;

      reconsider p1 = (p | ( Seg k)) as FinSequence of REAL by FINSEQ_1: 18;

      p1 c= p by TREES_1:def 1;

      then

      consider p2 be FinSequence such that

       A3: p = (p1 ^ p2) by TREES_1: 1;

      reconsider p2 as FinSequence of REAL by A3, FINSEQ_1: 36;

      

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

      1 <= k by A1, FINSEQ_3: 25;

      then k in ( Seg k) by FINSEQ_1: 3;

      then

       A5: k in (( dom p) /\ ( Seg k)) by A1, XBOOLE_0:def 4;

      then

       A6: k in ( dom p1) by RELAT_1: 61;

      

       A7: for i st i in ( Seg ( len p2)) holds (p2 . i) = 0

      proof

        let i;

        

         A8: ( len p1) <= (( len p1) + i) by NAT_1: 12;

        

         A9: k <= ( len p1) by A6, FINSEQ_3: 25;

        assume i in ( Seg ( len p2));

        then

         A10: i in ( dom p2) by FINSEQ_1:def 3;

        then 0 <> i by FINSEQ_3: 25;

        then ( len p1) <> (( len p1) + i);

        then

         A11: k <> (( len p1) + i) by A9, A8, XXREAL_0: 1;

        

        thus (p2 . i) = (p . (( len p1) + i)) by A3, A10, FINSEQ_1:def 7

        .= 0 by A2, A3, A10, A11, FINSEQ_1: 28;

      end;

       A12:

      now

        let j be Nat;

        assume

         A13: j in ( dom p2);

        

        hence (p2 . j) = 0 by A7, A4

        .= ((( len p2) |-> 0 ) . j) by A4, A13, FINSEQ_2: 57;

      end;

      p1 <> {} by A5, RELAT_1: 38, RELAT_1: 61;

      then ( len p1) <> 0 ;

      then

      consider p3 be FinSequence of REAL , x be Element of REAL such that

       A14: p1 = (p3 ^ <*x*>) by FINSEQ_2: 19;

      k <= ( len p) by A1, FINSEQ_3: 25;

      

      then

       A15: k = ( len p1) by FINSEQ_1: 17

      .= (( len p3) + ( len <*x*>)) by A14, FINSEQ_1: 22

      .= (( len p3) + 1) by FINSEQ_1: 39;

      

      then

       A16: x = (p1 . k) by A14, FINSEQ_1: 42

      .= a by A3, A6, FINSEQ_1:def 7;

      

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

      

       A18: for i st i in ( Seg ( len p3)) holds (p3 . i) = 0

      proof

        let i;

        assume

         A19: i in ( Seg ( len p3));

        then i <= ( len p3) by FINSEQ_1: 1;

        then

         A20: i <> k by A15, NAT_1: 13;

        

         A21: i in ( dom p3) by A19, FINSEQ_1:def 3;

        then

         A22: i in ( dom p1) by A14, FINSEQ_2: 15;

        

        thus (p3 . i) = (p1 . i) by A14, A21, FINSEQ_1:def 7

        .= (p . i) by A3, A22, FINSEQ_1:def 7

        .= 0 by A2, A3, A20, A22, FINSEQ_2: 15;

      end;

       A23:

      now

        let j be Nat;

        assume

         A24: j in ( dom p3);

        

        hence (p3 . j) = 0 by A18, A17

        .= ((( len p3) |-> 0 ) . j) by A17, A24, FINSEQ_2: 57;

      end;

      ( len (( len p3) |-> 0 )) = ( len p3) by CARD_1:def 7;

      then

       A25: p3 = (( len p3) |-> 0 ) by A23, FINSEQ_2: 9;

      ( len (( len p2) |-> 0 )) = ( len p2) by CARD_1:def 7;

      then p2 = (( len p2) |-> 0 ) by A12, FINSEQ_2: 9;

      

      then ( Sum p) = (( Sum (p3 ^ <*x*>)) + ( Sum (( len p2) |-> 0 ))) by A3, A14, RVSUM_1: 75

      .= (( Sum (p3 ^ <*x*>)) + 0 ) by RVSUM_1: 81

      .= (( Sum (( len p3) |-> 0 )) + x) by A25, RVSUM_1: 74

      .= ( 0 + a) by A16, RVSUM_1: 81

      .= (p . k);

      hence thesis;

    end;

    theorem :: ENTROPY1:14

    

     Th14: p is nonnegative implies for k st k in ( dom p) & (p . k) = ( Sum p) holds p has_onlyone_value_in k

    proof

      assume

       A1: p is nonnegative;

      let k1 be Nat such that

       A2: k1 in ( dom p) and

       A3: (p . k1) = ( Sum p);

      k1 <= ( len p) by A2, FINSEQ_3: 25;

      then

      consider j1 be Nat such that

       A4: (k1 + j1) = ( len p) by NAT_1: 10;

      reconsider j1 as Nat;

      

       A5: k1 >= 1 by A2, FINSEQ_3: 25;

       not ex i st i in ( dom p) & i <> k1 & (p . i) <> 0

      proof

        assume ex i st i in ( dom p) & i <> k1 & (p . i) <> 0 ;

        then

        consider k2 be Nat such that

         A6: k2 in ( dom p) and

         A7: k2 <> k1 and

         A8: (p . k2) <> 0 ;

        

         A9: (p . k2) > 0 by A1, A6, A8;

        k2 <= ( len p) by A6, FINSEQ_3: 25;

        then

        consider j2 be Nat such that

         A10: (k2 + j2) = ( len p) by NAT_1: 10;

        reconsider j2 as Nat;

        

         A11: k2 >= 1 by A6, FINSEQ_3: 25;

        per cases by A7, XXREAL_0: 1;

          suppose

           A12: k1 > k2;

          consider p1,p2 be FinSequence of REAL such that

           A13: ( len p1) = k2 and

           A14: ( len p2) = j2 and

           A15: p = (p1 ^ p2) by A10, FINSEQ_2: 23;

          

           A16: for k be Nat st k in ( dom p2) holds (p2 . k) >= 0

          proof

            let k be Nat such that

             A17: k in ( dom p2);

            k >= 1 by A17, FINSEQ_3: 25;

            then

             A18: (k2 + k) >= (1 + 0 ) by XREAL_1: 7;

            k <= j2 by A14, A17, FINSEQ_3: 25;

            then (k2 + k) <= ( len p) by A10, XREAL_1: 7;

            then

             A19: (k2 + k) in ( dom p) by A18, FINSEQ_3: 25;

            (p2 . k) = (p . (k2 + k)) by A13, A15, A17, FINSEQ_1:def 7;

            hence thesis by A1, A19;

          end;

          k2 in ( Seg k2) by A11, FINSEQ_1: 3;

          then

           A20: k2 in ( dom p1) by A13, FINSEQ_1:def 3;

          (p1 . k2) > 0 & for k be Nat st k in ( dom p1) holds (p1 . k) >= 0

          proof

            thus (p1 . k2) > 0 by A9, A15, A20, FINSEQ_1:def 7;

            

             A21: ( dom p1) c= ( dom p) by A15, FINSEQ_1: 26;

            let k be Nat such that

             A22: k in ( dom p1);

            (p1 . k) = (p . k) by A15, A22, FINSEQ_1:def 7;

            hence thesis by A1, A22, A21;

          end;

          then

           A23: ( Sum p1) > 0 by A20, RVSUM_1: 85;

           not k1 in ( Seg k2) by A12, FINSEQ_1: 1;

          then not k1 in ( dom p1) by A13, FINSEQ_1:def 3;

          then

          consider kk be Nat such that

           A24: kk in ( dom p2) and

           A25: k1 = (k2 + kk) by A2, A13, A15, FINSEQ_1: 25;

          (p2 . kk) = (p . k1) by A13, A15, A24, A25, FINSEQ_1:def 7;

          then

           A26: ( Sum p2) >= (p . k1) by A24, A16, MATRPROB: 5;

          ( Sum p) = (( Sum p1) + ( Sum p2)) by A15, RVSUM_1: 75;

          then ( Sum p) > ((p . k1) + 0 ) by A23, A26, XREAL_1: 8;

          hence thesis by A3;

        end;

          suppose

           A27: k1 < k2;

          consider p1,p2 be FinSequence of REAL such that

           A28: ( len p1) = k1 and

           A29: ( len p2) = j1 and

           A30: p = (p1 ^ p2) by A4, FINSEQ_2: 23;

          

           A31: for k be Nat st k in ( dom p2) holds (p2 . k) >= 0

          proof

            let k be Nat such that

             A32: k in ( dom p2);

            k >= 1 by A32, FINSEQ_3: 25;

            then

             A33: (k1 + k) >= (1 + 0 ) by XREAL_1: 7;

            k <= j1 by A29, A32, FINSEQ_3: 25;

            then (k1 + k) <= ( len p) by A4, XREAL_1: 7;

            then

             A34: (k1 + k) in ( dom p) by A33, FINSEQ_3: 25;

            (p2 . k) = (p . (k1 + k)) by A28, A30, A32, FINSEQ_1:def 7;

            hence thesis by A1, A34;

          end;

          k1 in ( Seg k1) by A5, FINSEQ_1: 3;

          then

           A35: k1 in ( dom p1) by A28, FINSEQ_1:def 3;

          (p1 . k1) = (p . k1) & for k be Nat st k in ( dom p1) holds (p1 . k) >= 0

          proof

            thus (p1 . k1) = (p . k1) by A30, A35, FINSEQ_1:def 7;

            

             A36: ( dom p1) c= ( dom p) by A30, FINSEQ_1: 26;

            let k be Nat such that

             A37: k in ( dom p1);

            (p1 . k) = (p . k) by A30, A37, FINSEQ_1:def 7;

            hence thesis by A1, A37, A36;

          end;

          then

           A38: ( Sum p1) >= (p . k1) by A35, MATRPROB: 5;

           not k2 in ( Seg k1) by A27, FINSEQ_1: 1;

          then not k2 in ( dom p1) by A28, FINSEQ_1:def 3;

          then

          consider kk be Nat such that

           A39: kk in ( dom p2) and

           A40: k2 = (k1 + kk) by A6, A28, A30, FINSEQ_1: 25;

          (p2 . kk) = (p . k2) by A28, A30, A39, A40, FINSEQ_1:def 7;

          then

           A41: ( Sum p2) > 0 by A9, A39, A31, RVSUM_1: 85;

          ( Sum p) = (( Sum p1) + ( Sum p2)) by A30, RVSUM_1: 75;

          then ( Sum p) > ((p . k1) + 0 ) by A38, A41, XREAL_1: 8;

          hence thesis by A3;

        end;

      end;

      hence thesis by A2;

    end;

    registration

      cluster ProbFinS -> non empty nonnegative for FinSequence of REAL ;

      coherence by MATRPROB:def 5, RVSUM_1: 72;

    end

    theorem :: ENTROPY1:15

    

     Th15: for p be ProbFinS FinSequence of REAL holds for k st k in ( dom p) & (p . k) = 1 holds p has_onlyone_value_in k

    proof

      let p be ProbFinS FinSequence of REAL ;

      let k such that

       A1: k in ( dom p) and

       A2: (p . k) = 1;

      (p . k) = ( Sum p) by A2, MATRPROB:def 5;

      hence thesis by A1, Th14;

    end;

    theorem :: ENTROPY1:16

    

     Th16: for i be non zero Nat holds (i |-> (1 / i)) is ProbFinS FinSequence of REAL

    proof

      let i be non zero Nat;

      reconsider i as non zero Element of NAT by ORDINAL1:def 12;

      

       A1: for k be Nat st k in ( dom (i |-> (1 / i))) holds ((i |-> (1 / i)) . k) >= 0

      proof

        let k be Nat;

        assume k in ( dom (i |-> (1 / i)));

        then k in ( Seg i) by FUNCOP_1: 13;

        hence thesis by FUNCOP_1: 7;

      end;

      reconsider 1i = (1 / i) as Element of REAL by XREAL_0:def 1;

      reconsider ii = (i |-> 1i) as FinSequence of REAL ;

      ( Sum (i |-> (1 / i))) = (i * (1 / i)) by RVSUM_1: 80

      .= 1 by XCMPLX_1: 106;

      then ii is ProbFinS by A1, MATRPROB:def 5;

      hence thesis;

    end;

    registration

      cluster with_sum=1 -> non empty-yielding for Matrix of REAL ;

      coherence

      proof

        let M be Matrix of REAL such that

         A1: M is with_sum=1;

        assume

         A2: M is empty-yielding;

        per cases by A2, MATRIX_0:def 10;

          suppose ( len M) = 0 ;

          then ( SumAll M) = 0 by MATRPROB: 23;

          hence thesis by A1, MATRPROB:def 7;

        end;

          suppose ( width M) = 0 & ( len M) > 0 ;

          then

          reconsider M1 = M as Matrix of ( len M), 0 , REAL by MATRIX_0: 20;

          ( SumAll M1) = 0 by MATRPROB: 24;

          hence thesis by A1, MATRPROB:def 7;

        end;

      end;

      cluster Joint_Probability -> non empty-yielding for Matrix of REAL ;

      coherence ;

    end

    theorem :: ENTROPY1:17

    for M be Matrix of REAL st M = {} holds ( SumAll M) = 0

    proof

      let M be Matrix of REAL ;

      assume M = {} ;

      then

      reconsider M1 = M as Matrix of 0 , ( width M), REAL by MATRIX_0: 13;

      ( len M1) = 0 by MATRIX_0: 22;

      hence thesis by MATRPROB: 23;

    end;

    theorem :: ENTROPY1:18

    

     Th18: for M be Matrix of D holds for i st i in ( dom M) holds ( dom (M . i)) = ( Seg ( width M))

    proof

      let M be Matrix of D;

      let i;

      assume i in ( dom M);

      

      hence ( dom (M . i)) = ( dom ( Line (M,i))) by MATRIX_0: 60

      .= ( Seg ( len ( Line (M,i)))) by FINSEQ_1:def 3

      .= ( Seg ( width M)) by MATRIX_0:def 7;

    end;

    theorem :: ENTROPY1:19

    

     Th19: MR is m-nonnegative iff for i st i in ( dom MR) holds ( Line (MR,i)) is nonnegative

    proof

      hereby

        assume

         A1: MR is m-nonnegative;

        let i such that

         A2: i in ( dom MR);

        now

          let k;

          assume k in ( dom ( Line (MR,i)));

          then

           A3: k in ( dom (MR . i)) by A2, MATRIX_0: 60;

          then k in ( Seg ( width MR)) by A2, Th18;

          then

           A4: (( Line (MR,i)) . k) = (MR * (i,k)) by MATRIX_0:def 7;

           [i, k] in ( Indices MR) by A2, A3, MATRPROB: 13;

          hence (( Line (MR,i)) . k) >= 0 by A1, A4, MATRPROB:def 6;

        end;

        hence ( Line (MR,i)) is nonnegative;

      end;

      assume

       A5: for i st i in ( dom MR) holds ( Line (MR,i)) is nonnegative;

      now

        let i, j such that

         A6: [i, j] in ( Indices MR);

        

         A7: j in ( Seg ( width MR)) by A6, MATRPROB: 12;

        then j in ( Seg ( len ( Line (MR,i)))) by MATRIX_0:def 7;

        then

         A8: j in ( dom ( Line (MR,i))) by FINSEQ_1:def 3;

        i in ( Seg ( len MR)) by A6, MATRPROB: 12;

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

        then

         A9: ( Line (MR,i)) is nonnegative by A5;

        (MR * (i,j)) = (( Line (MR,i)) . j) by A7, MATRIX_0:def 7;

        hence (MR * (i,j)) >= 0 by A8, A9;

      end;

      hence thesis by MATRPROB:def 6;

    end;

    begin

    theorem :: ENTROPY1:20

    

     Th20: for j st j in ( dom p) holds ( Col (( LineVec2Mx p),j)) = <*(p . j)*>

    proof

      set M = ( LineVec2Mx p);

      let j such that

       A1: j in ( dom p);

      

       A2: ( dom <*(p . j)*>) = ( Seg 1) by FINSEQ_1:def 8;

      

       A3: ( len ( Col (M,j))) = ( len M) by MATRIX_0:def 8;

      then ( len ( Col (M,j))) = 1 by MATRIXR1:def 10;

      then

       A4: ( dom ( Col (M,j))) = ( dom <*(p . j)*>) by A2, FINSEQ_1:def 3;

      now

        let k be Nat such that

         A5: k in ( dom ( Col (M,j)));

        

         A6: k <= 1 by A2, A4, A5, FINSEQ_1: 1;

        k >= 1 by A2, A4, A5, FINSEQ_1: 1;

        then

         A7: k = 1 by A6, XXREAL_0: 1;

        k in ( dom M) by A3, A5, FINSEQ_3: 29;

        

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

        .= (p . j) by A1, A7, MATRIXR1:def 10

        .= ( <*(p . j)*> . k) by A7, FINSEQ_1:def 8;

      end;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:21

    

     Th21: for p be non empty FinSequence of REAL holds for q be FinSequence of REAL holds for M be Matrix of REAL holds M = (( ColVec2Mx p) * ( LineVec2Mx q)) iff (( len M) = ( len p) & ( width M) = ( len q) & for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((p . i) * (q . j)))

    proof

      let p be non empty FinSequence of REAL ;

      let q be FinSequence of REAL ;

      let M be Matrix of REAL ;

      set M1 = ( ColVec2Mx p);

      set M2 = ( LineVec2Mx q);

      

       A1: ( len M1) = ( len p) by MATRIXR1:def 9;

      

       A2: ( len M2) = 1 by MATRIXR1:def 10;

      

       A3: ( len p) > 0 ;

      then

       A4: ( width M1) = 1 by MATRIXR1:def 9;

      

       A5: ( width M2) = ( len q) by MATRIXR1:def 10;

      hereby

        assume

         A6: M = (M1 * M2);

        then

         A7: ( len M) = ( len M1) by A4, A2, MATRPROB: 39;

        thus ( len M) = ( len p) & ( width M) = ( len q) by A1, A4, A2, A5, A6, MATRPROB: 39;

        

         A8: ( width M) = ( width M2) by A4, A2, A6, MATRPROB: 39;

        thus for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((p . i) * (q . j))

        proof

          let i, j such that

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

          

           A10: i in ( Seg ( len M)) by A9, MATRPROB: 12;

          then

           A11: i in ( dom p) by A1, A7, FINSEQ_1:def 3;

          j in ( Seg ( width M)) by A9, MATRPROB: 12;

          then

           A12: j in ( dom q) by A5, A8, FINSEQ_1:def 3;

          i in ( dom M1) by A7, A10, FINSEQ_1:def 3;

          

          then

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

          .= <*(p . i)*> by A3, A11, MATRIXR1:def 9;

          

          thus (M * (i,j)) = (( Line (M1,i)) "*" ( Col (M2,j))) by A4, A2, A6, A9, MATRPROB: 39

          .= ( <*(p . i)*> "*" <*(q . j)*>) by A12, A13, Th20

          .= ( Sum ( mlt ( <*(p . i)*>, <*(q . j)*>))) by RVSUM_1:def 16

          .= ( Sum <*((p . i) * (q . j))*>) by RVSUM_1: 62

          .= ((p . i) * (q . j)) by RVSUM_1: 73;

        end;

      end;

      assume that

       A14: ( len M) = ( len p) and

       A15: ( width M) = ( len q) and

       A16: for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((p . i) * (q . j));

      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

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

        j in ( Seg ( width M)) by A17, MATRPROB: 12;

        then

         A18: j in ( dom q) by A15, FINSEQ_1:def 3;

        

         A19: i in ( Seg ( len M)) by A17, MATRPROB: 12;

        then

         A20: i in ( dom M1) by A1, A14, FINSEQ_1:def 3;

        i in ( dom p) by A14, A19, FINSEQ_1:def 3;

        

        then

         A21: <*(p . i)*> = (M1 . i) by A3, MATRIXR1:def 9

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

        

        thus (M * (i,j)) = ((p . i) * (q . j)) by A16, A17

        .= ( Sum <*((p . i) * (q . j))*>) by RVSUM_1: 73

        .= ( Sum ( mlt ( <*(p . i)*>, <*(q . j)*>))) by RVSUM_1: 62

        .= ( <*(p . i)*> "*" <*(q . j)*>) by RVSUM_1:def 16

        .= (( Line (M1,i)) "*" ( Col (M2,j))) by A18, A21, Th20;

      end;

      hence thesis by A1, A4, A2, A5, A14, A15, MATRPROB: 39;

    end;

    theorem :: ENTROPY1:22

    

     Th22: for p be non empty FinSequence of REAL holds for q be FinSequence of REAL holds for M be Matrix of REAL holds M = (( ColVec2Mx p) * ( LineVec2Mx q)) iff (( len M) = ( len p) & ( width M) = ( len q) & for i st i in ( dom M) holds ( Line (M,i)) = ((p . i) * q))

    proof

      let p be non empty FinSequence of REAL , q be FinSequence of REAL , M be Matrix of REAL ;

      set M1 = ( ColVec2Mx p);

      set M2 = ( LineVec2Mx q);

      hereby

        assume

         A1: M = (M1 * M2);

        hence ( len M) = ( len p) & ( width M) = ( len q) by Th21;

        thus for i st i in ( dom M) holds ( Line (M,i)) = ((p . i) * q)

        proof

          let i;

          assume i in ( dom M);

          then

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

          

           A3: for j be Nat st j in ( dom ( Line (M,i))) holds (( Line (M,i)) . j) = (((p . i) * q) . j)

          proof

            let j be Nat;

            assume j in ( dom ( Line (M,i)));

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

            then

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

            then

             A5: [i, j] in ( Indices M) by A2, MATRPROB: 12;

            

            thus (( Line (M,i)) . j) = (M * (i,j)) by A4, MATRIX_0:def 7

            .= ((p . i) * (q . j)) by A1, A5, Th21

            .= (((p . i) * q) . j) by RVSUM_1: 44;

          end;

          ( dom ( Line (M,i))) = ( Seg ( len ( Line (M,i)))) by FINSEQ_1:def 3

          .= ( Seg ( width M)) by MATRIX_0:def 7

          .= ( Seg ( len q)) by A1, Th21

          .= ( dom q) by FINSEQ_1:def 3

          .= ( dom ((p . i) * q)) by VALUED_1:def 5;

          hence thesis by A3, FINSEQ_1: 13;

        end;

      end;

      assume that

       A6: ( len M) = ( len p) and

       A7: ( width M) = ( len q) and

       A8: for i st i in ( dom M) holds ( Line (M,i)) = ((p . i) * q);

      for i, j st [i, j] in ( Indices M) holds (M * (i,j)) = ((p . i) * (q . j))

      proof

        let i, j such that

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

        

         A10: i in ( dom M) by A9, MATRPROB: 13;

        j in ( Seg ( width M)) by A9, MATRPROB: 12;

        

        hence (M * (i,j)) = (( Line (M,i)) . j) by MATRIX_0:def 7

        .= (((p . i) * q) . j) by A8, A10

        .= ((p . i) * (q . j)) by RVSUM_1: 44;

      end;

      hence thesis by A6, A7, Th21;

    end;

    theorem :: ENTROPY1:23

    

     Th23: for p,q be ProbFinS FinSequence of REAL holds (( ColVec2Mx p) * ( LineVec2Mx q)) is Joint_Probability

    proof

      let p,q be ProbFinS FinSequence of REAL ;

      set M = (( ColVec2Mx p) * ( LineVec2Mx q));

      

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

      

       A2: ( LineSum M) = p

      proof

        set M1 = ( LineSum M);

        

         A3: ( len M1) = ( len M) by MATRPROB: 20;

        then

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

         A5:

        now

          let k be Nat such that

           A6: k in ( dom M1);

          k in ( Seg ( len M)) by A3, A6, FINSEQ_1:def 3;

          

          hence (M1 . k) = ( Sum ( Line (M,k))) by MATRPROB: 20

          .= ( Sum ((p . k) * q)) by A4, A6, Th22

          .= ((p . k) * ( Sum q)) by RVSUM_1: 87

          .= ((p . k) * 1) by MATRPROB:def 5

          .= (p . k);

        end;

        ( dom M1) = ( dom p) by A1, A3, FINSEQ_3: 29;

        hence thesis by A5, FINSEQ_1: 13;

      end;

      

       A7: ( width M) = ( len q) by Th22;

      now

        let i, j such that

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

        i in ( Seg ( len p)) by A1, A8, MATRPROB: 12;

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

        then

         A9: (p . i) >= 0 by MATRPROB:def 5;

        j in ( Seg ( len q)) by A7, A8, MATRPROB: 12;

        then j in ( dom q) by FINSEQ_1:def 3;

        then

         A10: (q . j) >= 0 by MATRPROB:def 5;

        (M * (i,j)) = ((p . i) * (q . j)) by A8, Th21;

        hence (M * (i,j)) >= 0 by A9, A10;

      end;

      then

       A11: M is m-nonnegative by MATRPROB:def 6;

      ( SumAll M) = ( Sum ( LineSum M)) by MATRPROB:def 3

      .= 1 by A2, MATRPROB:def 5;

      then M is with_sum=1 by MATRPROB:def 7;

      hence thesis by A11;

    end;

    definition

      let n;

      let MR be Matrix of n, REAL ;

      :: ENTROPY1:def3

      attr MR is diagonal means

      : Def3: for i, j st [i, j] in ( Indices MR) & (MR * (i,j)) <> 0 holds i = j;

    end

    registration

      let n;

      cluster diagonal for Matrix of n, REAL ;

      existence

      proof

        deffunc F( set, set) = ( In ( 0 , REAL ));

        reconsider n1 = n as Nat;

        consider M be Matrix of n1, REAL such that

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

        reconsider M1 = M as Matrix of n, REAL ;

        take M1;

        for i, j st [i, j] in ( Indices M) & (M * (i,j)) <> 0 holds i = j by A1;

        hence thesis;

      end;

    end

    theorem :: ENTROPY1:24

    

     Th24: for MR be Matrix of n, REAL holds MR is diagonal iff for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i

    proof

      let MR be Matrix of n, REAL ;

      

       A1: ( width MR) = n by MATRIX_0: 24;

      ( len MR) = n by MATRIX_0: 24;

      then

       A2: ( dom MR) = ( Seg ( width MR)) by A1, FINSEQ_1:def 3;

      hereby

        assume

         A3: MR is diagonal;

        now

          let i such that

           A4: i in ( dom MR);

          

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

           A6:

          now

            let j such that

             A7: j in ( dom ( Line (MR,i))) and

             A8: j <> i;

            j in ( dom (MR . i)) by A4, A7, MATRIX_0: 60;

            then

             A9: [i, j] in ( Indices MR) by A4, MATRPROB: 13;

            j in ( Seg ( width MR)) by A5, A7, FINSEQ_1:def 3;

            

            hence (( Line (MR,i)) . j) = (MR * (i,j)) by MATRIX_0:def 7

            .= 0 by A3, A8, A9;

          end;

          i in ( dom ( Line (MR,i))) by A2, A4, A5, FINSEQ_1:def 3;

          hence ( Line (MR,i)) has_onlyone_value_in i by A6;

        end;

        hence for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i;

      end;

      assume

       A10: for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i;

      for i, j st [i, j] in ( Indices MR) & (MR * (i,j)) <> 0 holds i = j

      proof

        let i, j such that

         A11: [i, j] in ( Indices MR) and

         A12: (MR * (i,j)) <> 0 ;

        

         A13: i in ( dom MR) by A11, MATRPROB: 13;

        then

         A14: ( Line (MR,i)) has_onlyone_value_in i by A10;

        j in ( dom (MR . i)) by A11, MATRPROB: 13;

        then

         A15: j in ( dom ( Line (MR,i))) by A13, MATRIX_0: 60;

        assume

         A16: i <> j;

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

        then ( dom ( Line (MR,i))) = ( Seg ( width MR)) by FINSEQ_1:def 3;

        

        then (MR * (i,j)) = (( Line (MR,i)) . j) by A15, MATRIX_0:def 7

        .= 0 by A16, A15, A14;

        hence thesis by A12;

      end;

      hence thesis;

    end;

    definition

      let p;

      :: ENTROPY1:def4

      func Vec2DiagMx p -> diagonal Matrix of ( len p), REAL means

      : Def4: for j st j in ( dom p) holds (it * (j,j)) = (p . j);

      existence

      proof

        defpred P[ Nat, Nat, Real] means ($1 = $2 implies $3 = (p . $1)) & ($1 <> $2 implies $3 = 0 );

        

         A1: for i,j be Nat st [i, j] in [:( Seg ( len p)), ( Seg ( len p)):] holds ex x be Element of REAL st P[i, j, x]

        proof

          let i,j be Nat;

          assume [i, j] in [:( Seg ( len p)), ( Seg ( len p)):];

          

           A2: (p . i) in REAL by XREAL_0:def 1;

          

           A3: 0 in REAL by XREAL_0:def 1;

          i = j implies P[i, j, (p . i)];

          hence thesis by A2, A3;

        end;

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

         A4: for i,j be Nat st [i, j] in ( Indices M) holds P[i, j, (M * (i,j))] from MATRIX_0:sch 2( A1);

        for i, j st [i, j] in ( Indices M) & (M * (i,j)) <> 0 holds i = j by A4;

        then

        reconsider M1 = M as diagonal Matrix of ( len p), REAL by Def3;

        take M1;

        ( len M) = ( len p) by MATRIX_0: 24;

        then

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

        ( width M) = ( len p) by MATRIX_0: 24;

        then

         A6: ( Seg ( width M1)) = ( dom p) by FINSEQ_1:def 3;

        for j st j in ( dom p) holds (M1 * (j,j)) = (p . j)

        proof

          let j;

          assume j in ( dom p);

          then [j, j] in ( Indices M1) by A6, A5, MATRPROB: 12;

          hence thesis by A4;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let M1,M2 be diagonal Matrix of ( len p), REAL such that

         A7: for j st j in ( dom p) holds (M1 * (j,j)) = (p . j) and

         A8: for j st j in ( dom p) holds (M2 * (j,j)) = (p . j);

        ( width M1) = ( len p) by MATRIX_0: 24;

        then

         A9: ( Seg ( width M1)) = ( dom p) by FINSEQ_1:def 3;

        

         A10: ( Indices M1) = ( Indices M2) by MATRIX_0: 26;

        now

          let i,j be Nat such that

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

          reconsider i1 = i, j1 = j as Nat;

          

           A12: [i1, j1] in ( Indices M1) by A11;

          then

           A13: j1 in ( Seg ( width M1)) by MATRPROB: 12;

          per cases ;

            suppose

             A14: i = j;

            

            hence (M1 * (i,j)) = (p . j) by A7, A9, A13

            .= (M2 * (i,j)) by A8, A9, A13, A14;

          end;

            suppose

             A15: i <> j;

            

            hence (M1 * (i,j)) = 0 by A12, Def3

            .= (M2 * (i,j)) by A10, A12, A15, Def3;

          end;

        end;

        hence thesis by MATRIX_0: 27;

      end;

    end

    theorem :: ENTROPY1:25

    

     Th25: MR = ( Vec2DiagMx p) iff ( len MR) = ( len p) & ( width MR) = ( len p) & for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i & (( Line (MR,i)) . i) = (p . i)

    proof

      hereby

        assume

         A1: MR = ( Vec2DiagMx p);

        then

        reconsider M1 = MR as diagonal Matrix of ( len p), REAL ;

        

         A2: ( len M1) = ( len p) by MATRIX_0: 24;

        then

         A3: ( dom MR) = ( dom p) by FINSEQ_3: 29;

        thus ( len MR) = ( len p) & ( width MR) = ( len p) by A2, MATRIX_0: 24;

        ( width M1) = ( len p) by MATRIX_0: 24;

        then

         A4: ( Seg ( width MR)) = ( dom p) by FINSEQ_1:def 3;

        thus for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i & (( Line (MR,i)) . i) = (p . i)

        proof

          let i such that

           A5: i in ( dom MR);

          

           A6: ( Line (M1,i)) has_onlyone_value_in i by A5, Th24;

          (( Line (MR,i)) . i) = (MR * (i,i)) by A3, A4, A5, MATRIX_0:def 7

          .= (p . i) by A1, A3, A5, Def4;

          hence thesis by A6;

        end;

      end;

      assume that

       A7: ( len MR) = ( len p) and

       A8: ( width MR) = ( len p) and

       A9: for i st i in ( dom MR) holds ( Line (MR,i)) has_onlyone_value_in i & (( Line (MR,i)) . i) = (p . i);

      reconsider MM = MR as Matrix of ( len p), REAL by A7, A8, MATRIX_0: 51;

      for i st i in ( dom MM) holds ( Line (MM,i)) has_onlyone_value_in i by A9;

      then

      reconsider MM as diagonal Matrix of ( len p), REAL by Th24;

      for j st j in ( dom p) holds (MM * (j,j)) = (p . j)

      proof

        

         A10: ( dom MM) = ( dom p) by A7, FINSEQ_3: 29;

        let j such that

         A11: j in ( dom p);

        ( Seg ( width MM)) = ( dom p) by A8, FINSEQ_1:def 3;

        

        hence (MM * (j,j)) = (( Line (MM,j)) . j) by A11, MATRIX_0:def 7

        .= (p . j) by A9, A11, A10;

      end;

      hence thesis by Def4;

    end;

    theorem :: ENTROPY1:26

    

     Th26: ( len p) = ( len MR) implies (MR1 = (( Vec2DiagMx p) * MR) iff ( len MR1) = ( len p) & ( width MR1) = ( width MR) & for i, j st [i, j] in ( Indices MR1) holds (MR1 * (i,j)) = ((p . i) * (MR * (i,j))))

    proof

      set MM = ( Vec2DiagMx p);

      

       A1: ( len MM) = ( len p) by Th25;

      

       A2: ( width MM) = ( len p) by Th25;

      assume

       A3: ( len p) = ( len MR);

      then

       A4: ( dom p) = ( dom MR) by FINSEQ_3: 29;

      hereby

        assume

         A5: MR1 = (MM * MR);

        hence ( len MR1) = ( len p) & ( width MR1) = ( width MR) by A3, A1, A2, MATRPROB: 39;

        

         A6: ( len MR1) = ( len MM) by A3, A2, A5, MATRPROB: 39;

        then

         A7: ( dom MR1) = ( dom MM) by FINSEQ_3: 29;

        

         A8: ( dom MR1) = ( dom p) by A1, A6, FINSEQ_3: 29;

        thus for i, j st [i, j] in ( Indices MR1) holds (MR1 * (i,j)) = ((p . i) * (MR * (i,j)))

        proof

          let i, j such that

           A9: [i, j] in ( Indices MR1);

          i in ( Seg ( len MR1)) by A9, MATRPROB: 12;

          then

           A10: i in ( dom MR1) by FINSEQ_1:def 3;

          then

           A11: (( Line (MM,i)) . i) = (p . i) by A7, Th25;

          set q = ( mlt (( Line (MM,i)),( Col (MR,j))));

          

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

          

           A13: ( len ( Col (MR,j))) = ( len MR) by MATRIX_0:def 8;

          

           A14: ( Line (MM,i)) has_onlyone_value_in i by A7, A10, Th25;

          then

           A15: (q . i) = ((( Line (MM,i)) . i) * (( Col (MR,j)) . i)) by A3, A2, A12, A13, Th12;

          

          thus (MR1 * (i,j)) = (( Line (MM,i)) "*" ( Col (MR,j))) by A3, A2, A5, A9, MATRPROB: 39

          .= ( Sum q) by RVSUM_1:def 16

          .= ((p . i) * (( Col (MR,j)) . i)) by A3, A2, A14, A11, A12, A13, A15, Th12, Th13

          .= ((p . i) * (MR * (i,j))) by A4, A8, A10, MATRIX_0:def 8;

        end;

      end;

      assume that

       A16: ( len MR1) = ( len p) and

       A17: ( width MR1) = ( width MR) and

       A18: for i, j st [i, j] in ( Indices MR1) holds (MR1 * (i,j)) = ((p . i) * (MR * (i,j)));

      

       A19: ( dom MR1) = ( dom MM) by A1, A16, FINSEQ_3: 29;

      

       A20: ( dom MR) = ( dom MR1) by A3, A16, FINSEQ_3: 29;

      for i, j st [i, j] in ( Indices MR1) holds (MR1 * (i,j)) = (( Line (MM,i)) "*" ( Col (MR,j)))

      proof

        let i, j such that

         A21: [i, j] in ( Indices MR1);

        i in ( Seg ( len MR1)) by A21, MATRPROB: 12;

        then

         A22: i in ( dom MR1) by FINSEQ_1:def 3;

        then

         A23: (( Line (MM,i)) . i) = (p . i) by A19, Th25;

        set q = ( mlt (( Line (MM,i)),( Col (MR,j))));

        

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

        

         A25: ( len ( Col (MR,j))) = ( len MR) by MATRIX_0:def 8;

        

         A26: ( Line (MM,i)) has_onlyone_value_in i by A19, A22, Th25;

        then

         A27: (q . i) = ((( Line (MM,i)) . i) * (( Col (MR,j)) . i)) by A3, A2, A24, A25, Th12;

        

        thus (MR1 * (i,j)) = ((p . i) * (MR * (i,j))) by A18, A21

        .= ((p . i) * (( Col (MR,j)) . i)) by A20, A22, MATRIX_0:def 8

        .= ( Sum q) by A3, A2, A26, A23, A24, A25, A27, Th12, Th13

        .= (( Line (MM,i)) "*" ( Col (MR,j))) by RVSUM_1:def 16;

      end;

      hence thesis by A3, A1, A2, A16, A17, MATRPROB: 39;

    end;

    theorem :: ENTROPY1:27

    

     Th27: ( len p) = ( len MR) implies (MR1 = (( Vec2DiagMx p) * MR) iff ( len MR1) = ( len p) & ( width MR1) = ( width MR) & for i st i in ( dom MR1) holds ( Line (MR1,i)) = ((p . i) * ( Line (MR,i))))

    proof

      set MM = ( Vec2DiagMx p);

      assume

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

      hereby

        assume

         A2: MR1 = (MM * MR);

        hence ( len MR1) = ( len p) & ( width MR1) = ( width MR) by A1, Th26;

        

         A3: ( width MR1) = ( width MR) by A1, A2, Th26;

        thus for i st i in ( dom MR1) holds ( Line (MR1,i)) = ((p . i) * ( Line (MR,i)))

        proof

          let i;

          assume i in ( dom MR1);

          then

           A4: i in ( Seg ( len MR1)) by FINSEQ_1:def 3;

          

           A5: for j be Nat st j in ( dom ( Line (MR1,i))) holds (( Line (MR1,i)) . j) = (((p . i) * ( Line (MR,i))) . j)

          proof

            let j be Nat;

            assume j in ( dom ( Line (MR1,i)));

            then j in ( Seg ( len ( Line (MR1,i)))) by FINSEQ_1:def 3;

            then

             A6: j in ( Seg ( width MR1)) by MATRIX_0:def 7;

            then

             A7: [i, j] in ( Indices MR1) by A4, MATRPROB: 12;

            

            thus (( Line (MR1,i)) . j) = (MR1 * (i,j)) by A6, MATRIX_0:def 7

            .= ((p . i) * (MR * (i,j))) by A1, A2, A7, Th26

            .= ((p . i) * (( Line (MR,i)) . j)) by A3, A6, MATRIX_0:def 7

            .= (((p . i) * ( Line (MR,i))) . j) by RVSUM_1: 44;

          end;

          ( dom ( Line (MR1,i))) = ( Seg ( len ( Line (MR1,i)))) by FINSEQ_1:def 3

          .= ( Seg ( width MR1)) by MATRIX_0:def 7

          .= ( Seg ( len ( Line (MR,i)))) by A3, MATRIX_0:def 7

          .= ( dom ( Line (MR,i))) by FINSEQ_1:def 3

          .= ( dom ((p . i) * ( Line (MR,i)))) by VALUED_1:def 5;

          hence thesis by A5, FINSEQ_1: 13;

        end;

      end;

      assume that

       A8: ( len MR1) = ( len p) and

       A9: ( width MR1) = ( width MR) and

       A10: for i st i in ( dom MR1) holds ( Line (MR1,i)) = ((p . i) * ( Line (MR,i)));

      for i, j st [i, j] in ( Indices MR1) holds (MR1 * (i,j)) = ((p . i) * (MR * (i,j)))

      proof

        let i, j such that

         A11: [i, j] in ( Indices MR1);

        

         A12: i in ( dom MR1) by A11, MATRPROB: 13;

        

         A13: j in ( Seg ( width MR1)) by A11, MATRPROB: 12;

        

        hence (MR1 * (i,j)) = (( Line (MR1,i)) . j) by MATRIX_0:def 7

        .= (((p . i) * ( Line (MR,i))) . j) by A10, A12

        .= ((p . i) * (( Line (MR,i)) . j)) by RVSUM_1: 44

        .= ((p . i) * (MR * (i,j))) by A9, A13, MATRIX_0:def 7;

      end;

      hence thesis by A1, A8, A9, Th26;

    end;

    theorem :: ENTROPY1:28

    

     Th28: for p be ProbFinS FinSequence of REAL holds for M be non empty-yielding Conditional_Probability Matrix of REAL st ( len p) = ( len M) holds (( Vec2DiagMx p) * M) is Joint_Probability

    proof

      let p be ProbFinS FinSequence of REAL ;

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      set M1 = (( Vec2DiagMx p) * M);

      assume

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

      then

       A2: ( len M1) = ( len p) by Th26;

      

       A3: ( LineSum M1) = p

      proof

        set M2 = ( LineSum M1);

        

         A4: ( len M2) = ( len M1) by MATRPROB: 20;

        then

         A5: ( dom M2) = ( dom M) by A1, A2, FINSEQ_3: 29;

        

         A6: ( dom M2) = ( dom M1) by A4, FINSEQ_3: 29;

         A7:

        now

          let k be Nat such that

           A8: k in ( dom M2);

          k in ( Seg ( len M1)) by A4, A8, FINSEQ_1:def 3;

          

          hence (M2 . k) = ( Sum ( Line (M1,k))) by MATRPROB: 20

          .= ( Sum ((p . k) * ( Line (M,k)))) by A1, A6, A8, Th27

          .= ((p . k) * ( Sum ( Line (M,k)))) by RVSUM_1: 87

          .= ((p . k) * ( Sum (M . k))) by A5, A8, MATRIX_0: 60

          .= ((p . k) * 1) by A5, A8, MATRPROB:def 9

          .= (p . k);

        end;

        ( dom M2) = ( dom p) by A2, A4, FINSEQ_3: 29;

        hence thesis by A7, FINSEQ_1: 13;

      end;

      

       A9: ( width M1) = ( width M) by A1, Th26;

      now

        let i, j such that

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

        

         A11: j in ( Seg ( width M)) by A9, A10, MATRPROB: 12;

        i in ( Seg ( len p)) by A2, A10, MATRPROB: 12;

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

        then

         A12: (p . i) >= 0 by MATRPROB:def 5;

        i in ( Seg ( len M)) by A1, A2, A10, MATRPROB: 12;

        then [i, j] in ( Indices M) by A11, MATRPROB: 12;

        then

         A13: (M * (i,j)) >= 0 by MATRPROB:def 6;

        (M1 * (i,j)) = ((p . i) * (M * (i,j))) by A1, A10, Th26;

        hence (M1 * (i,j)) >= 0 by A12, A13;

      end;

      then

       A14: M1 is m-nonnegative by MATRPROB:def 6;

      ( SumAll M1) = ( Sum ( LineSum M1)) by MATRPROB:def 3

      .= 1 by A3, MATRPROB:def 5;

      then M1 is with_sum=1 by MATRPROB:def 7;

      hence thesis by A14;

    end;

    theorem :: ENTROPY1:29

    

     Th29: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for k st k in ( dom p) holds ( len (p . k)) = (k * ( width M))

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      defpred P[ Nat] means $1 >= 1 & $1 <= ( len M) implies ( len (p . $1)) = ($1 * ( width M));

      

       A4: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume that

         A5: n >= 1 & n <= ( len M) implies ( len (p . n)) = (n * ( width M));

        assume that

         A6: (n + 1) >= 1 and

         A7: (n + 1) <= ( len M);

        now

          per cases ;

            suppose

             A8: n = 0 ;

            then 1 in ( dom M) by A7, FINSEQ_3: 25;

            hence thesis by A2, A8, MATRIX_0: 36;

          end;

            suppose

             A9: n <> 0 ;

            

             A10: (n + 1) in ( dom M) by A6, A7, FINSEQ_3: 25;

            n < ( len M) by A7, NAT_1: 13;

            then (p . (n + 1)) = ((p . n) ^ (M . (n + 1))) by A3, A9, NAT_1: 14;

            

            then ( len (p . (n + 1))) = (( len (p . n)) + ( len (M . (n + 1)))) by FINSEQ_1: 22

            .= ((n * ( width M)) + ( width M)) by A5, A7, A9, A10, MATRIX_0: 36, NAT_1: 13, NAT_1: 14

            .= ((n + 1) * ( width M));

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A11: P[ 0 ];

      

       A12: for n be Nat holds P[n] from NAT_1:sch 2( A11, A4);

      let k;

      assume k in ( dom p);

      then

       A13: k in ( Seg ( len p)) by FINSEQ_1:def 3;

      then

       A14: k <= ( len p) by FINSEQ_1: 1;

      k >= 1 by A13, FINSEQ_1: 1;

      hence thesis by A1, A12, A14;

    end;

    theorem :: ENTROPY1:30

    

     Th30: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for i, j st i in ( dom p) & j in ( dom p) & i <= j holds ( dom (p . i)) c= ( dom (p . j))

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let i, j such that

       A4: i in ( dom p) and

       A5: j in ( dom p) and

       A6: i <= j;

      

       A7: ( len (p . j)) = (j * ( width M)) by A1, A2, A3, A5, Th29;

      ( len (p . i)) = (i * ( width M)) by A1, A2, A3, A4, Th29;

      then ( len (p . i)) <= ( len (p . j)) by A6, A7, NAT_1: 4;

      then ( Seg ( len (p . i))) c= ( Seg ( len (p . j))) by FINSEQ_1: 5;

      then ( dom (p . i)) c= ( Seg ( len (p . j))) by FINSEQ_1:def 3;

      hence thesis by FINSEQ_1:def 3;

    end;

    theorem :: ENTROPY1:31

    

     Th31: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds ( len (p . 1)) = ( width M) & for j st [1, j] in ( Indices M) holds j in ( dom (p . 1)) & ((p . 1) . j) = (M * (1,j))

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      per cases ;

        suppose

         A4: ( len M) = 0 ;

        then p = {} by A1;

        then (p . 1) = {} by FUNCT_1:def 2, RELAT_1: 38;

        hence ( len (p . 1)) = ( width M) by A4, MATRIX_0:def 3;

        let j;

        

         A5: ( Seg ( len M)) = {} by A4;

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

        hence thesis by A5, MATRPROB: 12;

      end;

        suppose ( len M) > 0 ;

        then 1 <= ( len p) by A1, NAT_1: 14;

        then 1 in ( Seg ( len p)) by FINSEQ_1: 1;

        then 1 in ( dom p) by FINSEQ_1:def 3;

        

        hence

         A6: ( len (p . 1)) = (1 * ( width M)) by A1, A2, A3, Th29

        .= ( width M);

        let j such that

         A7: [1, j] in ( Indices M);

        j in ( Seg ( width M)) by A7, MATRPROB: 12;

        hence thesis by A2, A6, A7, FINSEQ_1:def 3, MATRPROB: 14;

      end;

    end;

    theorem :: ENTROPY1:32

    

     Th32: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for j st j >= 1 & j < ( len p) holds for l st l in ( dom (p . j)) holds ((p . j) . l) = ((p . (j + 1)) . l)

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let j such that

       A3: j >= 1 and

       A4: j < ( len p);

      

       A5: (p . (j + 1)) = ((p . j) ^ (M . (j + 1))) by A1, A2, A3, A4;

      let l;

      assume l in ( dom (p . j));

      hence thesis by A5, FINSEQ_1:def 7;

    end;

    theorem :: ENTROPY1:33

    

     Th33: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for i, j st i in ( dom p) & j in ( dom p) & i <= j holds for l st l in ( dom (p . i)) holds ((p . i) . l) = ((p . j) . l)

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      defpred P[ Nat] means $1 in ( dom p) implies for i st i in ( dom p) & i <= $1 holds (for l st l in ( dom (p . i)) holds ((p . i) . l) = ((p . $1) . l));

      

       A4: for j st P[j] holds P[(j + 1)]

      proof

        let j such that

         A5: j in ( dom p) implies for i st i in ( dom p) & i <= j holds for l st l in ( dom (p . i)) holds ((p . i) . l) = ((p . j) . l);

        assume

         A6: (j + 1) in ( dom p);

        then

         A7: (j + 1) <= ( len p) by FINSEQ_3: 25;

        (j + 1) >= 1 by A6, FINSEQ_3: 25;

        then

         A8: (j + 1) = 1 or (j + 1) > 1 by XXREAL_0: 1;

        let i such that

         A9: i in ( dom p) and

         A10: i <= (j + 1);

        i in ( Seg ( len p)) by A9, FINSEQ_1:def 3;

        then

         A11: i >= 1 by FINSEQ_1: 1;

        per cases by A8, NAT_1: 13;

          suppose (j + 1) = 1;

          hence thesis by A10, A11, XXREAL_0: 1;

        end;

          suppose

           A12: j >= 1;

          

           A13: j < ( len p) by A7, NAT_1: 13;

          then

           A14: j in ( Seg ( len p)) by A12, FINSEQ_1: 1;

          then

           A15: j in ( dom p) by FINSEQ_1:def 3;

          thus for l st l in ( dom (p . i)) holds ((p . i) . l) = ((p . (j + 1)) . l)

          proof

            let l such that

             A16: l in ( dom (p . i));

            per cases by A10, NAT_1: 8;

              suppose

               A17: i <= j;

              then

               A18: ( dom (p . i)) c= ( dom (p . j)) by A1, A2, A3, A9, A15, Th30;

              

              thus ((p . i) . l) = ((p . j) . l) by A5, A9, A14, A16, A17, FINSEQ_1:def 3

              .= ((p . (j + 1)) . l) by A1, A3, A12, A13, A16, A18, Th32;

            end;

              suppose i = (j + 1);

              hence thesis;

            end;

          end;

        end;

      end;

      

       A19: P[ 0 ];

      for j holds P[j] from NAT_1:sch 2( A19, A4);

      hence thesis;

    end;

    theorem :: ENTROPY1:34

    

     Th34: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for j st j >= 1 & j < ( len p) holds for l st l in ( Seg ( width M)) holds ((j * ( width M)) + l) in ( dom (p . (j + 1))) & ((p . (j + 1)) . ((j * ( width M)) + l)) = ((M . (j + 1)) . l)

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let j such that

       A4: j >= 1 and

       A5: j < ( len p);

      

       A6: (j + 1) >= 1 by A4, NAT_1: 13;

      j in ( Seg ( len p)) by A4, A5, FINSEQ_1: 1;

      then j in ( dom p) by FINSEQ_1:def 3;

      then

       A7: ( len (p . j)) = (j * ( width M)) by A1, A2, A3, Th29;

      let l such that

       A8: l in ( Seg ( width M));

      

       A9: l <= ( width M) by A8, FINSEQ_1: 1;

      (j + 1) <= ( len M) by A1, A5, NAT_1: 13;

      then (j + 1) in ( Seg ( len M)) by A6, FINSEQ_1: 1;

      then

       A10: (j + 1) in ( dom M) by FINSEQ_1:def 3;

      then

       A11: l in ( dom (M . (j + 1))) by A8, Th18;

      l >= 1 by A8, FINSEQ_1: 1;

      then

       A12: ((j * ( width M)) + l) >= ( 0 + 1) by XREAL_1: 7;

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

      

      then ( len (p . (j + 1))) = ((j + 1) * ( width M)) by A1, A2, A3, A10, Th29

      .= ((j * ( width M)) + ( width M));

      then ((j * ( width M)) + l) <= ( len (p . (j + 1))) by A9, XREAL_1: 7;

      then ((j * ( width M)) + l) in ( Seg ( len (p . (j + 1)))) by A12, FINSEQ_1: 1;

      hence ((j * ( width M)) + l) in ( dom (p . (j + 1))) by FINSEQ_1:def 3;

      (p . (j + 1)) = ((p . j) ^ (M . (j + 1))) by A1, A3, A4, A5;

      hence thesis by A11, A7, FINSEQ_1:def 7;

    end;

    theorem :: ENTROPY1:35

    

     Th35: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for i, j st [i, j] in ( Indices M) holds (((i - 1) * ( width M)) + j) in ( dom (p . i)) & (M * (i,j)) = ((p . i) . (((i - 1) * ( width M)) + j))

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let i, j such that

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

      

       A5: j in ( Seg ( width M)) by A4, MATRPROB: 12;

      i in ( Seg ( len M)) by A4, MATRPROB: 12;

      then

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

      then

       A7: i >= 1 by FINSEQ_3: 25;

      

       A8: i <= ( len M) by A6, FINSEQ_3: 25;

      per cases by A7, XXREAL_0: 1;

        suppose

         A9: i > 1;

        then

        reconsider ii = (i - 1) as Nat by NAT_1: 20;

        i < (( len M) + 1) by A8, NAT_1: 13;

        then

         A10: (i - 1) < ((( len M) + 1) - 1) by XREAL_1: 14;

        (ii + 1) > 1 by A9;

        then

         A11: ii >= 1 by NAT_1: 13;

        then ((p . (ii + 1)) . ((ii * ( width M)) + j)) = ((M . (ii + 1)) . j) by A1, A2, A3, A5, A10, Th34;

        hence thesis by A1, A2, A3, A4, A5, A11, A10, Th34, MATRPROB: 14;

      end;

        suppose i = 1;

        hence thesis by A1, A2, A3, A4, Th31;

      end;

    end;

    theorem :: ENTROPY1:36

    

     Th36: for M be Matrix of D holds for p be FinSequence of (D * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for i, j st [i, j] in ( Indices M) holds (((i - 1) * ( width M)) + j) in ( dom (p . ( len M))) & (M * (i,j)) = ((p . ( len M)) . (((i - 1) * ( width M)) + j))

    proof

      let M be Matrix of D;

      let p be FinSequence of (D * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let i, j such that

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

      

       A5: (((i - 1) * ( width M)) + j) in ( dom (p . i)) by A1, A2, A3, A4, Th35;

      

       A6: (M * (i,j)) = ((p . i) . (((i - 1) * ( width M)) + j)) by A1, A2, A3, A4, Th35;

      

       A7: i in ( Seg ( len M)) by A4, MATRPROB: 12;

      then

       A8: ( len M) <> 0 ;

      

       A9: i <= ( len M) by A7, FINSEQ_1: 1;

      ( len M) >= 1 by A8, NAT_1: 14;

      then ( len M) in ( Seg ( len p)) by A1, FINSEQ_1: 1;

      then

       A10: ( len M) in ( dom p) by FINSEQ_1:def 3;

      

       A11: i in ( dom p) by A1, A7, FINSEQ_1:def 3;

      then ( dom (p . i)) c= ( dom (p . ( len M))) by A1, A2, A3, A9, A10, Th30;

      hence thesis by A1, A2, A3, A9, A11, A10, A5, A6, Th33;

    end;

    theorem :: ENTROPY1:37

    

     Th37: for M be Matrix of REAL holds for p be FinSequence of ( REAL * ) st (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds for k st k >= 1 & k < ( len M) holds ( Sum (p . (k + 1))) = (( Sum (p . k)) + ( Sum (M . (k + 1))))

    proof

      let M be Matrix of REAL ;

      let p be FinSequence of ( REAL * ) such that

       A1: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      let k such that

       A2: k >= 1 and

       A3: k < ( len M);

      (p . (k + 1)) = ((p . k) ^ (M . (k + 1))) by A1, A2, A3;

      hence thesis by RVSUM_1: 75;

    end;

    theorem :: ENTROPY1:38

    

     Th38: for M be Matrix of REAL holds for p be FinSequence of ( REAL * ) st ( len p) = ( len M) & (p . 1) = (M . 1) & (for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))) holds ( SumAll M) = ( Sum (p . ( len M)))

    proof

      let M be Matrix of REAL ;

      let p be FinSequence of ( REAL * ) such that

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

       A2: (p . 1) = (M . 1) and

       A3: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      per cases ;

        suppose

         A4: ( len M) = 0 ;

        then p = {} by A1;

        

        hence ( Sum (p . ( len M))) = 0 by FUNCT_1:def 2, RELAT_1: 38, RVSUM_1: 72

        .= ( SumAll M) by A4, MATRPROB: 23;

      end;

        suppose

         A5: ( len M) > 0 ;

        then

         A6: ( len M) >= 1 by NAT_1: 14;

        set q = ( LineSum M);

        

         A7: ( len q) = ( len M) by MATRPROB:def 1;

        then

        consider qq be FinSequence of REAL such that

         A8: ( len qq) = ( len q) and

         A9: (qq . 1) = (q . 1) and

         A10: for k st 0 <> k & k < ( len q) holds (qq . (k + 1)) = ((qq . k) + (q . (k + 1))) and

         A11: ( Sum q) = (qq . ( len q)) by A5, Th9, NAT_1: 14;

        

         A12: ( len qq) = ( len M) by A8, MATRPROB:def 1

        .= ( len ( Sum p)) by A1, MATRPROB:def 1;

        

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

        

         A14: ( len ( Sum p)) = ( len p) by MATRPROB:def 1;

        then

         A15: ( dom ( Sum p)) = ( dom p) by FINSEQ_3: 29;

        for j be Nat st j in ( dom qq) holds (qq . j) = (( Sum p) . j)

        proof

          defpred P[ Nat] means $1 in ( dom qq) implies (qq . $1) = (( Sum p) . $1);

          

           A16: for k st P[k] holds P[(k + 1)]

          proof

            let k such that

             A17: P[k];

            assume

             A18: (k + 1) in ( dom qq);

            then

             A19: (k + 1) <= ( len qq) by A13, FINSEQ_1: 1;

            

             A20: (k + 1) in ( dom ( Sum p)) by A1, A7, A14, A8, A13, A18, FINSEQ_1:def 3;

            

             A21: (k + 1) in ( dom M) by A7, A8, A13, A18, FINSEQ_1:def 3;

            (k + 1) >= 1 by A13, A18, FINSEQ_1: 1;

            then

             A22: (k + 1) = 1 or (k + 1) > 1 by XXREAL_0: 1;

            per cases by A22, NAT_1: 13;

              suppose

               A23: (k + 1) = 1;

              

               A24: 1 in ( Seg ( len M)) by A6, FINSEQ_1: 1;

              then

               A25: 1 in ( dom M) by FINSEQ_1:def 3;

              

               A26: 1 in ( dom p) by A1, A24, FINSEQ_1:def 3;

              (qq . (k + 1)) = ( Sum ( Line (M,1))) by A9, A23, A24, MATRPROB: 20

              .= ( Sum (M . 1)) by A25, MATRIX_0: 60

              .= (( Sum p) . 1) by A2, A15, A26, MATRPROB:def 1;

              hence thesis by A23;

            end;

              suppose

               A27: k >= 1;

              

               A28: k < ( len qq) by A19, NAT_1: 13;

              then

               A29: k < ( len M) by A8, MATRPROB:def 1;

              k in ( Seg ( len qq)) by A27, A28, FINSEQ_1: 1;

              then

               A30: k in ( dom ( Sum p)) by A12, FINSEQ_1:def 3;

              (qq . (k + 1)) = ((qq . k) + (q . (k + 1))) by A8, A10, A27, A28

              .= (( Sum (p . k)) + (q . (k + 1))) by A13, A17, A27, A28, A30, FINSEQ_1: 1, MATRPROB:def 1

              .= (( Sum (p . k)) + ( Sum ( Line (M,(k + 1))))) by A7, A8, A13, A18, MATRPROB: 20

              .= (( Sum (p . k)) + ( Sum (M . (k + 1)))) by A21, MATRIX_0: 60

              .= ( Sum (p . (k + 1))) by A3, A27, A29, Th37

              .= (( Sum p) . (k + 1)) by A20, MATRPROB:def 1;

              hence thesis;

            end;

          end;

          

           A31: P[ 0 ] by A13, FINSEQ_1: 1;

          for j holds P[j] from NAT_1:sch 2( A31, A16);

          hence thesis;

        end;

        then

         A32: qq = ( Sum p) by A12, FINSEQ_2: 9;

        ( len M) in ( Seg ( len M)) by A5, FINSEQ_1: 3;

        then

         A33: ( len M) in ( dom ( Sum p)) by A1, A14, FINSEQ_1:def 3;

        

        thus ( SumAll M) = ( Sum q) by MATRPROB:def 3

        .= (( Sum p) . ( len M)) by A11, A32, MATRPROB:def 1

        .= ( Sum (p . ( len M))) by A33, MATRPROB:def 1;

      end;

    end;

    definition

      let D be non empty set;

      let M be Matrix of D;

      :: ENTROPY1:def5

      func Mx2FinS (M) -> FinSequence of D means

      : Def5: it = {} if ( len M) = 0

      otherwise ex p be FinSequence of (D * ) st it = (p . ( len M)) & ( len p) = ( len M) & (p . 1) = (M . 1) & for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)));

      existence

      proof

        thus ( len M) = 0 implies ex z be FinSequence of D st z = {}

        proof

          assume ( len M) = 0 ;

          ( <*> D) = {} ;

          hence thesis;

        end;

        thus ( len M) <> 0 implies ex z be FinSequence of D st ex p be FinSequence of (D * ) st z = (p . ( len M)) & ( len p) = ( len M) & (p . 1) = (M . 1) & for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1)))

        proof

          reconsider M1 = (M . 1) as Element of (D * ) by FINSEQ_1:def 11;

          defpred P[ Nat, set, set] means ex p1,q1 be Element of (D * ) st q1 = $2 & p1 = (M . ($1 + 1)) & $3 = (q1 ^ p1);

          assume

           A1: ( len M) <> 0 ;

          

           A2: for n be Nat st 1 <= n & n < ( len M) holds for x be Element of (D * ) holds ex y be Element of (D * ) st P[n, x, y]

          proof

            let n be Nat such that 1 <= n and

             A3: n < ( len M);

            

             A4: 1 <= (n + 1) by NAT_1: 11;

            (n + 1) <= ( len M) by A3, NAT_1: 13;

            then (n + 1) in ( dom M) by A4, FINSEQ_3: 25;

            then

            reconsider p1 = (M . (n + 1)) as Element of (D * ) by FINSEQ_2: 11;

            let x be Element of (D * );

            set y = (x ^ p1);

            reconsider y as Element of (D * ) by FINSEQ_1:def 11;

            take y, p1, x;

            thus thesis;

          end;

          ex p be FinSequence of (D * ) st ( len p) = ( len M) & ((p . 1) = M1 or ( len M) = 0 ) & for n be Nat st 1 <= n & n < ( len M) holds P[n, (p . n), (p . (n + 1))] from RECDEF_1:sch 4( A2);

          then

          consider p be FinSequence of (D * ) such that

           A5: ( len p) = ( len M) and

           A6: (p . 1) = M1 or ( len M) = 0 and

           A7: for n be Nat st 1 <= n & n < ( len M) holds P[n, (p . n), (p . (n + 1))];

          reconsider z = (p . ( len M)) as FinSequence of D;

          take z;

          for n be Nat st 1 <= n & n < ( len M) holds (p . (n + 1)) = ((p . n) ^ (M . (n + 1)))

          proof

            let n be Nat such that

             A8: 1 <= n and

             A9: n < ( len M);

            ex p1,q1 be Element of (D * ) st q1 = (p . n) & p1 = (M . (n + 1)) & (p . (n + 1)) = (q1 ^ p1) by A7, A8, A9;

            hence thesis;

          end;

          hence thesis by A1, A5, A6;

        end;

      end;

      uniqueness

      proof

        let z1,z2 be FinSequence of D;

        thus ( len M) = 0 & z1 = {} & z2 = {} implies z1 = z2;

        assume ( len M) <> 0 ;

        then

         A10: ( len M) >= 1 by NAT_1: 14;

        given p1 be FinSequence of (D * ) such that

         A11: z1 = (p1 . ( len M)) and ( len p1) = ( len M) and

         A12: (p1 . 1) = (M . 1) and

         A13: for k st k >= 1 & k < ( len M) holds (p1 . (k + 1)) = ((p1 . k) ^ (M . (k + 1)));

        given p2 be FinSequence of (D * ) such that

         A14: z2 = (p2 . ( len M)) and ( len p2) = ( len M) and

         A15: (p2 . 1) = (M . 1) and

         A16: for k st k >= 1 & k < ( len M) holds (p2 . (k + 1)) = ((p2 . k) ^ (M . (k + 1)));

        for k st k >= 1 & k <= ( len M) holds (p1 . k) = (p2 . k)

        proof

          defpred P[ Nat] means $1 >= 1 & $1 <= ( len M) implies (p1 . $1) = (p2 . $1);

          

           A17: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            assume that

             A18: n >= 1 & n <= ( len M) implies (p1 . n) = (p2 . n);

            assume that (n + 1) >= 1 and

             A19: (n + 1) <= ( len M);

            now

              per cases ;

                suppose n = 0 ;

                hence thesis by A12, A15;

              end;

                suppose

                 A20: n <> 0 ;

                

                 A21: n < ( len M) by A19, NAT_1: 13;

                

                hence (p1 . (n + 1)) = ((p2 . n) ^ (M . (n + 1))) by A13, A18, A20, NAT_1: 14

                .= (p2 . (n + 1)) by A16, A20, A21, NAT_1: 14;

              end;

            end;

            hence thesis;

          end;

          

           A22: P[ 0 ];

          thus for n be Nat holds P[n] from NAT_1:sch 2( A22, A17);

        end;

        hence thesis by A10, A11, A14;

      end;

      consistency ;

    end

    theorem :: ENTROPY1:39

    

     Th39: for M be Matrix of D holds ( len ( Mx2FinS M)) = (( len M) * ( width M))

    proof

      let M be Matrix of D;

      per cases ;

        suppose

         A1: ( len M) = 0 ;

        then ( Mx2FinS M) = {} by Def5;

        hence thesis by A1;

      end;

        suppose

         A2: ( len M) > 0 ;

        then

        consider p be FinSequence of (D * ) such that

         A3: ( Mx2FinS M) = (p . ( len M)) and

         A4: ( len p) = ( len M) and

         A5: (p . 1) = (M . 1) and

         A6: for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1))) by Def5;

        ( len M) in ( Seg ( len M)) by A2, FINSEQ_1: 3;

        then ( len M) in ( dom p) by A4, FINSEQ_1:def 3;

        hence thesis by A3, A4, A5, A6, Th29;

      end;

    end;

    theorem :: ENTROPY1:40

    

     Th40: for M be Matrix of D holds for i, j st [i, j] in ( Indices M) holds (((i - 1) * ( width M)) + j) in ( dom ( Mx2FinS M)) & (M * (i,j)) = (( Mx2FinS M) . (((i - 1) * ( width M)) + j))

    proof

      let M be Matrix of D;

      let i, j such that

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

      ( Seg ( len M)) <> {} by A1, MATRPROB: 12;

      then ( len M) <> 0 ;

      then ex p be FinSequence of (D * ) st ( Mx2FinS M) = (p . ( len M)) & ( len p) = ( len M) & (p . 1) = (M . 1) & for k st k >= 1 & k < ( len M) holds (p . (k + 1)) = ((p . k) ^ (M . (k + 1))) by Def5;

      hence thesis by A1, Th36;

    end;

    theorem :: ENTROPY1:41

    

     Th41: for M be Matrix of D holds for k, l st k in ( dom ( Mx2FinS M)) & l = (k - 1) holds [((l div ( width M)) + 1), ((l mod ( width M)) + 1)] in ( Indices M) & (( Mx2FinS M) . k) = (M * (((l div ( width M)) + 1),((l mod ( width M)) + 1)))

    proof

      let M be Matrix of D;

      let k, l such that

       A1: k in ( dom ( Mx2FinS M)) and

       A2: l = (k - 1);

      set jj = ((l mod ( width M)) + 1);

      set ii = ((l div ( width M)) + 1);

      

       A3: ( len ( Mx2FinS M)) = (( len M) * ( width M)) by Th39;

      k in ( Seg ( len ( Mx2FinS M))) by A1, FINSEQ_1:def 3;

      then k <= ( len ( Mx2FinS M)) by FINSEQ_1: 1;

      then k < ((( len M) * ( width M)) + 1) by A3, NAT_1: 13;

      then

       A4: (k - 1) < (((( len M) * ( width M)) + 1) - 1) by XREAL_1: 9;

      

       A5: ( Mx2FinS M) <> {} by A1;

      then

       A6: ( width M) <> 0 by A3;

      

       A7: ( width M) > 0 by A5, A3;

      then

       A8: l = (((l div ( width M)) * ( width M)) + (l mod ( width M))) by NAT_D: 2;

      ( width M) divides (( len M) * ( width M)) by NAT_D:def 3;

      then (l div ( width M)) < ((( len M) * ( width M)) div ( width M)) by A2, A6, A4, Th1;

      then (l div ( width M)) < ( len M) by A6, NAT_D: 18;

      then

       A9: ii <= ( len M) by NAT_1: 13;

      (l mod ( width M)) < ( width M) by A7, NAT_D: 1;

      then

       A10: jj <= ( width M) by NAT_1: 13;

      jj >= 1 by NAT_1: 11;

      then

       A11: jj in ( Seg ( width M)) by A10, FINSEQ_1: 1;

      ii >= 1 by NAT_1: 11;

      then ii in ( Seg ( len M)) by A9, FINSEQ_1: 1;

      hence [ii, jj] in ( Indices M) by A11, MATRPROB: 12;

      

      then (M * (ii,jj)) = (( Mx2FinS M) . (((ii - 1) * ( width M)) + jj)) by Th40

      .= (( Mx2FinS M) . k) by A2, A8;

      hence thesis;

    end;

    theorem :: ENTROPY1:42

    

     Th42: ( SumAll MR) = ( Sum ( Mx2FinS MR))

    proof

      per cases ;

        suppose

         A1: ( len MR) = 0 ;

        

        hence ( Sum ( Mx2FinS MR)) = 0 by Def5, RVSUM_1: 72

        .= ( SumAll MR) by A1, MATRPROB: 23;

      end;

        suppose ( len MR) > 0 ;

        then ex p be FinSequence of ( REAL * ) st ( Mx2FinS MR) = (p . ( len MR)) & ( len p) = ( len MR) & (p . 1) = (MR . 1) & for k st k >= 1 & k < ( len MR) holds (p . (k + 1)) = ((p . k) ^ (MR . (k + 1))) by Def5;

        hence thesis by Th38;

      end;

    end;

    theorem :: ENTROPY1:43

    

     Th43: MR is m-nonnegative iff ( Mx2FinS MR) is nonnegative

    proof

      hereby

        assume

         A1: MR is m-nonnegative;

        for k st k in ( dom ( Mx2FinS MR)) holds (( Mx2FinS MR) . k) >= 0

        proof

          let i such that

           A2: i in ( dom ( Mx2FinS MR));

          i in ( Seg ( len ( Mx2FinS MR))) by A2, FINSEQ_1:def 3;

          then i >= 1 by FINSEQ_1: 1;

          then

          reconsider l = (i - 1) as Nat by NAT_1: 21;

          

           A3: (( Mx2FinS MR) . i) = (MR * (((l div ( width MR)) + 1),((l mod ( width MR)) + 1))) by A2, Th41;

           [((l div ( width MR)) + 1), ((l mod ( width MR)) + 1)] in ( Indices MR) by A2, Th41;

          hence thesis by A1, A3, MATRPROB:def 6;

        end;

        hence ( Mx2FinS MR) is nonnegative;

      end;

      assume

       A4: ( Mx2FinS MR) is nonnegative;

      now

        let i, j such that

         A5: [i, j] in ( Indices MR);

        

         A6: (MR * (i,j)) = (( Mx2FinS MR) . (((i - 1) * ( width MR)) + j)) by A5, Th40;

        (((i - 1) * ( width MR)) + j) in ( dom ( Mx2FinS MR)) by A5, Th40;

        hence (MR * (i,j)) >= 0 by A4, A6;

      end;

      hence thesis by MATRPROB:def 6;

    end;

    theorem :: ENTROPY1:44

    

     Th44: MR is Joint_Probability iff ( Mx2FinS MR) is ProbFinS

    proof

      hereby

        assume MR is Joint_Probability;

        then

        reconsider MRR = MR as Joint_Probability Matrix of REAL ;

        

         A1: MRR is m-nonnegative with_sum=1 Matrix of REAL ;

        then ( Mx2FinS MR) is nonnegative by Th43;

        then

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

        ( Sum ( Mx2FinS MR)) = ( SumAll MR) by Th42

        .= 1 by A1, MATRPROB:def 7;

        hence ( Mx2FinS MR) is ProbFinS by A2, MATRPROB:def 5;

      end;

      assume ( Mx2FinS MR) is ProbFinS;

      then

      reconsider pp = ( Mx2FinS MR) as ProbFinS FinSequence of REAL ;

      reconsider p = pp as non empty ProbFinS FinSequence of REAL ;

      ( SumAll MR) = ( Sum p) by Th42

      .= 1 by MATRPROB:def 5;

      then

       A3: MR is with_sum=1 by MATRPROB:def 7;

      p is nonnegative;

      then MR is m-nonnegative by Th43;

      hence thesis by A3;

    end;

    theorem :: ENTROPY1:45

    

     Th45: for p,q be ProbFinS FinSequence of REAL holds ( Mx2FinS (( ColVec2Mx p) * ( LineVec2Mx q))) is ProbFinS by Th23, Th44;

    theorem :: ENTROPY1:46

    for p be ProbFinS FinSequence of REAL holds for M be non empty-yielding Conditional_Probability Matrix of REAL st ( len p) = ( len M) holds ( Mx2FinS (( Vec2DiagMx p) * M)) is ProbFinS by Th28, Th44;

    begin

    definition

      let a be Real;

      let p;

      assume that

       A1: p is nonnegative;

      :: ENTROPY1:def6

      func FinSeq_log (a,p) -> FinSequence of REAL means

      : Def6: ( len it ) = ( len p) & for k be Nat st k in ( dom it ) holds ((p . k) > 0 implies (it . k) = ( log (a,(p . k)))) & ((p . k) = 0 implies (it . k) = 0 );

      existence

      proof

        defpred P[ Nat, set] means ((p . $1) > 0 implies $2 = ( log (a,(p . $1)))) & ((p . $1) = 0 implies $2 = 0 );

        

         A2: for k be Nat st k in ( Seg ( len p)) holds ex x be Element of REAL st P[k, x]

        proof

          let k be Nat;

          assume k in ( Seg ( len p));

          then

           A3: k in ( dom p) by FINSEQ_1:def 3;

          per cases by A1, A3;

            suppose

             A4: (p . k) > 0 ;

            reconsider ll = ( log (a,(p . k))) as Element of REAL by XREAL_0:def 1;

            take ll;

            thus thesis by A4;

          end;

            suppose

             A5: (p . k) = 0 ;

            take ( In ( 0 , REAL ));

            thus thesis by A5;

          end;

        end;

        consider pp be FinSequence of REAL such that

         A6: ( dom pp) = ( Seg ( len p)) & for k be Nat st k in ( Seg ( len p)) holds P[k, (pp . k)] from FINSEQ_1:sch 5( A2);

        ( len pp) = ( len p) by A6, FINSEQ_1:def 3;

        hence thesis by A6;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL such that

         A7: ( len p1) = ( len p) and

         A8: for k be Nat st k in ( dom p1) holds ((p . k) > 0 implies (p1 . k) = ( log (a,(p . k)))) & ((p . k) = 0 implies (p1 . k) = 0 ) and

         A9: ( len p2) = ( len p) and

         A10: for k be Nat st k in ( dom p2) holds ((p . k) > 0 implies (p2 . k) = ( log (a,(p . k)))) & ((p . k) = 0 implies (p2 . k) = 0 );

        

         A11: for k be Nat st k in ( dom p1) holds (p1 . k) = (p2 . k)

        proof

          let k be Nat;

          assume

           A12: k in ( dom p1);

          then

           A13: k in ( dom p) by A7, FINSEQ_3: 29;

          

           A14: k in ( dom p2) by A7, A9, A12, FINSEQ_3: 29;

          per cases by A1, A13;

            suppose

             A15: (p . k) > 0 ;

            

            hence (p1 . k) = ( log (a,(p . k))) by A8, A12

            .= (p2 . k) by A10, A14, A15;

          end;

            suppose

             A16: (p . k) = 0 ;

            

            hence (p1 . k) = 0 by A8, A12

            .= (p2 . k) by A10, A14, A16;

          end;

        end;

        ( dom p1) = ( Seg ( len p2)) by A7, A9, FINSEQ_1:def 3

        .= ( dom p2) by FINSEQ_1:def 3;

        hence thesis by A11, FINSEQ_1: 13;

      end;

    end

    definition

      let p;

      :: ENTROPY1:def7

      func Infor_FinSeq_of p -> FinSequence of REAL equals ( mlt (p,( FinSeq_log (2,p))));

      correctness ;

    end

    theorem :: ENTROPY1:47

    

     Th47: for p be nonnegative FinSequence of REAL holds for q holds q = ( Infor_FinSeq_of p) iff ( len q) = ( len p) & for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(p . k))))

    proof

      let p be nonnegative FinSequence of REAL ;

      let q;

      set pp = ( mlt (p,( FinSeq_log (2,p))));

      

       A1: ( len p) = ( len ( FinSeq_log (2,p))) by Def6;

      then

       A2: ( len pp) = ( len p) by MATRPROB: 30;

      hereby

        assume

         A3: q = ( Infor_FinSeq_of p);

        thus ( len q) = ( len p) & for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(p . k))))

        proof

          

           A4: ( dom p) = ( dom q) by A2, A3, FINSEQ_3: 29;

          thus ( len q) = ( len p) by A1, A3, MATRPROB: 30;

          let k such that

           A5: k in ( dom q);

          

           A6: (q . k) = ((p . k) * (( FinSeq_log (2,p)) . k)) by A3, RVSUM_1: 59;

          

           A7: k in ( dom ( FinSeq_log (2,p))) by A1, A2, A3, A5, FINSEQ_3: 29;

          per cases by A5, A4, Def1;

            suppose (p . k) = 0 ;

            hence thesis by A6;

          end;

            suppose (p . k) > 0 ;

            hence thesis by A6, A7, Def6;

          end;

        end;

      end;

      assume that

       A8: ( len q) = ( len p) and

       A9: for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(p . k))));

      

       A10: ( dom q) = ( dom p) by A8, FINSEQ_3: 29;

      ( len q) = ( len pp) by A1, A8, MATRPROB: 30;

      then

       A11: ( dom q) = ( dom pp) by FINSEQ_3: 29;

      

       A12: ( dom p) = ( dom ( FinSeq_log (2,p))) by A1, FINSEQ_3: 29;

      now

        let k be Nat such that

         A13: k in ( dom q);

        

         A14: (pp . k) = ((p . k) * (( FinSeq_log (2,p)) . k)) by RVSUM_1: 59;

        per cases by A10, A13, Def1;

          suppose

           A15: (p . k) = 0 ;

          

          hence (q . k) = ( 0 * ( log (2,(p . k)))) by A9, A13

          .= (pp . k) by A14, A15;

        end;

          suppose (p . k) > 0 ;

          then (( FinSeq_log (2,p)) . k) = ( log (2,(p . k))) by A12, A10, A13, Def6;

          

          hence (pp . k) = ((p . k) * ( log (2,(p . k)))) by RVSUM_1: 59

          .= (q . k) by A9, A13;

        end;

      end;

      hence thesis by A11, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:48

    

     Th48: for p be nonnegative FinSequence of REAL holds for k st k in ( dom p) holds ((p . k) = 0 implies (( Infor_FinSeq_of p) . k) = 0 ) & ((p . k) > 0 implies (( Infor_FinSeq_of p) . k) = ((p . k) * ( log (2,(p . k)))))

    proof

      let p be nonnegative FinSequence of REAL ;

      

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

      .= ( Seg ( len ( Infor_FinSeq_of p))) by Th47

      .= ( dom ( Infor_FinSeq_of p)) by FINSEQ_1:def 3;

      let k such that

       A2: k in ( dom p);

      hereby

        assume (p . k) = 0 ;

        

        hence (( Infor_FinSeq_of p) . k) = ( 0 * ( log (2,(p . k)))) by A2, A1, Th47

        .= 0 ;

      end;

      thus thesis by A2, A1, Th47;

    end;

    theorem :: ENTROPY1:49

    for p be nonnegative FinSequence of REAL holds for q holds q = ( - ( Infor_FinSeq_of p)) iff (( len q) = ( len p) & for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(1 / (p . k))))))

    proof

      let p be nonnegative FinSequence of REAL , q;

      set p0 = ( Infor_FinSeq_of p);

      hereby

        assume

         A1: q = ( - p0);

        then

         A2: ( dom q) = ( dom p0) by VALUED_1: 8;

        

         A3: ( Seg ( len q)) = ( dom q) by FINSEQ_1:def 3

        .= ( Seg ( len p0)) by A2, FINSEQ_1:def 3

        .= ( Seg ( len p)) by Th47;

        for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(1 / (p . k)))))

        proof

          let k such that

           A4: k in ( dom q);

          k in ( Seg ( len q)) by A4, FINSEQ_1:def 3;

          then

           A5: k in ( dom p) by A3, FINSEQ_1:def 3;

          

           A6: (q . k) = ( - (p0 . k)) by A1, RVSUM_1: 17;

          

          then

           A7: (q . k) = ( - ((p . k) * ( log (2,(p . k))))) by A2, A4, Th47

          .= ((p . k) * ( - ( log (2,(p . k)))));

          per cases by A5, Def1;

            suppose

             A8: (p . k) = 0 ;

            then (p0 . k) = 0 by A5, Th48;

            hence thesis by A6, A8;

          end;

            suppose (p . k) > 0 ;

            hence thesis by A7, Th5;

          end;

        end;

        hence ( len q) = ( len p) & for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(1 / (p . k))))) by A3, FINSEQ_1: 6;

      end;

      assume that

       A9: ( len q) = ( len p) and

       A10: for k st k in ( dom q) holds (q . k) = ((p . k) * ( log (2,(1 / (p . k)))));

      

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

      .= ( Seg ( len p0)) by A9, Th47

      .= ( dom p0) by FINSEQ_1:def 3;

      

       A12: for k be Nat st k in ( dom q) holds (( - p0) . k) = (q . k)

      proof

        let k be Nat;

        assume

         A13: k in ( dom q);

        then k in ( Seg ( len p)) by A9, FINSEQ_1:def 3;

        then

         A14: k in ( dom p) by FINSEQ_1:def 3;

        per cases by A14, Def1;

          suppose

           A15: (p . k) = 0 ;

          

          thus (( - p0) . k) = ( - (p0 . k)) by RVSUM_1: 17

          .= ( - 0 ) by A14, A15, Th48

          .= ((p . k) * ( log (2,(1 / (p . k))))) by A15

          .= (q . k) by A10, A13;

        end;

          suppose

           A16: (p . k) > 0 ;

          

          thus (( - p0) . k) = ( - (p0 . k)) by RVSUM_1: 17

          .= ( - ((p . k) * ( log (2,(p . k))))) by A11, A13, Th47

          .= ((p . k) * ( - ( log (2,(p . k)))))

          .= ((p . k) * ( log (2,(1 / (p . k))))) by A16, Th5

          .= (q . k) by A10, A13;

        end;

      end;

      ( dom q) = ( dom ( - p0)) by A11, VALUED_1: 8;

      hence thesis by A12, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:50

    

     Th50: for p be nonnegative FinSequence of REAL st r1 >= 0 & r2 >= 0 holds for i st i in ( dom p) & (p . i) = (r1 * r2) holds (( Infor_FinSeq_of p) . i) = (((r1 * r2) * ( log (2,r1))) + ((r1 * r2) * ( log (2,r2))))

    proof

      let p be nonnegative FinSequence of REAL such that

       A1: r1 >= 0 and

       A2: r2 >= 0 ;

      let i such that

       A3: i in ( dom p) and

       A4: (p . i) = (r1 * r2);

      ( len p) = ( len ( Infor_FinSeq_of p)) by Th47;

      then i in ( dom ( Infor_FinSeq_of p)) by A3, FINSEQ_3: 29;

      

      hence (( Infor_FinSeq_of p) . i) = ((r1 * r2) * ( log (2,(r1 * r2)))) by A4, Th47

      .= (((r1 * r2) * ( log (2,r1))) + ((r1 * r2) * ( log (2,r2)))) by A1, A2, Th6;

    end;

    theorem :: ENTROPY1:51

    

     Th51: for p be nonnegative FinSequence of REAL st r >= 0 holds ( Infor_FinSeq_of (r * p)) = (((r * ( log (2,r))) * p) + (r * ( mlt (p,( FinSeq_log (2,p))))))

    proof

      let p be nonnegative FinSequence of REAL such that

       A1: r >= 0 ;

      reconsider q = (r * p) as nonnegative FinSequence of REAL by A1, Th10;

      set qq = ( Infor_FinSeq_of q);

      

       A2: ( dom q) = ( dom p) by VALUED_1:def 5;

      

       A3: ( dom ((r * ( log (2,r))) * p)) = ( dom p) by VALUED_1:def 5;

      

       A4: ( len ( FinSeq_log (2,p))) = ( len p) by Def6;

      then ( len ( mlt (p,( FinSeq_log (2,p))))) = ( len p) by MATRPROB: 30;

      then ( dom ( mlt (p,( FinSeq_log (2,p))))) = ( dom p) by FINSEQ_3: 29;

      then ( dom (r * ( mlt (p,( FinSeq_log (2,p)))))) = ( dom p) by VALUED_1:def 5;

      then ( len ((r * ( log (2,r))) * p)) = ( len (r * ( mlt (p,( FinSeq_log (2,p)))))) by A3, FINSEQ_3: 29;

      then ( len (((r * ( log (2,r))) * p) + (r * ( mlt (p,( FinSeq_log (2,p))))))) = ( len ((r * ( log (2,r))) * p)) by INTEGRA5: 2;

      then

       A5: ( dom (((r * ( log (2,r))) * p) + (r * ( mlt (p,( FinSeq_log (2,p))))))) = ( dom ((r * ( log (2,r))) * p)) by FINSEQ_3: 29;

      ( len q) = ( len qq) by Th47;

      then

       A6: ( dom q) = ( dom qq) by FINSEQ_3: 29;

      

       A7: ( dom ( FinSeq_log (2,p))) = ( dom p) by A4, FINSEQ_3: 29;

      now

        let k be Nat such that

         A8: k in ( dom qq);

        

         A9: (q . k) = (r * (p . k)) by RVSUM_1: 44;

        (p . k) >= 0 by A2, A6, A8, Def1;

        then

         A10: (qq . k) = (((r * (p . k)) * ( log (2,r))) + ((r * (p . k)) * ( log (2,(p . k))))) by A1, A6, A8, A9, Th50;

        

         A11: (((r * ( log (2,r))) * p) . k) = ((r * ( log (2,r))) * (p . k)) by RVSUM_1: 44;

        

         A12: ((r * ( mlt (p,( FinSeq_log (2,p))))) . k) = (r * (( mlt (p,( FinSeq_log (2,p)))) . k)) by RVSUM_1: 44

        .= (r * ((p . k) * (( FinSeq_log (2,p)) . k))) by RVSUM_1: 59

        .= ((r * (p . k)) * (( FinSeq_log (2,p)) . k));

        per cases by A2, A6, A8, Def1;

          suppose (p . k) > 0 ;

          then (qq . k) = ((((r * ( log (2,r))) * p) . k) + ((r * ( mlt (p,( FinSeq_log (2,p))))) . k)) by A2, A6, A7, A8, A10, A11, A12, Def6;

          hence (qq . k) = ((((r * ( log (2,r))) * p) + (r * ( mlt (p,( FinSeq_log (2,p)))))) . k) by A2, A6, A3, A5, A8, VALUED_1:def 1;

        end;

          suppose (p . k) = 0 ;

          hence (qq . k) = ((((r * ( log (2,r))) * p) + (r * ( mlt (p,( FinSeq_log (2,p)))))) . k) by A2, A6, A3, A5, A8, A10, A11, A12, VALUED_1:def 1;

        end;

      end;

      hence thesis by A2, A6, A3, A5, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:52

    

     Th52: for p be non empty ProbFinS FinSequence of REAL holds for k st k in ( dom p) holds (( Infor_FinSeq_of p) . k) <= 0

    proof

      let p be non empty ProbFinS FinSequence of REAL , k such that

       A1: k in ( dom p);

      per cases by A1, MATRPROB: 53, MATRPROB:def 5;

        suppose (p . k) = 0 ;

        hence thesis by A1, Th48;

      end;

        suppose

         A2: (p . k) > 0 & (p . k) <= 1;

        then

         A3: (( Infor_FinSeq_of p) . k) = ((p . k) * ( log (2,(p . k)))) by A1, Th48;

        thus (( Infor_FinSeq_of p) . k) <= 0

        proof

          

           A4: ( log (2,1)) = 0 by POWER: 51;

          per cases by A2, XXREAL_0: 1;

            suppose (p . k) < 1;

            then ( log (2,(p . k))) < 0 by A2, A4, POWER: 57;

            hence thesis by A2, A3;

          end;

            suppose (p . k) = 1;

            hence thesis by A3, POWER: 51;

          end;

        end;

      end;

    end;

    definition

      let MR;

      assume

       A1: MR is m-nonnegative;

      :: ENTROPY1:def8

      func Infor_FinSeq_of MR -> Matrix of REAL means

      : Def8: ( len it ) = ( len MR) & ( width it ) = ( width MR) & for k st k in ( dom it ) holds (it . k) = ( mlt (( Line (MR,k)),( FinSeq_log (2,( Line (MR,k))))));

      existence

      proof

        deffunc F( Nat) = ( mlt (( Line (MR,$1)),( FinSeq_log (2,( Line (MR,$1))))));

        consider p be FinSequence such that

         A2: ( len p) = ( len MR) and

         A3: for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_1:sch 2;

        

         A4: ( rng p) c= ( REAL * )

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider j be Nat such that

           A5: j in ( dom p) and

           A6: x = (p . j) by FINSEQ_2: 10;

          (p . j) = ( mlt (( Line (MR,j)),( FinSeq_log (2,( Line (MR,j)))))) by A3, A5;

          hence thesis by A6, FINSEQ_1:def 11;

        end;

        

         A7: for x be object st x in ( rng p) holds ex q be FinSequence st q = x & ( len q) = ( width MR)

        proof

          let x be object;

          assume x in ( rng p);

          then

          consider j be Nat such that

           A8: j in ( dom p) and

           A9: x = (p . j) by FINSEQ_2: 10;

          j in ( dom MR) by A2, A8, FINSEQ_3: 29;

          then ( Line (MR,j)) is nonnegative by A1, Th19;

          then

           A10: ( len ( FinSeq_log (2,( Line (MR,j))))) = ( len ( Line (MR,j))) by Def6;

          ( len ( Line (MR,j))) = ( width MR) by MATRIX_0:def 7;

          then

           A11: ( len ( mlt (( Line (MR,j)),( FinSeq_log (2,( Line (MR,j))))))) = ( width MR) by A10, MATRPROB: 30;

          x = ( mlt (( Line (MR,j)),( FinSeq_log (2,( Line (MR,j)))))) by A3, A8, A9;

          hence thesis by A11;

        end;

        then

        reconsider p as Matrix of REAL by A4, FINSEQ_1:def 4, MATRIX_0:def 1;

        take p;

        ( width p) = ( width MR)

        proof

          per cases ;

            suppose

             A12: ( len MR) = 0 ;

            then ( width p) = 0 by A2, MATRIX_0:def 3;

            hence thesis by A12, MATRIX_0:def 3;

          end;

            suppose

             A13: ( len MR) > 0 ;

            then ( len p) >= 1 by A2, NAT_1: 14;

            then 1 in ( Seg ( len p)) by FINSEQ_1: 1;

            then

             A14: 1 in ( dom p) by FINSEQ_1:def 3;

            then

             A15: (p . 1) in ( rng p) by FUNCT_1: 3;

            ex q be FinSequence st q = (p . 1) & ( len q) = ( width MR) by A7, A14, FUNCT_1: 3;

            hence thesis by A2, A13, A15, MATRIX_0:def 3;

          end;

        end;

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let M1,M2 be Matrix of REAL such that

         A16: ( len M1) = ( len MR) and ( width M1) = ( width MR) and

         A17: for k st k in ( dom M1) holds (M1 . k) = ( mlt (( Line (MR,k)),( FinSeq_log (2,( Line (MR,k)))))) and

         A18: ( len M2) = ( len MR) and ( width M2) = ( width MR) and

         A19: for k st k in ( dom M2) holds (M2 . k) = ( mlt (( Line (MR,k)),( FinSeq_log (2,( Line (MR,k))))));

        

         A20: ( dom M1) = ( dom M2) by A16, A18, FINSEQ_3: 29;

        now

          let k be Nat such that

           A21: k in ( dom M1);

          

          thus (M1 . k) = ( mlt (( Line (MR,k)),( FinSeq_log (2,( Line (MR,k)))))) by A17, A21

          .= (M2 . k) by A19, A20, A21;

        end;

        hence thesis by A20, FINSEQ_1: 13;

      end;

    end

    theorem :: ENTROPY1:53

    

     Th53: for M be m-nonnegative Matrix of REAL holds for k st k in ( dom M) holds ( Line (( Infor_FinSeq_of M),k)) = ( Infor_FinSeq_of ( Line (M,k)))

    proof

      let M be m-nonnegative Matrix of REAL ;

      set M1 = ( Infor_FinSeq_of M);

      ( len M1) = ( len M) by Def8;

      then

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

      let k such that

       A2: k in ( dom M);

      

      thus ( Line (M1,k)) = (M1 . k) by A2, A1, MATRIX_0: 60

      .= ( Infor_FinSeq_of ( Line (M,k))) by A2, A1, Def8;

    end;

    theorem :: ENTROPY1:54

    

     Th54: for M be m-nonnegative Matrix of REAL holds for M1 be Matrix of REAL holds M1 = ( Infor_FinSeq_of M) iff ( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = ((M * (i,j)) * ( log (2,(M * (i,j)))))

    proof

      let M be m-nonnegative Matrix of REAL ;

      let M1 be Matrix of REAL ;

      hereby

        assume

         A1: M1 = ( Infor_FinSeq_of M);

        then

         A2: ( width M1) = ( width M) by Def8;

        

         A3: ( len M1) = ( len M) by A1, Def8;

        now

          let i, j such that

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

          

           A5: j in ( Seg ( width M1)) by A4, MATRPROB: 12;

          i in ( Seg ( len M1)) by A4, MATRPROB: 12;

          then

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

          then

          reconsider p = ( Line (M,i)) as nonnegative FinSequence of REAL by Th19;

          

           A7: ( len p) = ( width M) by MATRIX_0:def 7;

          ( len p) = ( len ( Infor_FinSeq_of p)) by Th47;

          then

           A8: j in ( dom ( Infor_FinSeq_of p)) by A2, A5, A7, FINSEQ_1:def 3;

          

           A9: (p . j) = (M * (i,j)) by A2, A5, MATRIX_0:def 7;

          

          thus (M1 * (i,j)) = (( Line (M1,i)) . j) by A5, MATRIX_0:def 7

          .= (( Infor_FinSeq_of p) . j) by A1, A6, Th53

          .= ((M * (i,j)) * ( log (2,(M * (i,j))))) by A9, A8, Th47;

        end;

        hence ( len M1) = ( len M) & ( width M1) = ( width M) & for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = ((M * (i,j)) * ( log (2,(M * (i,j))))) by A1, Def8;

      end;

      assume that

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

       A11: ( width M1) = ( width M) and

       A12: for i, j st [i, j] in ( Indices M1) holds (M1 * (i,j)) = ((M * (i,j)) * ( log (2,(M * (i,j)))));

      

       A13: ( dom M1) = ( dom M) by A10, FINSEQ_3: 29;

      for k st k in ( dom M1) holds (M1 . k) = ( mlt (( Line (M,k)),( FinSeq_log (2,( Line (M,k))))))

      proof

        let k such that

         A14: k in ( dom M1);

        

         A15: ( len (M1 . k)) = ( width M1) by A14, MATRIX_0: 36;

        reconsider p = ( Line (M,k)) as nonnegative FinSequence of REAL by A13, A14, Th19;

        

         A16: ( len p) = ( width M) by MATRIX_0:def 7;

        

         A17: ( len ( FinSeq_log (2,p))) = ( len p) by Def6;

        then ( len ( mlt (p,( FinSeq_log (2,p))))) = ( len p) by MATRPROB: 30;

        then

         A18: ( dom (M1 . k)) = ( dom ( mlt (p,( FinSeq_log (2,p))))) by A11, A16, A15, FINSEQ_3: 29;

        

         A19: k in ( Seg ( len M)) by A10, A14, FINSEQ_1:def 3;

        now

          let j be Nat such that

           A20: j in ( dom (M1 . k));

          

           A21: j in ( Seg ( width M)) by A11, A15, A20, FINSEQ_1:def 3;

          then

           A22: (p . j) = (M * (k,j)) by MATRIX_0:def 7;

          

           A23: [k, j] in ( Indices M) by A19, A21, MATRPROB: 12;

          

           A24: (( mlt (p,( FinSeq_log (2,p)))) . j) = ((p . j) * (( FinSeq_log (2,p)) . j)) by RVSUM_1: 59

          .= ((M * (k,j)) * (( FinSeq_log (2,p)) . j)) by A21, MATRIX_0:def 7;

          

           A25: j in ( dom ( FinSeq_log (2,p))) by A16, A17, A21, FINSEQ_1:def 3;

          

           A26: [k, j] in ( Indices M1) by A14, A20, MATRPROB: 13;

          

          then

           A27: ((M1 . k) . j) = (M1 * (k,j)) by MATRPROB: 14

          .= ((M * (k,j)) * ( log (2,(M * (k,j))))) by A12, A26;

          per cases by A23, MATRPROB:def 6;

            suppose (M * (k,j)) = 0 ;

            hence ((M1 . k) . j) = (( mlt (p,( FinSeq_log (2,p)))) . j) by A27, A24;

          end;

            suppose (M * (k,j)) > 0 ;

            hence (( mlt (p,( FinSeq_log (2,p)))) . j) = ((M1 . k) . j) by A25, A27, A22, A24, Def6;

          end;

        end;

        hence thesis by A18, FINSEQ_1: 13;

      end;

      hence thesis by A10, A11, Def8;

    end;

    definition

      let p be FinSequence of REAL ;

      :: ENTROPY1:def9

      func Entropy p -> Real equals ( - ( Sum ( Infor_FinSeq_of p)));

      correctness ;

    end

    theorem :: ENTROPY1:55

    for p be non empty ProbFinS FinSequence of REAL holds ( Entropy p) >= 0

    proof

      let p be non empty ProbFinS FinSequence of REAL ;

      set p1 = ( - ( Infor_FinSeq_of p));

      

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

      .= ( Seg ( len ( Infor_FinSeq_of p))) by Th47

      .= ( dom ( Infor_FinSeq_of p)) by FINSEQ_1:def 3;

      

       A2: for k be Nat st k in ( dom p1) holds (p1 . k) >= 0

      proof

        let k be Nat;

        assume k in ( dom p1);

        then k in ( dom p) by A1, VALUED_1: 8;

        then (( Infor_FinSeq_of p) . k) <= 0 by Th52;

        then ( - (( Infor_FinSeq_of p) . k)) >= ( - 0 );

        hence thesis by RVSUM_1: 17;

      end;

      ( Entropy p) = ( Sum p1) by RVSUM_1: 88;

      hence thesis by A2, RVSUM_1: 84;

    end;

    theorem :: ENTROPY1:56

    for p be non empty ProbFinS FinSequence of REAL st ex k st k in ( dom p) & (p . k) = 1 holds ( Entropy p) = 0

    proof

      let p be non empty ProbFinS FinSequence of REAL ;

      assume ex k st k in ( dom p) & (p . k) = 1;

      then

      consider k1 be Nat such that

       A1: k1 in ( dom p) and

       A2: (p . k1) = 1;

      set q = ( Infor_FinSeq_of p);

      ( len q) = ( len p) by Th47;

      then

       A3: ( dom q) = ( dom p) by FINSEQ_3: 29;

      

       A4: p has_onlyone_value_in k1 by A1, A2, Th15;

      for k st k in ( dom q) holds (q . k) = 0

      proof

        let k such that

         A5: k in ( dom q);

        per cases ;

          suppose k = k1;

          

          hence (q . k) = (1 * ( log (2,1))) by A2, A5, Th47

          .= 0 by POWER: 51;

        end;

          suppose k <> k1;

          then

           A6: (p . k) = 0 by A4, A3, A5;

          

          thus (q . k) = ((p . k) * ( log (2,(p . k)))) by A5, Th47

          .= 0 by A6;

        end;

      end;

      then for x be object st x in ( dom q) holds (q . x) = 0 ;

      then q = (( dom q) --> 0 ) by FUNCOP_1: 11;

      then q = (( len q) |-> 0 ) by FINSEQ_1:def 3;

      then ( Sum q) = 0 by RVSUM_1: 81;

      hence thesis;

    end;

    theorem :: ENTROPY1:57

    

     Th57: for p,q be non empty ProbFinS FinSequence of REAL , pp,qq be FinSequence of REAL st ( len p) = ( len q) & ( len pp) = ( len p) & ( len qq) = ( len q) & (for k st k in ( dom p) holds (p . k) > 0 & (q . k) > 0 & (pp . k) = ( - ((p . k) * ( log (2,(p . k))))) & (qq . k) = ( - ((p . k) * ( log (2,(q . k)))))) holds ( Sum pp) <= ( Sum qq) & ((for k st k in ( dom p) holds (p . k) = (q . k)) iff ( Sum pp) = ( Sum qq)) & ((ex k st k in ( dom p) & (p . k) <> (q . k)) iff ( Sum pp) < ( Sum qq))

    proof

      let p,q be non empty ProbFinS FinSequence of REAL , pp,qq be FinSequence of REAL such that

       A1: ( len p) = ( len q) and

       A2: ( len pp) = ( len p) and

       A3: ( len qq) = ( len q) and

       A4: for k st k in ( dom p) holds (p . k) > 0 & (q . k) > 0 & (pp . k) = ( - ((p . k) * ( log (2,(p . k))))) & (qq . k) = ( - ((p . k) * ( log (2,(q . k)))));

      set p1 = (pp - qq);

      

       A5: number_e <> 1 by TAYLOR_1: 11;

      

       A6: ( len (pp - qq)) = ( len p) by A1, A2, A3, RVSUM_1: 116;

      then

       A7: ( dom (pp - qq)) = ( dom pp) by A2, FINSEQ_3: 29;

      then for k st k in ( dom pp) holds ((pp - qq) . k) = ((pp . k) - (qq . k)) by VALUED_1: 13;

      then

       A8: (( Sum pp) - ( Sum qq)) = ( Sum (pp - qq)) by A1, A2, A3, A6, Th8;

      

       A9: ( dom pp) = ( Seg ( len pp)) by FINSEQ_1:def 3

      .= ( dom p) by A2, FINSEQ_1:def 3;

      

       A10: for k st k in ( dom p) holds (p1 . k) = (((p . k) * ( log (2, number_e ))) * ( log ( number_e ,((q . k) / (p . k)))))

      proof

        let k such that

         A11: k in ( dom p);

        

         A12: (pp . k) = ( - ((p . k) * ( log (2,(p . k))))) by A4, A11;

        

         A13: (qq . k) = ( - ((p . k) * ( log (2,(q . k))))) by A4, A11;

        

         A14: (p . k) > 0 by A4, A11;

        then

         A15: ( - ( log (2,(p . k)))) = ( log (2,(1 / (p . k)))) by Th5;

        

         A16: (q . k) > 0 by A4, A11;

        then ((q . k) / (p . k)) > 0 by A14, XREAL_1: 139;

        then

         A17: ( log (2,((q . k) / (p . k)))) = (( log (2, number_e )) * ( log ( number_e ,((q . k) / (p . k))))) by A5, POWER: 56, TAYLOR_1: 11;

        

        thus (p1 . k) = ((pp . k) - (qq . k)) by A7, A9, A11, VALUED_1: 13

        .= ((p . k) * (( log (2,(1 / (p . k)))) + ( log (2,(q . k))))) by A12, A13, A15

        .= ((p . k) * ( log (2,((1 / (p . k)) * (q . k))))) by A14, A16, POWER: 53

        .= (((p . k) * ( log (2, number_e ))) * ( log ( number_e ,((q . k) / (p . k))))) by A17;

      end;

      set n = ( len p);

      deffunc F( Nat) = ( In ((((p . $1) * ( log (2, number_e ))) * (((q . $1) / (p . $1)) - 1)), REAL ));

      consider p2 be FinSequence of REAL such that

       A18: ( len p2) = n and

       A19: for k be Nat st k in ( dom p2) holds (p2 . k) = F(k) from FINSEQ_2:sch 1;

      

       A20: ( dom p2) = ( Seg ( len p2)) by FINSEQ_1:def 3

      .= ( dom p) by A18, FINSEQ_1:def 3;

      

       A21: ( len p1) = ( len p) by A1, A2, A3, RVSUM_1: 116;

      then

       A22: p1 is Element of (n -tuples_on REAL ) by FINSEQ_2: 92;

      

       A23: ( dom p2) = ( Seg n) by A18, FINSEQ_1:def 3;

      

       A24: ( len (q - p)) = ( len q) by A1, RVSUM_1: 116;

      

       A25: for k st k in ( dom q) holds ((q - p) . k) = ((q . k) - (p . k))

      proof

        let k;

        assume k in ( dom q);

        then k in ( dom (q - p)) by A24, FINSEQ_3: 29;

        hence thesis by VALUED_1: 13;

      end;

      

       A26: ( dom p) = ( Seg n) by FINSEQ_1:def 3;

      

       A27: ( dom (q - p)) = ( dom p2) by A1, A18, A24, FINSEQ_3: 29;

      

       A28: for k be Nat st k in ( dom p2) holds (p2 . k) = ((( log (2, number_e )) * (q - p)) . k)

      proof

        let k be Nat such that

         A29: k in ( dom p2);

        

         A30: (p . k) > 0 by A4, A20, A29;

        

        thus (p2 . k) = F(k) by A19, A29

        .= (( log (2, number_e )) * ((((p . k) / (p . k)) * (q . k)) - (p . k)))

        .= (( log (2, number_e )) * ((1 * (q . k)) - (p . k))) by A30, XCMPLX_1: 60

        .= (( log (2, number_e )) * ((q - p) . k)) by A27, A29, VALUED_1: 13

        .= ((( log (2, number_e )) * (q - p)) . k) by RVSUM_1: 44;

      end;

      ( dom p2) = ( dom (( log (2, number_e )) * (q - p))) by A27, VALUED_1:def 5;

      

      then

       A31: ( Sum p2) = ( Sum (( log (2, number_e )) * (q - p))) by A28, FINSEQ_1: 13

      .= (( log (2, number_e )) * ( Sum (q - p))) by RVSUM_1: 87

      .= (( log (2, number_e )) * (( Sum q) - ( Sum p))) by A1, A24, A25, Th8

      .= (( log (2, number_e )) * (1 - ( Sum p))) by MATRPROB:def 5

      .= (( log (2, number_e )) * (1 - 1)) by MATRPROB:def 5

      .= 0 ;

      ( number_e - 0 ) > (2 - 1) by TAYLOR_1: 11, XREAL_1: 15;

      then

       A32: ( log (2, number_e )) > 0 by Th4;

      

       A33: for k be Nat st k in ( Seg n) holds (p1 . k) <= (p2 . k)

      proof

        let k be Nat such that

         A34: k in ( Seg n);

        

         A35: k in ( dom p) by A34, FINSEQ_1:def 3;

        then

         A36: (p . k) > 0 by A4;

        (q . k) > 0 by A4, A35;

        then ((q . k) / (p . k)) > 0 by A36, XREAL_1: 139;

        then ( log ( number_e ,((q . k) / (p . k)))) <= (((q . k) / (p . k)) - 1) by Th3;

        then (((p . k) * ( log (2, number_e ))) * ( log ( number_e ,((q . k) / (p . k))))) <= (((p . k) * ( log (2, number_e ))) * (((q . k) / (p . k)) - 1)) by A32, A36, XREAL_1: 64;

        then (p1 . k) <= F(k) by A10, A35;

        hence thesis by A19, A23, A34;

      end;

      

       A37: p2 is Element of (n -tuples_on REAL ) by A18, FINSEQ_2: 92;

      hence ( Sum pp) <= ( Sum qq) by A8, A33, A22, A31, RVSUM_1: 82, XREAL_1: 50;

      

       A38: (ex k st k in ( Seg n) & (p . k) <> (q . k)) implies ( Sum pp) < ( Sum qq)

      proof

        assume ex k st k in ( Seg n) & (p . k) <> (q . k);

        then

        consider k1 be Nat such that

         A39: k1 in ( Seg n) and

         A40: (p . k1) <> (q . k1);

        

         A41: k1 in ( dom p) by A39, FINSEQ_1:def 3;

        then

         A42: (p . k1) > 0 by A4;

        then

         A43: ((p . k1) * ( log (2, number_e ))) > 0 by A32, XREAL_1: 129;

        (q . k1) > 0 by A4, A41;

        then

         A44: ((q . k1) / (p . k1)) > 0 by A42, XREAL_1: 139;

        ((q . k1) / (p . k1)) <> 1 by A40, XCMPLX_1: 58;

        then ( log ( number_e ,((q . k1) / (p . k1)))) < (((q . k1) / (p . k1)) - 1) by A44, Th3;

        then (((p . k1) * ( log (2, number_e ))) * ( log ( number_e ,((q . k1) / (p . k1))))) < (((p . k1) * ( log (2, number_e ))) * (((q . k1) / (p . k1)) - 1)) by A43, XREAL_1: 68;

        then (p1 . k1) < F(k1) by A10, A41;

        then (p1 . k1) < (p2 . k1) by A19, A23, A39;

        then (( Sum pp) - ( Sum qq)) < 0 by A8, A33, A22, A37, A31, A39, RVSUM_1: 83;

        hence thesis by XREAL_1: 48;

      end;

      

       A45: ( dom p1) = ( dom p2) by A21, A18, FINSEQ_3: 29;

      thus (for k st k in ( dom p) holds (p . k) = (q . k)) iff ( Sum pp) = ( Sum qq)

      proof

        hereby

          assume

           A46: for k st k in ( dom p) holds (p . k) = (q . k);

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

          proof

            let k be Nat such that

             A47: k in ( dom p);

            

             A48: (p . k) = (q . k) by A46, A47;

            (p . k) > 0 by A4, A47;

            then ((q . k) / (p . k)) = 1 by A48, XCMPLX_1: 60;

            then (((p . k) * ( log (2, number_e ))) * ( log ( number_e ,((q . k) / (p . k))))) = (((p . k) * ( log (2, number_e ))) * (((q . k) / (p . k)) - 1)) by Th3;

            then

             A49: (p1 . k) = F(k) by A10, A47;

            k in ( Seg n) by A47, FINSEQ_1:def 3;

            hence thesis by A19, A23, A49;

          end;

          then ( Sum p1) = 0 by A20, A45, A31, FINSEQ_1: 13;

          hence ( Sum pp) = ( Sum qq) by A8;

        end;

        assume

         A50: ( Sum pp) = ( Sum qq);

        assume not for k st k in ( dom p) holds (p . k) = (q . k);

        hence contradiction by A26, A38, A50;

      end;

      hence thesis by A26, A38;

    end;

    theorem :: ENTROPY1:58

    for p be non empty ProbFinS FinSequence of REAL st (for k st k in ( dom p) holds (p . k) > 0 ) holds ( Entropy p) <= ( log (2,( len p))) & ((for k st k in ( dom p) holds (p . k) = (1 / ( len p))) iff ( Entropy p) = ( log (2,( len p)))) & ((ex k st k in ( dom p) & (p . k) <> (1 / ( len p))) iff ( Entropy p) < ( log (2,( len p))))

    proof

      let p be non empty ProbFinS FinSequence of REAL such that

       A1: for k st k in ( dom p) holds (p . k) > 0 ;

      set p3 = ( - ( Infor_FinSeq_of p));

      set n = ( len p);

      reconsider n1 = n as non zero Element of NAT ;

      reconsider nn = (1 / n1) as Element of REAL by XREAL_0:def 1;

      reconsider p1 = (n |-> nn) as FinSequence of REAL ;

      deffunc F( Nat) = ( In (( - ((p . $1) * ( log (2,(p1 . $1))))), REAL ));

      consider p2 be FinSequence of REAL such that

       A2: ( len p2) = n and

       A3: for k be Nat st k in ( dom p2) holds (p2 . k) = F(k) from FINSEQ_2:sch 1;

      

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

      

       A5: for k be Nat st k in ( dom p2) holds (p2 . k) = ((( - ( log (2,(1 / n1)))) * p) . k)

      proof

        let k be Nat such that

         A6: k in ( dom p2);

        

        thus (p2 . k) = F(k) by A3, A6

        .= ( - ((p . k) * ( log (2,(1 / n1))))) by A4, A6, FINSEQ_2: 57

        .= (( - ( log (2,(1 / n1)))) * (p . k))

        .= ((( - ( log (2,(1 / n1)))) * p) . k) by RVSUM_1: 44;

      end;

      

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

      

       A8: ( dom ( Infor_FinSeq_of p)) = ( Seg ( len ( Infor_FinSeq_of p))) by FINSEQ_1:def 3

      .= ( Seg n) by Th47;

      

       A9: ( len p3) = n & for k st k in ( Seg n) holds (p3 . k) = ( - ((p . k) * ( log (2,(p . k)))))

      proof

        ( dom p3) = ( Seg n) by A8, VALUED_1: 8;

        hence ( len p3) = n by FINSEQ_1:def 3;

        hereby

          let k such that

           A10: k in ( Seg n);

          

          thus (p3 . k) = ( - (( Infor_FinSeq_of p) . k)) by RVSUM_1: 17

          .= ( - ((p . k) * ( log (2,(p . k))))) by A8, A10, Th47;

        end;

      end;

      ( dom p2) = ( dom p) by A2, FINSEQ_3: 29;

      then ( dom p2) = ( dom (( - ( log (2,(1 / n1)))) * p)) by VALUED_1:def 5;

      then p2 = (( - ( log (2,(1 / n1)))) * p) by A5, FINSEQ_1: 13;

      

      then

       A11: ( Sum p2) = (( - ( log (2,(1 / n1)))) * ( Sum p)) by RVSUM_1: 87

      .= (( - ( log (2,(1 / n1)))) * 1) by MATRPROB:def 5

      .= ( log (2,(1 / (1 / n1)))) by Th5

      .= ( log (2,n));

      

       A12: p1 is non empty ProbFinS FinSequence of REAL by Th16;

      

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

      

       A14: for k st k in ( dom p) holds (p . k) > 0 & (p1 . k) > 0 & (p3 . k) = ( - ((p . k) * ( log (2,(p . k))))) & (p2 . k) = ( - ((p . k) * ( log (2,(p1 . k)))))

      proof

        let k;

        assume

         A15: k in ( dom p);

        hence (p . k) > 0 & (p1 . k) > 0 by A1, FINSEQ_2: 57, A13;

        thus (p3 . k) = ( - ((p . k) * ( log (2,(p . k))))) by A15, A9, A13;

        (p2 . k) = F(k) by A15, A3, A4, A13;

        hence thesis;

      end;

      

       A16: ( Sum p3) = ( Entropy p) by RVSUM_1: 88;

      hence ( Entropy p) <= ( log (2,( len p))) by A7, A12, A2, A9, A14, A11, Th57;

      thus (for k st k in ( dom p) holds (p . k) = (1 / ( len p))) iff ( Entropy p) = ( log (2,( len p)))

      proof

        hereby

          assume

           A17: for k st k in ( dom p) holds (p . k) = (1 / ( len p));

          now

            let k such that

             A18: k in ( dom p);

            

            thus (p . k) = (1 / n) by A17, A18

            .= (p1 . k) by A13, A18, FINSEQ_2: 57;

          end;

          hence ( Entropy p) = ( log (2,n)) by A7, A12, A2, A9, A14, A16, A11, Th57;

        end;

        assume

         A19: ( Entropy p) = ( log (2,n));

        hereby

          let k;

          assume

           A20: k in ( dom p);

          

          hence (p . k) = (p1 . k) by A7, A12, A2, A9, A14, A16, A11, A19, Th57

          .= (1 / n) by A13, A20, FINSEQ_2: 57;

        end;

      end;

      

       A21: (for k st k in ( dom p) holds (p . k) = (p1 . k)) iff ( Sum p3) = ( Sum p2) by A7, A12, A2, A9, A14, Th57;

      thus (ex k st k in ( dom p) & (p . k) <> (1 / ( len p))) iff ( Entropy p) < ( log (2,( len p)))

      proof

        hereby

          assume ex k st k in ( dom p) & (p . k) <> (1 / ( len p));

          then

          consider k1 be Nat such that

           A22: k1 in ( dom p) and

           A23: (p . k1) <> (1 / n);

          (p1 . k1) <> (p . k1) by A13, A22, A23, FINSEQ_2: 57;

          hence ( Entropy p) < ( log (2,n)) by A7, A12, A2, A9, A14, A16, A11, A22, Th57;

        end;

        assume ( Entropy p) < ( log (2,n));

        then

        consider k1 be Nat such that

         A24: k1 in ( dom p) and

         A25: (p . k1) <> (p1 . k1) by A21, A11, RVSUM_1: 88;

        (p1 . k1) = (1 / n) by A13, A24, FINSEQ_2: 57;

        hence thesis by A24, A25;

      end;

    end;

    theorem :: ENTROPY1:59

    

     Th59: for M be m-nonnegative Matrix of REAL holds ( Mx2FinS ( Infor_FinSeq_of M)) = ( Infor_FinSeq_of ( Mx2FinS M))

    proof

      let M be m-nonnegative Matrix of REAL ;

      reconsider p = ( Mx2FinS M) as nonnegative FinSequence of REAL by Th43;

      set pp = ( Infor_FinSeq_of p);

      set qq = ( Mx2FinS ( Infor_FinSeq_of M));

      set MM = ( Infor_FinSeq_of M);

      

       A1: ( len p) = (( len M) * ( width M)) by Th39;

      

       A2: ( width MM) = ( width M) by Def8;

      ( len MM) = ( len M) by Def8;

      then

       A3: ( len qq) = (( len M) * ( width M)) by A2, Th39;

      ( len pp) = ( len p) by Th47;

      then

       A4: ( dom qq) = ( dom pp) by A1, A3, FINSEQ_3: 29;

      

       A5: ( dom qq) = ( dom p) by A1, A3, FINSEQ_3: 29;

      now

        let k be Nat such that

         A6: k in ( dom qq);

        k in ( Seg ( len qq)) by A6, FINSEQ_1:def 3;

        then k >= 1 by FINSEQ_1: 1;

        then

        reconsider l = (k - 1) as Nat by NAT_1: 21;

        set jj = ((l mod ( width MM)) + 1);

        set ii = ((l div ( width MM)) + 1);

        

         A7: [ii, jj] in ( Indices MM) by A6, Th41;

        

         A8: (qq . k) = (MM * (ii,jj)) by A6, Th41;

        

         A9: (p . k) = (M * (ii,jj)) by A2, A5, A6, Th41;

        

        thus (pp . k) = ((p . k) * ( log (2,(p . k)))) by A4, A6, Th47

        .= (qq . k) by A7, A8, A9, Th54;

      end;

      hence thesis by A4, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:60

    

     Th60: for p,q be ProbFinS FinSequence of REAL holds for M be Matrix of REAL st M = (( ColVec2Mx p) * ( LineVec2Mx q)) holds ( SumAll ( Infor_FinSeq_of M)) = (( Sum ( Infor_FinSeq_of p)) + ( Sum ( Infor_FinSeq_of q)))

    proof

      let p,q be ProbFinS FinSequence of REAL ;

      set p1 = ( Infor_FinSeq_of p);

      set p2 = (( Sum ( Infor_FinSeq_of q)) * p);

      

       A1: ( len p1) = ( len p) by Th47;

      ( dom p2) = ( dom p) by VALUED_1:def 5;

      then

       A2: ( len p1) = ( len p2) by A1, FINSEQ_3: 29;

      ( len ( FinSeq_log (2,q))) = ( len q) by Def6;

      then

       A3: ( len ( mlt (q,( FinSeq_log (2,q))))) = ( len q) by MATRPROB: 30;

      let M be Matrix of REAL such that

       A4: M = (( ColVec2Mx p) * ( LineVec2Mx q));

      reconsider M as Joint_Probability Matrix of REAL by A4, Th23;

      set M1 = ( Infor_FinSeq_of M);

      set L = ( LineSum M1);

      

       A5: ( len L) = ( len M1) by MATRPROB:def 1;

      then

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

      

       A7: ( len M1) = ( len M) by Def8;

      then

       A8: ( dom M1) = ( dom M) by FINSEQ_3: 29;

      

       A9: ( len M) = ( len p) by A4, Th22;

      then

       A10: ( dom M) = ( dom p) by FINSEQ_3: 29;

       A11:

      now

        let k such that

         A12: k in ( dom L);

        reconsider pp = ( Line (M,k)) as nonnegative FinSequence of REAL by A6, A8, A12, Th19;

        

         A13: pp = ((p . k) * q) by A4, A6, A8, A12, Th22;

        ( dom (((p . k) * ( log (2,(p . k)))) * q)) = ( dom q) by VALUED_1:def 5;

        then

         A14: ( len (((p . k) * ( log (2,(p . k)))) * q)) = ( len q) by FINSEQ_3: 29;

        ( dom ((p . k) * ( mlt (q,( FinSeq_log (2,q)))))) = ( dom ( mlt (q,( FinSeq_log (2,q))))) by VALUED_1:def 5;

        then

         A15: ( len (((p . k) * ( log (2,(p . k)))) * q)) = ( len ((p . k) * ( mlt (q,( FinSeq_log (2,q)))))) by A3, A14, FINSEQ_3: 29;

        

         A16: (p . k) >= 0 by A6, A8, A10, A12, Def1;

        

        thus (L . k) = ( Sum (M1 . k)) by A12, MATRPROB:def 1

        .= ( Sum ( Line (M1,k))) by A6, A12, MATRIX_0: 60

        .= ( Sum ( Infor_FinSeq_of pp)) by A6, A8, A12, Th53

        .= ( Sum ((((p . k) * ( log (2,(p . k)))) * q) + ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by A13, A16, Th51

        .= (( Sum (((p . k) * ( log (2,(p . k)))) * q)) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by A15, INTEGRA5: 2

        .= ((((p . k) * ( log (2,(p . k)))) * ( Sum q)) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by RVSUM_1: 87

        .= ((((p . k) * ( log (2,(p . k)))) * 1) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by MATRPROB:def 5

        .= (((p . k) * ( log (2,(p . k)))) + ((p . k) * ( Sum ( Infor_FinSeq_of q)))) by RVSUM_1: 87;

      end;

      

       A17: ( dom p1) = ( dom L) by A9, A7, A5, A1, FINSEQ_3: 29;

      now

        let k such that

         A18: k in ( dom p1);

        

        thus (L . k) = (((p . k) * ( log (2,(p . k)))) + ((p . k) * ( Sum ( Infor_FinSeq_of q)))) by A11, A17, A18

        .= ((p1 . k) + ((p . k) * ( Sum ( Infor_FinSeq_of q)))) by A18, Th47

        .= ((p1 . k) + (p2 . k)) by RVSUM_1: 44;

      end;

      

      then ( Sum L) = (( Sum p1) + ( Sum p2)) by A9, A7, A5, A1, A2, Th7

      .= (( Sum p1) + (( Sum ( Infor_FinSeq_of q)) * ( Sum p))) by RVSUM_1: 87

      .= (( Sum p1) + (( Sum ( Infor_FinSeq_of q)) * 1)) by MATRPROB:def 5

      .= (( Sum ( Infor_FinSeq_of p)) + ( Sum ( Infor_FinSeq_of q)));

      hence thesis by MATRPROB:def 3;

    end;

    definition

      let MR;

      :: ENTROPY1:def10

      func Entropy_of_Joint_Prob MR -> Real equals ( Entropy ( Mx2FinS MR));

      coherence ;

    end

    theorem :: ENTROPY1:61

    for p,q be ProbFinS FinSequence of REAL holds ( Entropy_of_Joint_Prob (( ColVec2Mx p) * ( LineVec2Mx q))) = (( Entropy p) + ( Entropy q))

    proof

      let p,q be ProbFinS FinSequence of REAL ;

      set M = (( ColVec2Mx p) * ( LineVec2Mx q));

      reconsider M as Joint_Probability Matrix of REAL by Th23;

      set pp = ( Mx2FinS (( ColVec2Mx p) * ( LineVec2Mx q)));

      reconsider pp as ProbFinS FinSequence of REAL by Th45;

      (( Entropy p) + ( Entropy q)) = ( - (( Sum ( Infor_FinSeq_of p)) + ( Sum ( Infor_FinSeq_of q))))

      .= ( - ( SumAll ( Infor_FinSeq_of M))) by Th60

      .= ( - ( Sum ( Mx2FinS ( Infor_FinSeq_of M)))) by Th42

      .= ( - ( Sum ( Infor_FinSeq_of pp))) by Th59;

      hence thesis;

    end;

    definition

      let MR;

      :: ENTROPY1:def11

      func Entropy_of_Cond_Prob MR -> FinSequence of REAL means

      : Def11: ( len it ) = ( len MR) & for k st k in ( dom it ) holds (it . k) = ( Entropy ( Line (MR,k)));

      existence

      proof

        deffunc F( Nat) = ( In (( Entropy ( Line (MR,$1))), REAL ));

        consider p be FinSequence of REAL such that

         A1: ( len p) = ( len MR) and

         A2: for k be Nat st k in ( dom p) holds (p . k) = F(k) from FINSEQ_2:sch 1;

        take p;

        thus ( len p) = ( len MR) by A1;

        let k;

        assume k in ( dom p);

        then (p . k) = F(k) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL such that

         A3: ( len p1) = ( len MR) and

         A4: for k st k in ( dom p1) holds (p1 . k) = ( Entropy ( Line (MR,k))) and

         A5: ( len p2) = ( len MR) and

         A6: for k st k in ( dom p2) holds (p2 . k) = ( Entropy ( Line (MR,k)));

        

         A7: ( dom p1) = ( dom p2) by A3, A5, FINSEQ_3: 29;

        now

          let k be Nat such that

           A8: k in ( dom p1);

          

          thus (p1 . k) = ( Entropy ( Line (MR,k))) by A4, A8

          .= (p2 . k) by A6, A7, A8;

        end;

        hence thesis by A7, FINSEQ_1: 13;

      end;

    end

    theorem :: ENTROPY1:62

    

     Th62: for M be non empty-yielding Conditional_Probability Matrix of REAL holds for p be FinSequence of REAL holds p = ( Entropy_of_Cond_Prob M) iff ( len p) = ( len M) & for k st k in ( dom p) holds (p . k) = ( - ( Sum (( Infor_FinSeq_of M) . k)))

    proof

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      let p be FinSequence of REAL ;

      

       A1: ( len ( Infor_FinSeq_of M)) = ( len M) by Def8;

      hereby

        assume

         A2: p = ( Entropy_of_Cond_Prob M);

        then

         A3: ( len p) = ( len M) by Def11;

        then

         A4: ( dom p) = ( dom M) by FINSEQ_3: 29;

        now

          let k such that

           A5: k in ( dom p);

          

           A6: k in ( dom ( Infor_FinSeq_of M)) by A1, A3, A5, FINSEQ_3: 29;

          

          thus (p . k) = ( Entropy ( Line (M,k))) by A2, A5, Def11

          .= ( - ( Sum ( Line (( Infor_FinSeq_of M),k)))) by A4, A5, Th53

          .= ( - ( Sum (( Infor_FinSeq_of M) . k))) by A6, MATRIX_0: 60;

        end;

        hence ( len p) = ( len M) & for k st k in ( dom p) holds (p . k) = ( - ( Sum (( Infor_FinSeq_of M) . k))) by A2, Def11;

      end;

      assume that

       A7: ( len p) = ( len M) and

       A8: for k st k in ( dom p) holds (p . k) = ( - ( Sum (( Infor_FinSeq_of M) . k)));

      

       A9: ( dom p) = ( dom M) by A7, FINSEQ_3: 29;

      

       A10: ( dom ( Infor_FinSeq_of M)) = ( dom M) by A1, FINSEQ_3: 29;

      now

        let k such that

         A11: k in ( dom p);

        

        thus (p . k) = ( - ( Sum (( Infor_FinSeq_of M) . k))) by A8, A11

        .= ( - ( Sum ( Line (( Infor_FinSeq_of M),k)))) by A10, A9, A11, MATRIX_0: 60

        .= ( Entropy ( Line (M,k))) by A9, A11, Th53;

      end;

      hence thesis by A7, Def11;

    end;

    theorem :: ENTROPY1:63

    

     Th63: for M be non empty-yielding Conditional_Probability Matrix of REAL holds ( Entropy_of_Cond_Prob M) = ( - ( LineSum ( Infor_FinSeq_of M)))

    proof

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      set p = ( Entropy_of_Cond_Prob M);

      set q = ( - ( LineSum ( Infor_FinSeq_of M)));

      

       A1: ( dom q) = ( dom ( LineSum ( Infor_FinSeq_of M))) by VALUED_1: 8;

      then ( len q) = ( len ( LineSum ( Infor_FinSeq_of M))) by FINSEQ_3: 29;

      then ( len q) = ( len ( Infor_FinSeq_of M)) by MATRPROB:def 1;

      then

       A2: ( len q) = ( len M) by Def8;

      ( len p) = ( len M) by Th62;

      then

       A3: ( dom p) = ( dom q) by A2, FINSEQ_3: 29;

      now

        let k be Nat such that

         A4: k in ( dom p);

        

        thus (p . k) = ( - ( Sum (( Infor_FinSeq_of M) . k))) by A4, Th62

        .= ( - (( Sum ( Infor_FinSeq_of M)) . k)) by A1, A3, A4, MATRPROB:def 1

        .= (q . k) by RVSUM_1: 17;

      end;

      hence thesis by A3, FINSEQ_1: 13;

    end;

    theorem :: ENTROPY1:64

    

     Th64: for p be ProbFinS FinSequence of REAL holds for M be non empty-yielding Conditional_Probability Matrix of REAL st ( len p) = ( len M) holds for M1 be Matrix of REAL st M1 = (( Vec2DiagMx p) * M) holds ( SumAll ( Infor_FinSeq_of M1)) = (( Sum ( Infor_FinSeq_of p)) + ( Sum ( mlt (p,( LineSum ( Infor_FinSeq_of M))))))

    proof

      let p be ProbFinS FinSequence of REAL ;

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      assume

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

      let M1 be Matrix of REAL such that

       A2: M1 = (( Vec2DiagMx p) * M);

      reconsider M1 as Joint_Probability Matrix of REAL by A1, A2, Th28;

      

       A3: ( len M1) = ( len p) by A1, A2, Th26;

      then

       A4: ( dom M1) = ( dom p) by FINSEQ_3: 29;

      set M2 = ( Infor_FinSeq_of M1);

      set L = ( LineSum M2);

      

       A5: ( len L) = ( len M2) by MATRPROB:def 1;

      then

       A6: ( dom L) = ( dom M2) by FINSEQ_3: 29;

      

       A7: ( len M2) = ( len M1) by Def8;

      then

       A8: ( dom M2) = ( dom M1) by FINSEQ_3: 29;

      

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

      

       A10: for k st k in ( dom L) holds (L . k) = (((p . k) * ( log (2,(p . k)))) + ((p . k) * ( Sum ( Infor_FinSeq_of ( Line (M,k))))))

      proof

        let k such that

         A11: k in ( dom L);

        reconsider pp = ( Line (M1,k)) as nonnegative FinSequence of REAL by A6, A8, A11, Th19;

        

         A12: (p . k) >= 0 by A6, A8, A4, A11, Def1;

        reconsider q = ( Line (M,k)) as non empty ProbFinS FinSequence of REAL by A6, A8, A4, A9, A11, MATRPROB: 60;

        

         A13: pp = ((p . k) * q) by A1, A2, A6, A8, A11, Th27;

        ( dom (((p . k) * ( log (2,(p . k)))) * q)) = ( dom q) by VALUED_1:def 5;

        then

         A14: ( len (((p . k) * ( log (2,(p . k)))) * q)) = ( len q) by FINSEQ_3: 29;

        ( len ( FinSeq_log (2,q))) = ( len q) by Def6;

        then

         A15: ( len ( mlt (q,( FinSeq_log (2,q))))) = ( len q) by MATRPROB: 30;

        ( dom ((p . k) * ( mlt (q,( FinSeq_log (2,q)))))) = ( dom ( mlt (q,( FinSeq_log (2,q))))) by VALUED_1:def 5;

        then

         A16: ( len ((p . k) * ( mlt (q,( FinSeq_log (2,q)))))) = ( len ( mlt (q,( FinSeq_log (2,q))))) by FINSEQ_3: 29;

        (L . k) = ( Sum (M2 . k)) by A11, MATRPROB:def 1

        .= ( Sum ( Line (M2,k))) by A6, A11, MATRIX_0: 60

        .= ( Sum ( Infor_FinSeq_of pp)) by A6, A8, A11, Th53

        .= ( Sum ((((p . k) * ( log (2,(p . k)))) * q) + ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by A13, A12, Th51

        .= (( Sum (((p . k) * ( log (2,(p . k)))) * q)) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by A15, A14, A16, INTEGRA5: 2

        .= ((((p . k) * ( log (2,(p . k)))) * ( Sum q)) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by RVSUM_1: 87

        .= ((((p . k) * ( log (2,(p . k)))) * 1) + ( Sum ((p . k) * ( mlt (q,( FinSeq_log (2,q))))))) by MATRPROB:def 5

        .= (((p . k) * ( log (2,(p . k)))) + ((p . k) * ( Sum ( Infor_FinSeq_of q)))) by RVSUM_1: 87;

        hence thesis;

      end;

      set M3 = ( Infor_FinSeq_of M);

      set L2 = ( LineSum M3);

      set p2 = ( mlt (p,L2));

      set p1 = ( Infor_FinSeq_of p);

      

       A17: ( len p1) = ( len p) by Th47;

      then

       A18: ( dom p1) = ( dom M) by A1, FINSEQ_3: 29;

      

       A19: ( len M3) = ( len M) by Def8;

      then

       A20: ( len L2) = ( len p) by A1, MATRPROB:def 1;

      then

       A21: ( len p2) = ( len p) by MATRPROB: 30;

      

       A22: ( dom p1) = ( dom M3) by A1, A19, A17, FINSEQ_3: 29;

      

       A23: ( dom L2) = ( dom p1) by A20, A17, FINSEQ_3: 29;

      

       A24: ( dom p1) = ( dom L) by A3, A7, A5, A17, FINSEQ_3: 29;

      now

        let k such that

         A25: k in ( dom p1);

        

         A26: (p2 . k) = ((p . k) * (L2 . k)) by RVSUM_1: 59

        .= ((p . k) * ( Sum (M3 . k))) by A23, A25, MATRPROB:def 1

        .= ((p . k) * ( Sum ( Line (M3,k)))) by A22, A25, MATRIX_0: 60

        .= ((p . k) * ( Sum ( Infor_FinSeq_of ( Line (M,k))))) by A18, A25, Th53;

        

        thus (L . k) = (((p . k) * ( log (2,(p . k)))) + ((p . k) * ( Sum ( Infor_FinSeq_of ( Line (M,k)))))) by A10, A24, A25

        .= ((p1 . k) + (p2 . k)) by A25, A26, Th47;

      end;

      then ( Sum L) = (( Sum ( Infor_FinSeq_of p)) + ( Sum ( mlt (p,( LineSum ( Infor_FinSeq_of M)))))) by A3, A7, A5, A17, A21, Th7;

      hence thesis by MATRPROB:def 3;

    end;

    theorem :: ENTROPY1:65

    for p be ProbFinS FinSequence of REAL holds for M be non empty-yielding Conditional_Probability Matrix of REAL st ( len p) = ( len M) holds ( Entropy_of_Joint_Prob (( Vec2DiagMx p) * M)) = (( Entropy p) + ( Sum ( mlt (p,( Entropy_of_Cond_Prob M)))))

    proof

      let p be ProbFinS FinSequence of REAL ;

      let M be non empty-yielding Conditional_Probability Matrix of REAL ;

      set M1 = (( Vec2DiagMx p) * M);

      assume

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

      then

      reconsider M1 as Joint_Probability Matrix of REAL by Th28;

      

       A2: (( Entropy p) + ( Sum ( mlt (p,( Entropy_of_Cond_Prob M))))) = (( - ( Sum ( Infor_FinSeq_of p))) + ( Sum ( mlt (p,( - ( LineSum ( Infor_FinSeq_of M))))))) by Th63

      .= (( - ( Sum ( Infor_FinSeq_of p))) + ( Sum ( - ( mlt (p,( LineSum ( Infor_FinSeq_of M))))))) by RVSUM_1: 65

      .= (( - ( Sum ( Infor_FinSeq_of p))) + ( - ( Sum ( mlt (p,( LineSum ( Infor_FinSeq_of M))))))) by RVSUM_1: 88;

      ( Entropy_of_Joint_Prob M1) = ( - ( Sum ( Mx2FinS ( Infor_FinSeq_of M1)))) by Th59

      .= ( - ( SumAll ( Infor_FinSeq_of M1))) by Th42

      .= ( - (( Sum ( Infor_FinSeq_of p)) + ( Sum ( mlt (p,( LineSum ( Infor_FinSeq_of M))))))) by A1, Th64

      .= (( - ( Sum ( Infor_FinSeq_of p))) - ( Sum ( mlt (p,( LineSum ( Infor_FinSeq_of M))))));

      hence thesis by A2;

    end;