theorem :: RVSUM_1:91
for i being natural Number
for R being Element of i -tuples_on REAL st Sum (sqr R) = 0 holds
R = i |-> 0