theorem Th2: :: EUCLID_2:2

for n being Nat
for v being Element of n -tuples_on REAL holds mlt (v,(0* n)) = 0* n