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 st r <> 0 holds

Carrier (r (*) LR) = 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 st r <> 0 holds

Carrier (r (*) LR) = r * (Carrier LR)

let LR be Linear_Combination of R; :: thesis: ( r <> 0 implies Carrier (r (*) LR) = r * (Carrier LR) )

assume A1: r <> 0 ; :: thesis: Carrier (r (*) LR) = r * (Carrier LR)

thus Carrier (r (*) LR) c= r * (Carrier LR) by Th22; :: according to XBOOLE_0:def 10 :: thesis: r * (Carrier LR) c= Carrier (r (*) LR)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Carrier LR) or x in Carrier (r (*) LR) )

assume x in r * (Carrier LR) ; :: thesis: x in Carrier (r (*) LR)

then consider v being Element of R such that

A2: x = r * v and

A3: v in Carrier LR ;

(r ") * (r * v) = ((r ") * r) * v by RLVECT_1:def 7

.= 1 * v by A1, XCMPLX_0:def 7

.= v by RLVECT_1:def 8 ;

then A4: LR . v = (r (*) LR) . x by A1, A2, Def2;

LR . v <> 0 by A3, RLVECT_2:19;

hence x in Carrier (r (*) LR) by A2, A4; :: thesis: verum

for LR being Linear_Combination of R st r <> 0 holds

Carrier (r (*) LR) = 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 st r <> 0 holds

Carrier (r (*) LR) = r * (Carrier LR)

let LR be Linear_Combination of R; :: thesis: ( r <> 0 implies Carrier (r (*) LR) = r * (Carrier LR) )

assume A1: r <> 0 ; :: thesis: Carrier (r (*) LR) = r * (Carrier LR)

thus Carrier (r (*) LR) c= r * (Carrier LR) by Th22; :: according to XBOOLE_0:def 10 :: thesis: r * (Carrier LR) c= Carrier (r (*) LR)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in r * (Carrier LR) or x in Carrier (r (*) LR) )

assume x in r * (Carrier LR) ; :: thesis: x in Carrier (r (*) LR)

then consider v being Element of R such that

A2: x = r * v and

A3: v in Carrier LR ;

(r ") * (r * v) = ((r ") * r) * v by RLVECT_1:def 7

.= 1 * v by A1, XCMPLX_0:def 7

.= v by RLVECT_1:def 8 ;

then A4: LR . v = (r (*) LR) . x by A1, A2, Def2;

LR . v <> 0 by A3, RLVECT_2:19;

hence x in Carrier (r (*) LR) by A2, A4; :: thesis: verum