theorem :: EUCLID_4:4

for a, b being Real
for n being Nat
for x being Element of REAL n holds (a * b) * x = a * (b * x) by RVSUM_1:49;