let V be Z_Module; :: thesis: for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let L be Linear_Combination of V; :: thesis: for A being Subset of V
for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
let A be Subset of V; :: thesis: for F being FinSequence of V st rng F c= the carrier of (Lin A) holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
defpred S₁[ Nat] means for F being FinSequence of V st rng F c= the carrier of (Lin A) & len F = $1 holds
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
let F be FinSequence of V; :: thesis: ( rng F c= the carrier of (Lin A) & len F = n + 1 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
A3: rng F c= the carrier of (Lin A) and
A4: len F = n + 1 ; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
consider G being FinSequence, x being object such that
A5: F = G ^ <*x*> by A4, FINSEQ_2:18;
reconsider G = G, x9 = <*x*> as FinSequence of V by A5, FINSEQ_1:36;
A6: rng (G ^ <*x*>) = (rng G) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng G) \/ {x} by FINSEQ_1:38 ;
then A7: rng G c= rng F by A5, XBOOLE_1:7;
{x} c= rng F by A5, A6, XBOOLE_1:7;
then {x} c= the carrier of (Lin A) by A3;
then A8: ( x in {x} implies x in the carrier of (Lin A) ) ;
then consider LA1 being Linear_Combination of A such that
A9: x = Sum LA1 by STRUCT_0:def 5, TARSKI:def 1, ZMODUL02:64;
x in V by A8, STRUCT_0:def 5, TARSKI:def 1, ZMODUL01:24;
then reconsider x = x as Vector of V ;
len (G ^ <*x*>) = (len G) + (len <*x*>) by FINSEQ_1:22
.= (len G) + 1 by FINSEQ_1:39 ;
then consider LA2 being Linear_Combination of A such that
A10: Sum (L (#) G) = Sum LA2 by A2, A3, A4, A5, A7, XBOOLE_1:1;
(L . x) * LA1 is Linear_Combination of A by ZMODUL02:31;
then A11: LA2 + ((L . x) * LA1) is Linear_Combination of A by ZMODUL02:27;
Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A5, ZMODUL02:51
.= (Sum LA2) + (Sum (L (#) x9)) by A10, RLVECT_1:41
.= (Sum LA2) + (Sum <*((L . x) * x)*>) by ZMODUL02:15
.= (Sum LA2) + ((L . x) * (Sum LA1)) by A9, RLVECT_1:44
.= (Sum LA2) + (Sum ((L . x) * LA1)) by ZMODUL02:53
.= Sum (LA2 + ((L . x) * LA1)) by ZMODUL02:52 ;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A11; :: thesis: verum

end;

let F be FinSequence of V; :: thesis: ( rng F c= the carrier of (Lin A) implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume A12: rng F c= the carrier of (Lin A) ; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A13: len F is Element of NAT ;
A14: S₁[ 0 ]

proof

let F be FinSequence of V; :: thesis: ( rng F c= the carrier of (Lin A) & len F = 0 implies ex K being Linear_Combination of A st Sum (L (#) F) = Sum K )
assume that
rng F c= the carrier of (Lin A) and
A15: len F = 0 ; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
F = <*> the carrier of V by A15;
then L (#) F = <*> the carrier of V by ZMODUL02:14;
then A16: Sum (L (#) F) = 0. V by RLVECT_1:43
.= Sum (ZeroLC V) by ZMODUL02:19 ;
ZeroLC V is Linear_Combination of A by ZMODUL02:11;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A14, A1);
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A12, A13; :: thesis: verum