theorem Th10: :: RLAFFIN1:10
for r, s being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for AR being Subset of R holds (r * s) * AR = r * (s * AR)