let GF be Ring; for V being LeftMod of GF
for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let V be LeftMod of GF; for L being Linear_Combination of V
for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let L be Linear_Combination of V; for C being finite Subset of V st Carrier L c= C holds
ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let C be finite Subset of V; ( Carrier L c= C implies ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) ) )
assume A1:
Carrier L c= C
; ex F being FinSequence of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
set D = C \ (Carrier L);
consider G being FinSequence of V such that
A2:
G is one-to-one
and
A3:
rng G = Carrier L
and
A4:
Sum L = Sum (L (#) G)
by VECTSP_6:def 6;
consider p being FinSequence such that
A5:
rng p = C \ (Carrier L)
and
A6:
p is one-to-one
by FINSEQ_4:58;
reconsider p = p as FinSequence of the carrier of V by A5, FINSEQ_1:def 4;
A7:
rng G misses rng p
A8:
len p = len (L (#) p)
by VECTSP_6:def 5;
then A11: Sum (L (#) p) =
(0. GF) * (Sum p)
by A8, RLVECT_2:67
.=
0. V
by VECTSP_1:14
;
set F = G ^ p;
take
G ^ p
; ( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) )
A12: Sum (L (#) (G ^ p)) =
Sum ((L (#) G) ^ (L (#) p))
by VECTSP_6:13
.=
(Sum (L (#) G)) + (0. V)
by A11, RLVECT_1:41
.=
Sum L
by A4, RLVECT_1:def 4
;
rng (G ^ p) =
(Carrier L) \/ (C \ (Carrier L))
by A3, A5, FINSEQ_1:31
.=
C
by A1, XBOOLE_1:45
;
hence
( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) )
by A2, A6, A12, A7, FINSEQ_3:91; verum