theorem Th1: :: EUCLIDLP:1

for s, t, u being Real
for n being Nat
for x being Element of REAL n holds
( (s / t) * (u * x) = ((s * u) / t) * x & (1 / t) * (u * x) = (u / t) * x )