let p be FinSequence of REAL ; :: thesis: ( p is nonnegative implies for k being 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 Nat st k in dom p & p . k = Sum p holds
p has_onlyone_value_in k
let k1 be Nat; :: thesis: ( k1 in dom p & p . k1 = Sum p implies p has_onlyone_value_in k1 )
assume that
A2: k1 in dom p and
A3: p . k1 = Sum p ; :: thesis: p has_onlyone_value_in k1
k1 <= len p by A2, FINSEQ_3:25;
then consider j1 being Nat such that
A4: k1 + j1 = len p by NAT_1:10;
reconsider j1 = j1 as Nat ;
A5: k1 >= 1 by A2, FINSEQ_3:25;
for i being Nat holds
( not i in dom p or not i <> k1 or not p . i <> 0 )

proof

assume ex i being Nat st
( i in dom p & i <> k1 & p . i <> 0 ) ; :: thesis: contradiction
then consider k2 being Nat such that
A6: k2 in dom p and
A7: k2 <> k1 and
A8: p . k2 <> 0 ;
A9: p . k2 > 0 by A1, A6, A8;
k2 <= len p by A6, FINSEQ_3:25;
then consider j2 being Nat such that
A10: k2 + j2 = len p by NAT_1:10;
reconsider j2 = j2 as Nat ;
A11: k2 >= 1 by A6, FINSEQ_3:25;

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

suppose A12: k1 > k2 ; :: thesis: contradiction

consider p1, p2 being FinSequence of REAL such that
A13: len p1 = k2 and
A14: len p2 = j2 and
A15: p = p1 ^ p2 by A10, FINSEQ_2:23;
A16: 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 by A17, FINSEQ_3:25;
then A18: k2 + k >= 1 + 0 by XREAL_1:7;
k <= j2 by A14, A17, FINSEQ_3:25;
then k2 + k <= len p by A10, XREAL_1:7;
then A19: k2 + k in dom p by A18, FINSEQ_3:25;
p2 . k = p . (k2 + k) by A13, A15, A17, FINSEQ_1:def 7;
hence p2 . k >= 0 by A1, A19; :: thesis: verum

end;

k2 in Seg k2 by A11, FINSEQ_1:3;
then A20: k2 in dom p1 by A13, 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 A9, A15, A20, FINSEQ_1:def 7; :: thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
A21: dom p1 c= dom p by A15, FINSEQ_1:26;
let k be Nat; :: thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A22: k in dom p1 ; :: thesis: p1 . k >= 0
p1 . k = p . k by A15, A22, FINSEQ_1:def 7;
hence p1 . k >= 0 by A1, A22, A21; :: thesis: verum

end;

then A23: Sum p1 > 0 by A20, RVSUM_1:85;
not k1 in Seg k2 by A12, FINSEQ_1:1;
then not k1 in dom p1 by A13, FINSEQ_1:def 3;
then consider kk being Nat such that
A24: kk in dom p2 and
A25: k1 = k2 + kk by A2, A13, A15, FINSEQ_1:25;
p2 . kk = p . k1 by A13, A15, A24, A25, FINSEQ_1:def 7;
then A26: Sum p2 >= p . k1 by A24, A16, MATRPROB:5;
Sum p = (Sum p1) + (Sum p2) by A15, RVSUM_1:75;
then Sum p > (p . k1) + 0 by A23, A26, XREAL_1:8;
hence contradiction by A3; :: thesis: verum

end;

suppose A27: k1 < k2 ; :: thesis: contradiction

consider p1, p2 being FinSequence of REAL such that
A28: len p1 = k1 and
A29: len p2 = j1 and
A30: p = p1 ^ p2 by A4, FINSEQ_2:23;
A31: 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 A32: k in dom p2 ; :: thesis: p2 . k >= 0
k >= 1 by A32, FINSEQ_3:25;
then A33: k1 + k >= 1 + 0 by XREAL_1:7;
k <= j1 by A29, A32, FINSEQ_3:25;
then k1 + k <= len p by A4, XREAL_1:7;
then A34: k1 + k in dom p by A33, FINSEQ_3:25;
p2 . k = p . (k1 + k) by A28, A30, A32, FINSEQ_1:def 7;
hence p2 . k >= 0 by A1, A34; :: thesis: verum

end;

k1 in Seg k1 by A5, FINSEQ_1:3;
then A35: k1 in dom p1 by A28, 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 A30, A35, FINSEQ_1:def 7; :: thesis: for k being Nat st k in dom p1 holds
p1 . k >= 0
A36: dom p1 c= dom p by A30, FINSEQ_1:26;
let k be Nat; :: thesis: ( k in dom p1 implies p1 . k >= 0 )
assume A37: k in dom p1 ; :: thesis: p1 . k >= 0
p1 . k = p . k by A30, A37, FINSEQ_1:def 7;
hence p1 . k >= 0 by A1, A37, A36; :: thesis: verum

end;

then A38: Sum p1 >= p . k1 by A35, MATRPROB:5;
not k2 in Seg k1 by A27, FINSEQ_1:1;
then not k2 in dom p1 by A28, FINSEQ_1:def 3;
then consider kk being Nat such that
A39: kk in dom p2 and
A40: k2 = k1 + kk by A6, A28, A30, FINSEQ_1:25;
p2 . kk = p . k2 by A28, A30, A39, A40, FINSEQ_1:def 7;
then A41: Sum p2 > 0 by A9, A39, A31, RVSUM_1:85;
Sum p = (Sum p1) + (Sum p2) by A30, RVSUM_1:75;
then Sum p > (p . k1) + 0 by A38, A41, XREAL_1:8;
hence contradiction by A3; :: thesis: verum

end;

end;

end;

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