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

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 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 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;assume A2: S

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

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 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;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

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