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
sum LR = sum (r (*) 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
sum LR = sum (r (*) LR)
let LR be Linear_Combination of R; :: thesis: ( r <> 0 implies sum LR = sum (r (*) LR) )
set rL = r (*) LR;
deffunc H₁( Element of R) -> Element of the carrier of R = r * $1;
consider f being Function of the carrier of R, the carrier of R such that
A1: for v being Element of R holds f . v = H₁(v) from FUNCT_2:sch 4();
consider F being FinSequence of R such that
A2: F is one-to-one and
A3: rng F = Carrier LR and
A4: sum LR = Sum (LR * F) by Def3;
assume A5: r <> 0 ; :: thesis: sum LR = sum (r (*) LR)

now :: thesis: for x1, x2 being object st x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in dom (f * F) & x2 in dom (f * F) & (f * F) . x1 = (f * F) . x2 implies x1 = x2 )
assume that
A6: x1 in dom (f * F) and
A7: x2 in dom (f * F) and
A8: (f * F) . x1 = (f * F) . x2 ; :: thesis: x1 = x2
A9: f . (F /. x1) = r * (F /. x1) by A1;
A10: x1 in dom F by A6, FUNCT_1:11;
then A11: F . x1 = F /. x1 by PARTFUN1:def 6;
A12: x2 in dom F by A7, FUNCT_1:11;
then A13: F . x2 = F /. x2 by PARTFUN1:def 6;
( (f * F) . x1 = f . (F . x1) & (f * F) . x2 = f . (F . x2) ) by A6, A7, FUNCT_1:12;
then A14: r * (F /. x1) = r * (F /. x2) by A1, A8, A9, A11, A13;
F /. x1 = 1 * (F /. x1) by RLVECT_1:def 8
.= ((r ") * r) * (F /. x1) by A5, XCMPLX_0:def 7
.= (r ") * (r * (F /. x2)) by A14, RLVECT_1:def 7
.= ((r ") * r) * (F /. x2) by RLVECT_1:def 7
.= 1 * (F /. x2) by A5, XCMPLX_0:def 7
.= F /. x2 by RLVECT_1:def 8 ;
hence x1 = x2 by A2, A10, A11, A12, A13, FUNCT_1:def 4; :: thesis: verum

end;

then A15: f * F is one-to-one by FUNCT_1:def 4;
A16: len (LR * F) = len F by FINSEQ_2:33;
A17: len (f * F) = len F by FINSEQ_2:33;
A18: len ((r (*) LR) * (f * F)) = len (f * F) by FINSEQ_2:33;

now :: thesis: for k being Nat st 1 <= k & k <= len F holds
((r (*) LR) * (f * F)) . k = (LR * F) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len F implies ((r (*) LR) * (f * F)) . k = (LR * F) . k )
assume A19: ( 1 <= k & k <= len F ) ; :: thesis: ((r (*) LR) * (f * F)) . k = (LR * F) . k
then k in dom F by FINSEQ_3:25;
then A20: F /. k = F . k by PARTFUN1:def 6;
k in dom (LR * F) by A16, A19, FINSEQ_3:25;
then A21: (LR * F) . k = LR . (F . k) by FUNCT_1:12;
k in dom (f * F) by A17, A19, FINSEQ_3:25;
then A22: (f * F) . k = f . (F . k) by FUNCT_1:12;
k in dom ((r (*) LR) * (f * F)) by A17, A18, A19, FINSEQ_3:25;
then ((r (*) LR) * (f * F)) . k = (r (*) LR) . ((f * F) . k) by FUNCT_1:12;
hence ((r (*) LR) * (f * F)) . k = (r (*) LR) . (r * (F /. k)) by A1, A20, A22
.= LR . ((r ") * (r * (F /. k))) by A5, Def2
.= LR . (((r ") * r) * (F /. k)) by RLVECT_1:def 7
.= LR . (1 * (F /. k)) by A5, XCMPLX_0:def 7
.= (LR * F) . k by A20, A21, RLVECT_1:def 8 ;
:: thesis: verum

end;

then A23: LR * F = (r (*) LR) * (f * F) by A16, A17, A18;
Carrier (r (*) LR) c= rng (f * F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Carrier (r (*) LR) or x in rng (f * F) )
assume x in Carrier (r (*) LR) ; :: thesis: x in rng (f * F)
then x in r * (Carrier LR) by A5, Th23;
then consider v being Element of R such that
A24: x = r * v and
A25: v in Carrier LR ;
consider y being object such that
A26: y in dom F and
A27: F . y = v by A3, A25, FUNCT_1:def 3;
A28: f . v = x by A1, A24;
A29: dom F = dom (f * F) by A17, FINSEQ_3:29;
then (f * F) . y = f . v by A26, A27, FUNCT_1:12;
hence x in rng (f * F) by A26, A28, A29, FUNCT_1:def 3; :: thesis: verum

end;

hence sum LR = sum (r (*) LR) by A4, A15, A23, Th30; :: thesis: verum