theorem Th3: :: RFUNCT_4:3

for n being Nat
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