let k be Element of 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 Element of 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 ;
reconsider p1 = p | (Seg k) as FinSequence of REAL by FINSEQ_1:23;
p1 c= p by TREES_1:def 1;
then consider p2 being FinSequence such that
A3: p = p1 ^ p2 by TREES_1:8;
reconsider p2 = p2 as FinSequence of REAL by A3, FINSEQ_1:50;
A4: dom p2 = Seg (len p2) by FINSEQ_1:def 3;
1 <= k by A1, FINSEQ_3:27;
then k in Seg k by FINSEQ_1:5;
then A5: k in (dom p) /\ (Seg k) by A1, XBOOLE_0:def 4;
then A6: k in dom p1 by RELAT_1:90;
A7: for i being Element of NAT st i in Seg (len p2) holds
p2 . i = 0

proof

let i be Element of 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:27;
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:27;
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:41 ; :: thesis: verum

end;

A12: now

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:71 ;
:: thesis: verum

end;

p1 <> {} by A5, RELAT_1:60, RELAT_1:90;
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:22;
k <= len p by A1, FINSEQ_3:27;
then A15: k = len p1 by FINSEQ_1:21
.= (len p3) + (len <*x*>) by A14, FINSEQ_1:35
.= (len p3) + 1 by FINSEQ_1:56 ;
then A16: x = p1 . k by A14, FINSEQ_1:59
.= a by A3, A6, FINSEQ_1:def 7 ;
A17: dom p3 = Seg (len p3) by FINSEQ_1:def 3;
A18: for i being Element of NAT st i in Seg (len p3) holds
p3 . i = 0

proof

let i be Element of 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:3;
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:18;
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:18 ; :: thesis: verum

end;

A23: now

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:71 ;
:: thesis: verum

end;

len ((len p3) |-> 0 ) = len p3 by FINSEQ_1:def 18;
then A25: p3 = (len p3) |-> 0 by A23, FINSEQ_2:10;
len ((len p2) |-> 0 ) = len p2 by FINSEQ_1:def 18;
then p2 = (len p2) |-> 0 by A12, FINSEQ_2:10;
then Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> 0 )) by A3, A14, RVSUM_1:105
.= (Sum (p3 ^ <*x*>)) + 0 by RVSUM_1:111
.= (Sum ((len p3) |-> 0 )) + x by A25, RVSUM_1:104
.= 0 + a by A16, RVSUM_1:111
.= p . k ;
hence Sum p = p . k ; :: thesis: verum