let p be FinSequence of REAL ; :: thesis: ( p is nonnegative implies for k being Element of NAT st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k )
assume A1: p is nonnegative ; :: thesis: for k being Element of NAT st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k
let k1 be Element of NAT ; :: thesis: ( k1 in dom p & p . k1 = Sum p implies p has_onlyone_value_in k1 )
assume A2: ( k1 in dom p & p . k1 = Sum p ) ; :: thesis: p has_onlyone_value_in k1
A3: ( k1 >= 1 & k1 <= len p ) by A2, FINSEQ_3:27;
then consider j1 being Nat such that
A4: k1 + j1 = len p by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
for i being Element of NAT holds
( not i in dom p or not i <> k1 or not p . i <> 0 )

proof

assume ex i being Element of NAT st
( i in dom p & i <> k1 & p . i <> 0 ) ; :: thesis: contradiction
then consider k2 being Element of NAT such that
A5: ( k2 in dom p & k2 <> k1 & p . k2 <> 0 ) ;
A6: ( k2 >= 1 & k2 <= len p ) by A5, FINSEQ_3:27;
then consider j2 being Nat such that
A7: k2 + j2 = len p by NAT_1:10;
reconsider j2 = j2 as Element of NAT by ORDINAL1:def 13;
A8: p . k2 > 0 by A1, A5, Def1;

per cases ( k1 > k2 or k1 < k2 ) by A5, XXREAL_0:1;

suppose k1 > k2 ; :: thesis: contradiction

then A9: not k1 in Seg k2 by FINSEQ_1:3;
consider p1, p2 being FinSequence of REAL such that
A10: ( len p1 = k2 & len p2 = j2 & p = p1 ^ p2 ) by A7, FINSEQ_2:26;
k2 in Seg k2 by A6, FINSEQ_1:5;
then A11: k2 in dom p1 by A10, FINSEQ_1:def 3;
( p1 . k2 > 0 & ( for k being Nat st k in dom p1 holds
p1 . k >= 0 ) )

proof

thus p1 . k2 > 0 by A8, A10, A11, FINSEQ_1:def 7; :: thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
let k be Nat; :: thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A12: k in dom p1 ; :: thesis: p1 . k >= 0
A13: dom p1 c= dom p by A10, FINSEQ_1:39;
p1 . k = p . k by A10, A12, FINSEQ_1:def 7;
hence p1 . k >= 0 by A1, A12, A13, Def1; :: thesis: verum

end;

then A14: Sum p1 > 0 by A11, RVSUM_1:115;
not k1 in dom p1 by A9, A10, FINSEQ_1:def 3;
then consider kk being Nat such that
A15: ( kk in dom p2 & k1 = k2 + kk ) by A2, A10, FINSEQ_1:38;
A16: p2 . kk = p . k1 by A10, A15, FINSEQ_1:def 7;
for k being Nat st k in dom p2 holds
p2 . k >= 0

proof

let k be Nat; :: thesis: ( k in dom p2 implies p2 . k >= 0 )
assume A17: k in dom p2 ; :: thesis: p2 . k >= 0
( k >= 1 & k <= j2 ) by A10, A17, FINSEQ_3:27;
then ( k2 + k >= 1 + 0 & k2 + k <= len p ) by A7, XREAL_1:9;
then A18: k2 + k in dom p by FINSEQ_3:27;
p2 . k = p . (k2 + k) by A10, A17, FINSEQ_1:def 7;
hence p2 . k >= 0 by A1, A18, Def1; :: thesis: verum

end;

then A19: Sum p2 >= p . k1 by A15, A16, MATRPROB:5;
Sum p = (Sum p1) + (Sum p2) by A10, RVSUM_1:105;
then Sum p > (p . k1) + 0 by A14, A19, XREAL_1:10;
hence contradiction by A2; :: thesis: verum

end;

suppose k1 < k2 ; :: thesis: contradiction

then A20: not k2 in Seg k1 by FINSEQ_1:3;
consider p1, p2 being FinSequence of REAL such that
A21: ( len p1 = k1 & len p2 = j1 & p = p1 ^ p2 ) by A4, FINSEQ_2:26;
k1 in Seg k1 by A3, FINSEQ_1:5;
then A22: k1 in dom p1 by A21, FINSEQ_1:def 3;
( p1 . k1 = p . k1 & ( for k being Nat st k in dom p1 holds
p1 . k >= 0 ) )

proof

thus p1 . k1 = p . k1 by A21, A22, FINSEQ_1:def 7; :: thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
let k be Nat; :: thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A23: k in dom p1 ; :: thesis: p1 . k >= 0
A24: dom p1 c= dom p by A21, FINSEQ_1:39;
p1 . k = p . k by A21, A23, FINSEQ_1:def 7;
hence p1 . k >= 0 by A1, A23, A24, Def1; :: thesis: verum

end;

then A25: Sum p1 >= p . k1 by A22, MATRPROB:5;
not k2 in dom p1 by A20, A21, FINSEQ_1:def 3;
then consider kk being Nat such that
A26: ( kk in dom p2 & k2 = k1 + kk ) by A5, A21, FINSEQ_1:38;
A27: p2 . kk = p . k2 by A21, A26, FINSEQ_1:def 7;
for k being Nat st k in dom p2 holds
p2 . k >= 0

proof

let k be Nat; :: thesis: ( k in dom p2 implies p2 . k >= 0 )
assume A28: k in dom p2 ; :: thesis: p2 . k >= 0
( k >= 1 & k <= j1 ) by A21, A28, FINSEQ_3:27;
then ( k1 + k >= 1 + 0 & k1 + k <= len p ) by A4, XREAL_1:9;
then A29: k1 + k in dom p by FINSEQ_3:27;
p2 . k = p . (k1 + k) by A21, A28, FINSEQ_1:def 7;
hence p2 . k >= 0 by A1, A29, Def1; :: thesis: verum

end;

then A30: Sum p2 > 0 by A8, A26, A27, RVSUM_1:115;
Sum p = (Sum p1) + (Sum p2) by A21, RVSUM_1:105;
then Sum p > (p . k1) + 0 by A25, A30, XREAL_1:10;
hence contradiction by A2; :: thesis: verum

end;

end;

end;

hence p has_onlyone_value_in k1 by A2, Def2; :: thesis: verum