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

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