let p, q be non empty ProbFinS FinSequence of REAL ; :: thesis: for pp, qq being FinSequence of REAL st len p = len q & len pp = len p & len qq = len q & ( for k being Nat 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 being Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Nat st
( k in dom p & p . k <> q . k ) ) )
let pp, qq be FinSequence of REAL ; :: thesis: ( len p = len q & len pp = len p & len qq = len q & ( for k being Nat 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)))) ) ) implies ( Sum pp <= Sum qq & ( ( for k being Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Nat st
( k in dom p & p . k <> q . k ) ) ) )
assume that
A1: len p = len q and
A2: len pp = len p and
A3: len qq = len q and
A4: for k being Nat 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)))) ) ; :: thesis: ( Sum pp <= Sum qq & ( ( for k being Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Nat st
( k in dom p & p . k <> 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 being Nat 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 being Nat st k in dom p holds
(pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k))))

proof

let k be Nat; :: thesis: ( k in dom p implies (pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k)))) )
assume A11: k in dom p ; :: thesis: (pp - qq) . k = ((p . k) * (log (2,number_e))) * (log (number_e,((q . k) / (p . k))))
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 (pp - qq) . 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 ; :: thesis: verum

end;

set n = len p;
deffunc H₁( Nat) -> Element of REAL = In ((((p . $1) * (log (2,number_e))) * (((q . $1) / (p . $1)) - 1)),REAL);
consider p2 being FinSequence of REAL such that
A18: len p2 = len p and
A19: for k being Nat st k in dom p2 holds
p2 . k = H₁(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 (pp - qq) = len p by A1, A2, A3, RVSUM_1:116;
then A22: pp - qq is Element of (len p) -tuples_on REAL by FINSEQ_2:92;
A23: dom p2 = Seg (len p) by A18, FINSEQ_1:def 3;
A24: len (q - p) = len q by A1, RVSUM_1:116;
A25: for k being Nat st k in dom q holds
(q - p) . k = (q . k) - (p . k)

proof

let k be Nat; :: thesis: ( k in dom q implies (q - p) . k = (q . k) - (p . k) )
assume k in dom q ; :: thesis: (q - p) . k = (q . k) - (p . k)
then k in dom (q - p) by A24, FINSEQ_3:29;
hence (q - p) . k = (q . k) - (p . k) by VALUED_1:13; :: thesis: verum

end;

A26: dom p = Seg (len p) by FINSEQ_1:def 3;
A27: dom (q - p) = dom p2 by A1, A18, A24, FINSEQ_3:29;
A28: for k being Nat st k in dom p2 holds
p2 . k = ((log (2,number_e)) * (q - p)) . k

proof

let k be Nat; :: thesis: ( k in dom p2 implies p2 . k = ((log (2,number_e)) * (q - p)) . k )
assume A29: k in dom p2 ; :: thesis: p2 . k = ((log (2,number_e)) * (q - p)) . k
A30: p . k > 0 by A4, A20, A29;
thus p2 . k = H₁(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 ; :: thesis: verum

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 being Nat st k in Seg (len p) holds
(pp - qq) . k <= p2 . k

proof

let k be Nat; :: thesis: ( k in Seg (len p) implies (pp - qq) . k <= p2 . k )
assume A34: k in Seg (len p) ; :: thesis: (pp - qq) . k <= p2 . k
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 (pp - qq) . k <= H₁(k) by A10, A35;
hence (pp - qq) . k <= p2 . k by A19, A23, A34; :: thesis: verum

end;

A37: p2 is Element of (len p) -tuples_on REAL by A18, FINSEQ_2:92;
hence Sum pp <= Sum qq by A8, A33, A22, A31, RVSUM_1:82, XREAL_1:50; :: thesis: ( ( ( for k being Nat st k in dom p holds
p . k = q . k ) implies Sum pp = Sum qq ) & ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k ) & ( ex k being Nat st
( k in dom p & p . k <> q . k ) implies Sum pp < Sum qq ) & ( Sum pp < Sum qq implies ex k being Nat st
( k in dom p & p . k <> q . k ) ) )
A38: ( ex k being Nat st
( k in Seg (len p) & p . k <> q . k ) implies Sum pp < Sum qq )

proof

assume ex k being Nat st
( k in Seg (len p) & p . k <> q . k ) ; :: thesis: Sum pp < Sum qq
then consider k1 being Nat such that
A39: k1 in Seg (len p) 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 (pp - qq) . k1 < H₁(k1) by A10, A41;
then (pp - qq) . k1 < p2 . k1 by A19, A23, A39;
then (Sum pp) - (Sum qq) < 0 by A8, A33, A22, A37, A31, A39, RVSUM_1:83;
hence Sum pp < Sum qq by XREAL_1:48; :: thesis: verum

end;

A45: dom (pp - qq) = dom p2 by A21, A18, FINSEQ_3:29;
thus ( ( for k being Nat st k in dom p holds
p . k = q . k ) iff Sum pp = Sum qq ) :: thesis: ( ex k being Nat st
( k in dom p & p . k <> q . k ) iff Sum pp < Sum qq )

proof

hereby :: thesis: ( Sum pp = Sum qq implies for k being Nat st k in dom p holds
p . k = q . k )

assume A46: for k being Nat st k in dom p holds
p . k = q . k ; :: thesis: Sum pp = Sum qq
for k being Nat st k in dom p holds
(pp - qq) . k = p2 . k

proof

let k be Nat; :: thesis: ( k in dom p implies (pp - qq) . k = p2 . k )
assume A47: k in dom p ; :: thesis: (pp - qq) . k = p2 . k
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: (pp - qq) . k = H₁(k) by A10, A47;
k in Seg (len p) by A47, FINSEQ_1:def 3;
hence (pp - qq) . k = p2 . k by A19, A23, A49; :: thesis: verum

end;

then Sum (pp - qq) = 0 by A20, A45, A31, FINSEQ_1:13;
hence Sum pp = Sum qq by A8; :: thesis: verum

end;

assume A50: Sum pp = Sum qq ; :: thesis: for k being Nat st k in dom p holds
p . k = q . k
assume ex k being Nat st
( k in dom p & not p . k = q . k ) ; :: thesis: contradiction
hence contradiction by A26, A38, A50; :: thesis: verum

end;

hence ( ex k being Nat st
( k in dom p & p . k <> q . k ) iff Sum pp < Sum qq ) by A26, A38; :: thesis: verum