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 :: thesis: for v being Element of R holds (r (*) (s (*) LR)) . v = ((r * s) (*) LR) . v
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 7
.= LR . (((r * s) ") * v) by XCMPLX_1:204
.= ((r * s) (*) LR) . v by A2, Def2 ; :: thesis: verum
end;
hence r (*) (s (*) LR) = (r * s) (*) LR ; :: thesis: verum
end;
end;