let V be RealUnitarySpace; :: 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;
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 A1: rng F c= the carrier of (Lin A) ; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A2: len F is Nat ;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: 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
A5: rng F c= the carrier of (Lin A) and
A6: 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
A7: F = G ^ <*x*> by A6, FINSEQ_2:18;
reconsider G = G, x9 = <*x*> as FinSequence of V by A7, FINSEQ_1:36;
A8: rng (G ^ <*x*>) = (rng G) \/ (rng <*x*>) by FINSEQ_1:31
.= (rng G) \/ {x} by FINSEQ_1:38 ;
then A9: rng G c= rng F by A7, XBOOLE_1:7;
{x} c= rng F by A7, A8, XBOOLE_1:7;
then {x} c= the carrier of (Lin A) by A5;
then ( x in {x} implies x in the carrier of (Lin A) ) ;
then A10: x in Lin A by STRUCT_0:def 5, TARSKI:def 1;
then A11: x in V by RUSUB_1:2;
consider LA1 being Linear_Combination of A such that
A12: x = Sum LA1 by A10, Th1;
reconsider x = x as VECTOR of V by A11, STRUCT_0:def 5;
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
A13: Sum (L (#) G) = Sum LA2 by A4, A5, A6, A7, A9, XBOOLE_1:1;
(L . x) * LA1 is Linear_Combination of A by RLVECT_2:44;
then A14: LA2 + ((L . x) * LA1) is Linear_Combination of A by RLVECT_2:38;
Sum (L (#) F) = Sum ((L (#) G) ^ (L (#) x9)) by A7, RLVECT_3:34
.= (Sum LA2) + (Sum (L (#) x9)) by A13, RLVECT_1:41
.= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26
.= (Sum LA2) + ((L . x) * (Sum LA1)) by A12, RLVECT_1:44
.= (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 A14; :: thesis: verum

end;

A15: 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
A16: len F = 0 ; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
F = <*> the carrier of V by A16;
then L (#) F = <*> the carrier of V by RLVECT_2:25;
then A17: Sum (L (#) F) = 0. V by RLVECT_1:43
.= Sum (ZeroLC V) 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 A17; :: thesis: verum

end;

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