let S be non empty addLoopStr ; :: thesis: for LS being Linear_Combination of S

for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds

sum LS = Sum (LS * F)

let LS be Linear_Combination of S; :: thesis: for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds

sum LS = Sum (LS * F)

let F be FinSequence of S; :: thesis: ( F is one-to-one & Carrier LS c= rng F implies sum LS = Sum (LS * F) )

assume that

A1: F is one-to-one and

A2: Carrier LS c= rng F ; :: thesis: sum LS = Sum (LS * F)

consider G being FinSequence of S such that

A3: G is one-to-one and

A4: rng G = Carrier LS and

A5: sum LS = Sum (LS * G) by Def3;

reconsider R = rng G as Subset of (rng F) by A2, A4;

reconsider FR = F - R, FR1 = F - (R `) as FinSequence of S by FINSEQ_3:86;

consider p being Permutation of (dom F) such that

A6: F * p = (F - (R `)) ^ (F - R) by FINSEQ_3:115;

(rng F) \ (R `) = (R `) `

.= R ;

then A7: rng FR1 = R by FINSEQ_3:65;

FR1 is one-to-one by A1, FINSEQ_3:87;

then FR1,G are_fiberwise_equipotent by A3, A7, RFINSEQ:26;

then consider q being Permutation of (dom G) such that

A8: FR1 = G * q by RFINSEQ:4;

len (LS * G) = len G by FINSEQ_2:33;

then A9: dom G = dom (LS * G) by FINSEQ_3:29;

(LS * G) * q = LS * FR1 by A8, RELAT_1:36;

then A10: sum LS = Sum (LS * FR1) by A5, A9, FINSOP_1:7;

len (LS * F) = len F by FINSEQ_2:33;

then A11: dom F = dom (LS * F) by FINSEQ_3:29;

(rng F) \ R = rng FR by FINSEQ_3:65;

then rng FR misses Carrier LS by A4, XBOOLE_1:79;

then A12: ( LS * (FR1 ^ FR) = (LS * FR1) ^ (LS * FR) & Sum (LS * FR) = 0 ) by Th29, FINSEQOP:9;

(LS * F) * p = LS * (FR1 ^ FR) by A6, RELAT_1:36;

hence Sum (LS * F) = Sum (LS * (FR1 ^ FR)) by A11, FINSOP_1:7

.= (sum LS) + 0 by A10, A12, RVSUM_1:75

.= sum LS ;

:: thesis: verum

for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds

sum LS = Sum (LS * F)

let LS be Linear_Combination of S; :: thesis: for F being FinSequence of S st F is one-to-one & Carrier LS c= rng F holds

sum LS = Sum (LS * F)

let F be FinSequence of S; :: thesis: ( F is one-to-one & Carrier LS c= rng F implies sum LS = Sum (LS * F) )

assume that

A1: F is one-to-one and

A2: Carrier LS c= rng F ; :: thesis: sum LS = Sum (LS * F)

consider G being FinSequence of S such that

A3: G is one-to-one and

A4: rng G = Carrier LS and

A5: sum LS = Sum (LS * G) by Def3;

reconsider R = rng G as Subset of (rng F) by A2, A4;

reconsider FR = F - R, FR1 = F - (R `) as FinSequence of S by FINSEQ_3:86;

consider p being Permutation of (dom F) such that

A6: F * p = (F - (R `)) ^ (F - R) by FINSEQ_3:115;

(rng F) \ (R `) = (R `) `

.= R ;

then A7: rng FR1 = R by FINSEQ_3:65;

FR1 is one-to-one by A1, FINSEQ_3:87;

then FR1,G are_fiberwise_equipotent by A3, A7, RFINSEQ:26;

then consider q being Permutation of (dom G) such that

A8: FR1 = G * q by RFINSEQ:4;

len (LS * G) = len G by FINSEQ_2:33;

then A9: dom G = dom (LS * G) by FINSEQ_3:29;

(LS * G) * q = LS * FR1 by A8, RELAT_1:36;

then A10: sum LS = Sum (LS * FR1) by A5, A9, FINSOP_1:7;

len (LS * F) = len F by FINSEQ_2:33;

then A11: dom F = dom (LS * F) by FINSEQ_3:29;

(rng F) \ R = rng FR by FINSEQ_3:65;

then rng FR misses Carrier LS by A4, XBOOLE_1:79;

then A12: ( LS * (FR1 ^ FR) = (LS * FR1) ^ (LS * FR) & Sum (LS * FR) = 0 ) by Th29, FINSEQOP:9;

(LS * F) * p = LS * (FR1 ^ FR) by A6, RELAT_1:36;

hence Sum (LS * F) = Sum (LS * (FR1 ^ FR)) by A11, FINSOP_1:7

.= (sum LS) + 0 by A10, A12, RVSUM_1:75

.= sum LS ;

:: thesis: verum