theorem Th23: :: RLAFFIN1:23

for r being Real
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R st r <> 0 holds
Carrier (r (*) LR) = r * (Carrier LR)