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_{1}( 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_{1}(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)

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;

Carrier (r (*) LR) c= rng (f * F)

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

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

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

then A15:
f * F is one-to-one
by FUNCT_1:def 4;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;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

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

then A23:
LR * F = (r (*) LR) * (f * F)
by A16, A17, A18;((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;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

Carrier (r (*) LR) c= rng (f * F)

proof

hence
sum LR = sum (r (*) LR)
by A4, A15, A23, Th30; :: thesis: verum
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;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