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 S_{1}[ 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 S_{1}[n] holds

S_{1}[n + 1]

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_{1}[ 0 ]
_{1}[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

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 S

ex K being Linear_Combination of A st Sum (L (#) F) = Sum K;

A1: for n being Nat st S

S

proof

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 )
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[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 A4, FINSEQ_2:18;

reconsider G = G, x9 = <*x*> as FinSequence of the carrier 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 ( x in {x} implies x in the carrier of (Lin A) ) ;

then A8: x in Lin A by STRUCT_0:def 5, TARSKI:def 1;

then consider LA1 being Linear_Combination of A such that

A9: x = Sum LA1 by RLVECT_3:14;

x in V by A8, RLSUB_1:9;

then reconsider x = x as VECTOR of V by 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

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 A5, RLVECT_3:34

.= (Sum LA2) + (Sum (L (#) x9)) by A10, RLVECT_1:41

.= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26

.= (Sum LA2) + ((L . x) * (Sum LA1)) by A9, 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 A11; :: thesis: verum

end;assume A2: S

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 A4, FINSEQ_2:18;

reconsider G = G, x9 = <*x*> as FinSequence of the carrier 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 ( x in {x} implies x in the carrier of (Lin A) ) ;

then A8: x in Lin A by STRUCT_0:def 5, TARSKI:def 1;

then consider LA1 being Linear_Combination of A such that

A9: x = Sum LA1 by RLVECT_3:14;

x in V by A8, RLSUB_1:9;

then reconsider x = x as VECTOR of V by 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

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 A5, RLVECT_3:34

.= (Sum LA2) + (Sum (L (#) x9)) by A10, RLVECT_1:41

.= (Sum LA2) + (Sum <*((L . x) * x)*>) by RLVECT_2:26

.= (Sum LA2) + ((L . x) * (Sum LA1)) by A9, 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 A11; :: thesis: verum

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

proof

for n being Nat holds S
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 (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 A16; :: thesis: verum

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

hence ex K being Linear_Combination of A st Sum (L (#) F) = Sum K by A12, A13; :: thesis: verum