let R be Ring; :: thesis: for V being LeftMod of R
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 the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
let V be LeftMod of R; :: 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 the carrier 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 the carrier 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 the carrier 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 the carrier of V st
( F is one-to-one & rng F = C & Sum L = Sum (L (#) F) )
consider G being FinSequence of the carrier 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 9;
set D = C \ (Carrier L);
consider p being FinSequence such that
A5: rng p = C \ (Carrier L) and
A6: p is one-to-one by FINSEQ_4:73;
reconsider p = p as FinSequence of the carrier of V by A5, FINSEQ_1:def 4;
A7: len p = len (L (#) p) by VECTSP_6:def 8;

now

let k be Element of NAT ; :: thesis: ( k in dom p implies (L (#) p) . k = (0. R) * (p /. k) )
assume A8: k in dom p ; :: thesis: (L (#) p) . k = (0. R) * (p /. k)
then k in dom (L (#) p) by A7, FINSEQ_3:31;
then A9: (L (#) p) . k = (L . (p /. k)) * (p /. k) by VECTSP_6:def 8;
p /. k = p . k by A8, PARTFUN1:def 8;
then p /. k in C \ (Carrier L) by A5, A8, FUNCT_1:def 5;
then not p /. k in Carrier L by XBOOLE_0:def 5;
hence (L (#) p) . k = (0. R) * (p /. k) by A9; :: thesis: verum

end;

then A10: Sum (L (#) p) = (0. R) * (Sum p) by A7, VECTSP_3:10
.= 0. V by VECTSP_1:59 ;
set F = G ^ p;
A11: Sum (L (#) (G ^ p)) = Sum ((L (#) G) ^ (L (#) p)) by VECTSP_6:37
.= (Sum (L (#) G)) + (0. V) by A10, RLVECT_1:58
.= Sum L by A4, RLVECT_1:def 7 ;
A12: rng G misses rng p

proof

assume rng G meets rng p ; :: thesis: contradiction
then consider x being set such that
A13: ( x in Carrier L & x in C \ (Carrier L) ) by A3, A5, XBOOLE_0:3;
thus contradiction by A13, XBOOLE_0:def 5; :: thesis: verum

end;

A14: rng (G ^ p) = (Carrier L) \/ (C \ (Carrier L)) by A3, A5, FINSEQ_1:44
.= C by A1, XBOOLE_1:45 ;
take G ^ p ; :: thesis: ( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) )
thus ( G ^ p is one-to-one & rng (G ^ p) = C & Sum L = Sum (L (#) (G ^ p)) ) by A2, A6, A11, A12, A14, FINSEQ_3:98; :: thesis: verum