let GF be Ring; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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

proof

assume rng G meets rng p ; :: thesis: contradiction
then ex x being object st
( x in Carrier L & x in C \ (Carrier L) ) by A3, A5, XBOOLE_0:3;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

A8: len p = len (L (#) p) by VECTSP_6:def 5;

now :: thesis: for k being Nat st k in dom p holds
(L (#) p) . k = (0. GF) * (p /. k)

let k be Nat; :: thesis: ( k in dom p implies (L (#) p) . k = (0. GF) * (p /. k) )
assume A9: k in dom p ; :: thesis: (L (#) p) . k = (0. GF) * (p /. k)
then p /. k = p . k by PARTFUN1:def 6;
then p /. k in C \ (Carrier L) by A5, A9, FUNCT_1:def 3;
then A10: not p /. k in Carrier L by XBOOLE_0:def 5;
k in dom (L (#) p) by A8, A9, FINSEQ_3:29;
then (L (#) p) . k = (L . (p /. k)) * (p /. k) by VECTSP_6:def 5;
hence (L (#) p) . k = (0. GF) * (p /. k) by A10; :: thesis: verum

end;

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 ; :: thesis: ( 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; :: thesis: verum