theorem Th2: :: EUCLID_4:2

for a being Real
for n being Nat holds a * (0* n) = 0* n