let r 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 Carrier (r (*) LR) c= r * (Carrier LR)
let R be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for LR being Linear_Combination of R holds Carrier (r (*) LR) c= r * (Carrier LR)
let LR be Linear_Combination of R; :: thesis: Carrier (r (*) LR) c= r * (Carrier LR)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (r (*) LR) or x in r * (Carrier LR) )
assume A1: x in Carrier (r (*) LR) ; :: thesis: x in r * (Carrier LR)
reconsider v = x as Element of R by A1;
A2: (r (*) LR) . v <> 0 by A1, RLVECT_2:19;
0 (*) LR = ZeroLC R by Def2;
then A3: r <> 0 by A1, RLVECT_2:def 5;
then (r (*) LR) . v = LR . ((r ") * v) by Def2;
then A4: (r ") * v in Carrier LR by A2;
r * ((r ") * v) = (r * (r ")) * v by RLVECT_1:def 7
.= 1 * v by A3, XCMPLX_0:def 7
.= v by RLVECT_1:def 8 ;
hence x in r * (Carrier LR) by A4; :: thesis: verum