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 A1: ( k in dom p & ( 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 ;
A2: ( 1 <= k & k <= len p ) by A1, FINSEQ_3:27;
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;
k in Seg k by A2, FINSEQ_1:5;
then B4: k in (dom p) /\ (Seg k) by A1, XBOOLE_0:def 4;
then A4: k in dom p1 by RELAT_1:90;
p1 <> {} by B4, RELAT_1:60, RELAT_1:90;
then len p1 <> 0 ;
then consider p3 being FinSequence of REAL , x being Element of REAL such that
A5: p1 = p3 ^ <*x*> by FINSEQ_2:22;
reconsider p2 = p2 as FinSequence of REAL by A3, FINSEQ_1:50;
A6: k = len p1 by A2, FINSEQ_1:21
.= (len p3) + (len <*x*>) by A5, FINSEQ_1:35
.= (len p3) + 1 by FINSEQ_1:56 ;
then A7: x = p1 . k by A5, FINSEQ_1:59
.= a by A3, A4, FINSEQ_1:def 7 ;
A8: 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 )
assume i in Seg (len p2) ; :: thesis: p2 . i = 0
then A9: i in dom p2 by FINSEQ_1:def 3;
A10: ( 1 <= k & k <= len p1 ) by A4, FINSEQ_3:27;
0 <> i by A9, FINSEQ_3:27;
then A11: len p1 <> (len p1) + i ;
len p1 <= (len p1) + i by NAT_1:12;
then A12: k <> (len p1) + i by A10, A11, XXREAL_0:1;
thus p2 . i = p . ((len p1) + i) by A3, A9, FINSEQ_1:def 7
.= 0 by A1, A3, A9, A12, FINSEQ_1:41 ; :: thesis: verum

end;

A13: p2 = (len p2) |-> 0

proof

A14: len ((len p2) |-> 0 ) = len p2 by FINSEQ_1:def 18;
X: dom p2 = Seg (len p2) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom p2 implies p2 . j = ((len p2) |-> 0 ) . j )
assume A15: j in dom p2 ; :: thesis: p2 . j = ((len p2) |-> 0 ) . j
hence p2 . j = 0 by A8, X
.= ((len p2) |-> 0 ) . j by A15, X, FINSEQ_2:71 ;
:: thesis: verum

end;

hence p2 = (len p2) |-> 0 by A14, FINSEQ_2:10; :: thesis: verum

end;

A16: 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 A17: i in Seg (len p3) ; :: thesis: p3 . i = 0
then ( 1 <= i & i <= len p3 ) by FINSEQ_1:3;
then A18: i <> k by A6, NAT_1:13;
A19: i in dom p3 by A17, FINSEQ_1:def 3;
then A20: i in dom p1 by A5, FINSEQ_2:18;
thus p3 . i = p1 . i by A5, A19, FINSEQ_1:def 7
.= p . i by A3, A20, FINSEQ_1:def 7
.= 0 by A1, A3, A18, A20, FINSEQ_2:18 ; :: thesis: verum

end;

A21: p3 = (len p3) |-> 0

proof

A22: len ((len p3) |-> 0 ) = len p3 by FINSEQ_1:def 18;
X: dom p3 = Seg (len p3) by FINSEQ_1:def 3;

now

let j be Nat; :: thesis: ( j in dom p3 implies p3 . j = ((len p3) |-> 0 ) . j )
assume A23: j in dom p3 ; :: thesis: p3 . j = ((len p3) |-> 0 ) . j
hence p3 . j = 0 by A16, X
.= ((len p3) |-> 0 ) . j by A23, X, FINSEQ_2:71 ;
:: thesis: verum

end;

hence p3 = (len p3) |-> 0 by A22, FINSEQ_2:10; :: thesis: verum

end;

Sum p = (Sum (p3 ^ <*x*>)) + (Sum ((len p2) |-> 0 )) by A3, A5, A13, RVSUM_1:105
.= (Sum (p3 ^ <*x*>)) + 0 by RVSUM_1:111
.= (Sum ((len p3) |-> 0 )) + x by A21, RVSUM_1:104
.= 0 + a by A7, RVSUM_1:111
.= p . k ;
hence Sum p = p . k ; :: thesis: verum