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