theorem Th4: :: RFUNCT_4:4

for n being Nat
for R being Element of n -tuples_on REAL st ( for i being Element of NAT st i in dom R holds
0 = R . i ) holds
R = n |-> 0