let V be Z_Module; for F being FinSequence of V st F is one-to-one holds
for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
let F be FinSequence of V; ( F is one-to-one implies for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L )
assume A1:
F is one-to-one
; for L being Linear_Combination of V st Carrier L c= rng F holds
Sum (L (#) F) = Sum L
rng F c= rng F
;
then reconsider X = rng F as Subset of (rng F) ;
let L be Linear_Combination of V; ( Carrier L c= rng F implies Sum (L (#) F) = Sum L )
assume A2:
Carrier L c= rng F
; Sum (L (#) F) = Sum L
consider G being FinSequence of V such that
A3:
G is one-to-one
and
A4:
rng G = Carrier L
and
A5:
Sum L = Sum (L (#) G)
by VECTSP_6:def 6;
reconsider A = rng G as Subset of (rng F) by A2, A4;
set F1 = F - (A `);
X \ (A `) =
X /\ ((A `) `)
by SUBSET_1:13
.=
A
by XBOOLE_1:28
;
then A6:
rng (F - (A `)) = rng G
by FINSEQ_3:65;
F - (A `) is one-to-one
by A1, FINSEQ_3:87;
then A7:
ex Q being Permutation of (dom G) st F - (A `) = G * Q
by A3, A6, RFINSEQ:4, RFINSEQ:26;
reconsider F1 = F - (A `), F2 = F - A as FinSequence of V by FINSEQ_3:86;
A8: (rng F2) /\ (rng G) =
((rng F) \ (rng G)) /\ (rng G)
by FINSEQ_3:65
.=
{}
by XBOOLE_0:def 7, XBOOLE_1:79
;
ex P being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * P
by FINSEQ_3:115;
then Sum (L (#) F) =
Sum (L (#) (F1 ^ F2))
by Th5
.=
Sum ((L (#) F1) ^ (L (#) F2))
by ZMODUL02:51
.=
(Sum (L (#) F1)) + (Sum (L (#) F2))
by RLVECT_1:41
.=
(Sum (L (#) F1)) + (0. V)
by A4, A8, Th6, XBOOLE_0:def 7
.=
(Sum (L (#) G)) + (0. V)
by A7, Th5
.=
Sum L
by A5, RLVECT_1:4
;
hence
Sum (L (#) F) = Sum L
; verum