theorem Th5: :: RFUNCT_4:5

for n being Nat
for R being Element of n -tuples_on REAL holds mlt ((n |-> 0),R) = n |-> 0