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