let n be Nat; :: thesis: for R being Element of n -tuples_on REAL st Sum R = 0 & ( for i being Element of NAT st i in dom R holds
0 <= R . i ) holds
for i being Element of NAT st i in dom R holds
R . i = 0
let R be Element of n -tuples_on REAL; :: thesis: ( Sum R = 0 & ( for i being Element of NAT st i in dom R holds
0 <= R . i ) implies for i being Element of NAT st i in dom R holds
R . i = 0 )
assume that
A1: Sum R = 0 and
A2: for i being Element of NAT st i in dom R holds
0 <= R . i ; :: thesis: for i being Element of NAT st i in dom R holds
R . i = 0
A3: for i being Nat st i in dom R holds
0 <= R . i by A2;
given k being Element of NAT such that A4: k in dom R and
A5: R . k <> 0 ; :: thesis: contradiction
0 <= R . k by A2, A4;
hence contradiction by A1, A3, A4, A5, RVSUM_1:85; :: thesis: verum