let r, s be Real; :: thesis: for R being non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct
for LR being Linear_Combination of R holds r (*) (s (*) LR) = (r * s) (*) LR
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for LR being Linear_Combination of R holds r (*) (s (*) LR) = (r * s) (*) LR
let LR be Linear_Combination of R; :: thesis: r (*) (s (*) LR) = (r * s) (*) LR

per cases ( r = 0 or s = 0 or ( r <> 0 & s <> 0 ) ) ;

suppose A1: ( r = 0 or s = 0 ) ; :: thesis: r (*) (s (*) LR) = (r * s) (*) LR

then (r * s) (*) LR = ZeroLC R by Def2;
hence r (*) (s (*) LR) = (r * s) (*) LR by A1, Def2, Th26; :: thesis: verum

end;

suppose A2: ( r <> 0 & s <> 0 ) ; :: thesis: r (*) (s (*) LR) = (r * s) (*) LR

now

let v be Element of R; :: thesis: (r (*) (s (*) LR)) . v = ((r * s) (*) LR) . v
thus (r (*) (s (*) LR)) . v = (s (*) LR) . ((r " ) * v) by A2, Def2
.= LR . ((s " ) * ((r " ) * v)) by A2, Def2
.= LR . (((s " ) * (r " )) * v) by RLVECT_1:def 10
.= LR . (((r * s) " ) * v) by XCMPLX_1:205
.= ((r * s) (*) LR) . v by A2, Def2 ; :: thesis: verum

end;

hence r (*) (s (*) LR) = (r * s) (*) LR by RLVECT_2:def 11; :: thesis: verum

end;

end;