let n be Element of 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 A1: ( Sum R = 0 & ( 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
A2: for i being Nat st i in dom R holds
0 <= R . i by A1;
given k being Element of NAT such that A3: ( k in dom R & R . k <> 0 ) ; :: thesis: contradiction
0 <= R . k by A1, A3;
hence contradiction by A1, A2, A3, RVSUM_1:115; :: thesis: verum