:: deftheorem Def2 defines (*) RLAFFIN1:def 2 :
for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R
for r being Real
for b₄ being Linear_Combination of R holds
( ( r <> 0 implies ( b₄ = r (*) LR iff for v being Element of R holds b₄ . v = LR . ((r ") * v) ) ) & ( not r <> 0 implies ( b₄ = r (*) LR iff b₄ = ZeroLC R ) ) );