let V be RealLinearSpace; :: thesis: for L being Linear_Combination of V
for A being Subset of V
for F being FinSequence of the carrier 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 the carrier 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 the carrier 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 S1[ Nat] means for F being FinSequence of the carrier 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
let F be FinSequence of the carrier 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 ;
reconsider G = G, x9 = <*x*> as FinSequence of the carrier of V by ;
A6: rng (G ^ <*x*>) = (rng G) \/ () by FINSEQ_1:31
.= (rng G) \/ {x} by FINSEQ_1:38 ;
then A7: rng G c= rng F by ;
{x} c= rng F by ;
then {x} c= the carrier of (Lin A) by A3;
then ( x in {x} implies x in the carrier of (Lin A) ) ;
then A8: x in Lin A by ;
then consider LA1 being Linear_Combination of A such that
A9: x = Sum LA1 by RLVECT_3:14;
x in V by ;
then reconsider x = x as VECTOR of V by STRUCT_0:def 5;
len (G ^ <*x*>) = (len G) + () 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 RLVECT_2:44;
then A11: LA2 + ((L . x) * LA1) is Linear_Combination of A by RLVECT_2:38;
Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by
.= (Sum LA2) + (Sum (L (#) x9)) by
.= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26
.= (Sum LA2) + ((L . x) * (Sum LA1)) by
.= (Sum LA2) + (Sum ((L . x) * LA1)) by RLVECT_3:2
.= Sum (LA2 + ((L . x) * LA1)) by RLVECT_3:1 ;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A11; :: thesis: verum
end;
let F be FinSequence of the carrier 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: S1[ 0 ]
proof
let F be FinSequence of the carrier 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 RLVECT_2:25;
then A16: Sum (L (#) F) = 0. V by RLVECT_1:43
.= Sum () by RLVECT_2:30 ;
ZeroLC V is Linear_Combination of A by RLVECT_2:22;
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A16; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A14, A1);
hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by ; :: thesis: verum