let RS be RealLinearSpace; for f being FinSequence of RS
for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
let f be FinSequence of RS; for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
let i be Nat; ( i in Seg (len f) implies f /. i in Z_Lin f )
assume A1:
i in Seg (len f)
; f /. i in Z_Lin f
set s = ((Seg (len f)) --> 0) +* ({i} --> 1);
A2:
dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f)
then A3:
((Seg (len f)) --> 0) +* ({i} --> 1) is FinSequence-like
;
rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT
then reconsider s = ((Seg (len f)) --> 0) +* ({i} --> 1) as FinSequence of INT by A3, FINSEQ_1:def 4;
len s = len f
by A2, FINSEQ_1:def 3;
then reconsider s = s as INT -valued len f -element FinSequence by CARD_1:def 7;
defpred S1[ Nat, set ] means $2 = (s . $1) * (f /. $1);
A6:
for k being Nat st k in Seg (len f) holds
ex x being Element of RS st S1[k,x]
;
consider w being FinSequence of RS such that
A7:
( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S1[i,w . i] ) )
from FINSEQ_1:sch 5(A6);
A8:
len w = len f
by A7, FINSEQ_1:def 3;
then reconsider w = w as len f -element FinSequence of RS by CARD_1:def 7;
then A10:
Sum w in Z_Lin f
;
A11:
w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i))
proof
consider w1 being
Function such that A12:
w1 = (Seg (len f)) --> (0. RS)
;
A13:
dom w1 = Seg (len f)
by A12, FUNCOP_1:13;
consider w2 being
Function such that A14:
w2 = {i} --> (f /. i)
;
A15:
dom w2 = {i}
by A14, FUNCOP_1:13;
consider ww being
Function such that A16:
ww = w1 +* w2
;
A17:
dom ww =
(Seg (len f)) \/ {i}
by A13, A15, A16, FUNCT_4:def 1
.=
Seg (len f)
by A1, ZFMISC_1:40
;
then reconsider ww =
ww as
FinSequence by FINSEQ_1:def 2;
rng w1 c= {(0. RS)}
by A12, FUNCOP_1:13;
then A18:
rng w1 c= the
carrier of
RS
by XBOOLE_1:1;
rng w2 c= {(f /. i)}
by A14, FUNCOP_1:13;
then A19:
rng w2 c= the
carrier of
RS
by XBOOLE_1:1;
A20:
rng ww c= (rng w1) \/ (rng w2)
by A16, FUNCT_4:17;
(rng w1) \/ (rng w2) c= the
carrier of
RS
by A18, A19, XBOOLE_1:8;
then
rng ww c= the
carrier of
RS
by A20;
then reconsider ww =
ww as
FinSequence of
RS by FINSEQ_1:def 4;
for
j being
Nat st
j in dom w holds
w /. j = ww /. j
proof
let j be
Nat;
( j in dom w implies w /. j = ww /. j )
assume A21:
j in dom w
;
w /. j = ww /. j
A22:
dom ({i} --> 1) = {i}
by FUNCOP_1:13;
per cases
( j in dom w2 or not j in dom w2 )
;
suppose A23:
j in dom w2
;
w /. j = ww /. jthen A24:
j = i
by A15, TARSKI:def 1;
then
w /. j = w . i
by A21, PARTFUN1:def 6;
then A25:
w /. j = (s . i) * (f /. i)
by A7, A21, A24;
A26:
i in {i}
by TARSKI:def 1;
then A27:
s . i =
({i} --> 1) . i
by A22, FUNCT_4:13
.=
1
by A26, FUNCOP_1:7
;
ww /. j =
ww . j
by A7, A17, A21, PARTFUN1:def 6
.=
w2 . j
by A16, A23, FUNCT_4:13
.=
f /. i
by A14, A15, A23, FUNCOP_1:7
;
hence
w /. j = ww /. j
by A25, A27, RLVECT_1:def 8;
verum end; suppose A28:
not
j in dom w2
;
w /. j = ww /. j
w /. j = w . j
by A21, PARTFUN1:def 6;
then A29:
w /. j = (s . j) * (f /. j)
by A7, A21;
not
j in dom ({i} --> 1)
by A15, A28;
then A30:
s . j =
((Seg (len f)) --> 0) . j
by FUNCT_4:11
.=
0
by A7, A21, FUNCOP_1:7
;
ww /. j =
ww . j
by A7, A17, A21, PARTFUN1:def 6
.=
w1 . j
by A16, A28, FUNCT_4:11
.=
0. RS
by A7, A12, A21, FUNCOP_1:7
;
hence
w /. j = ww /. j
by A29, A30, RLVECT_1:10;
verum end; end;
end;
hence
w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i))
by A7, A8, A12, A14, A16, A17, FINSEQ_5:12;
verum
end;
i in Seg (len w)
by A7, A1, FINSEQ_1:def 3;
hence
f /. i in Z_Lin f
by A10, A11, Th29; verum