let k be Nat; :: thesis: for p being FinSequence of REAL st p has_onlyone_value_in k holds
Sum p = p . k
let p be FinSequence of REAL ; :: thesis: ( p has_onlyone_value_in k implies Sum p = p . k )
assume that
A1: k in dom p and
A2: for i being Nat st i in dom p & i <> k holds
p . i = 0 ; :: according to ENTROPY1:def 2 :: thesis: Sum p = p . k
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 being FinSequence such that
A3: p = p1 ^ p2 by TREES_1:1;
reconsider p2 = 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 being Nat st i in Seg (len p2) holds
p2 . i = 0
proof
let i be Nat; :: thesis: ( i in Seg (len p2) implies p2 . i = 0 )
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) ; :: thesis: p2 . i = 0
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 ; :: thesis: verum
end;
A12: now :: thesis: for j being Nat st j in dom p2 holds
p2 . j = ((len p2) |-> 0) . j
let j be Nat; :: thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> 0) . j )
assume A13: j in dom p2 ; :: thesis: p2 . j = ((len p2) |-> 0) . j
hence p2 . j = 0 by A7, A4
.= ((len p2) |-> 0) . j by A4, A13, FINSEQ_2:57 ;
:: thesis: verum
end;
p1 <> {} by A5, RELAT_1:38, RELAT_1:61;
then len p1 <> 0 ;
then consider p3 being FinSequence of REAL , x being 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 being Nat st i in Seg (len p3) holds
p3 . i = 0
proof
let i be Nat; :: thesis: ( i in Seg (len p3) implies p3 . i = 0 )
assume A19: i in Seg (len p3) ; :: thesis: p3 . i = 0
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 ; :: thesis: verum
end;
A23: now :: thesis: for j being Nat st j in dom p3 holds
p3 . j = ((len p3) |-> 0) . j
let j be Nat; :: thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> 0) . j )
assume A24: j in dom p3 ; :: thesis: p3 . j = ((len p3) |-> 0) . j
hence p3 . j = 0 by A18, A17
.= ((len p3) |-> 0) . j by A17, A24, FINSEQ_2:57 ;
:: thesis: verum
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 Sum p = p . k ; :: thesis: verum