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 S1[ Element of 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:
S1[ 0 ]
A3:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[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 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
set such that A7:
F = G ^ <*x*>
by A6, FINSEQ_2:21;
reconsider G =
G,
x' =
<*x*> as
FinSequence of the
carrier of
V by A7, FINSEQ_1:50;
rng (G ^ <*x*>) =
(rng G) \/ (rng <*x*>)
by FINSEQ_1:44
.=
(rng G) \/ {x}
by FINSEQ_1:55
;
then
(
rng G c= rng F &
{x} c= rng F )
by A7, XBOOLE_1:7;
then A8:
(
rng G c= the
carrier of
(Lin A) &
{x} c= the
carrier of
(Lin A) )
by A5, XBOOLE_1:1;
then
(
x in {x} implies
x in the
carrier of
(Lin A) )
;
then A9:
x in Lin A
by STRUCT_0:def 5, TARSKI:def 1;
then consider LA1 being
Linear_Combination of
A such that A10:
x = Sum LA1
by RLVECT_3:17;
x in V
by A9, RLSUB_1:17;
then reconsider x =
x as
VECTOR of
V by STRUCT_0:def 5;
len (G ^ <*x*>) =
(len G) + (len <*x*>)
by FINSEQ_1:35
.=
(len G) + 1
by FINSEQ_1:56
;
then consider LA2 being
Linear_Combination of
A such that A11:
Sum (L (#) G) = Sum LA2
by A4, A6, A7, A8;
A12:
Sum (L (#) F) =
Sum ((L (#) G) ^ (L (#) x'))
by A7, RLVECT_3:41
.=
(Sum LA2) + (Sum (L (#) x'))
by A11, RLVECT_1:58
.=
(Sum LA2) + (Sum <*((L . x) * x)*>)
by RLVECT_2:42
.=
(Sum LA2) + ((L . x) * (Sum LA1))
by A10, RLVECT_1:61
.=
(Sum LA2) + (Sum ((L . x) * LA1))
by RLVECT_3:2
.=
Sum (LA2 + ((L . x) * LA1))
by RLVECT_3:1
;
(L . x) * LA1 is
Linear_Combination of
A
by RLVECT_2:67;
then
LA2 + ((L . x) * LA1) is
Linear_Combination of
A
by RLVECT_2:59;
hence
ex
K being
Linear_Combination of
A st
Sum (L (#) F) = Sum K
by A12;
:: thesis: verum
end;
A13:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A3);
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 )
assume A14:
rng F c= the carrier of (Lin A)
; :: thesis: ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
len F is Element of NAT
;
hence
ex K being Linear_Combination of A st Sum (L (#) F) = Sum K
by A13, A14; :: thesis: verum