let V be Z_Module; 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; 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; 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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
let F be
FinSequence of
V;
( 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
;
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;
verum
end;
let F be FinSequence of V; ( 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)
; ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A13:
len F is Element of NAT
;
A14:
S1[ 0 ]
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 A12, A13; verum