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

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