let V be RealUnitarySpace; 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;
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 A1:
rng F c= the carrier of (Lin A)
; ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
A2:
len F is Nat
;
A3:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
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 A5:
rng F c= the
carrier of
(Lin A)
and A6:
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 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;
verum
end;
A15:
S1[ 0 ]
for n being Nat holds S1[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; verum