let RS be RealLinearSpace; :: thesis: 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; :: thesis: for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f
let i be Nat; :: thesis: ( i in Seg (len f) implies f /. i in Z_Lin f )
assume AS: i in Seg (len f) ; :: thesis: f /. i in Z_Lin f
set s = ((Seg (len f)) --> 0) +* ({i} --> 1);
P0: dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f)

proof

dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = (dom ((Seg (len f)) --> 0)) \/ (dom ({i} --> 1)) by FUNCT_4:def 1
.= (Seg (len f)) \/ (dom ({i} --> 1)) by FUNCOP_1:19
.= (Seg (len f)) \/ {i} by FUNCOP_1:19 ;
hence dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f) by ZFMISC_1:46, AS; :: thesis: verum

end;

then P1: ((Seg (len f)) --> 0) +* ({i} --> 1) is FinSequence-like by FINSEQ_1:def 2;
rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT

proof

A0: (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) = {0} \/ (rng ({i} --> 1)) by AS, FUNCOP_1:14
.= {0} \/ {1} by FUNCOP_1:14 ;
0 in INT by INT_1:def 1;
then A1: {0} c= INT by ZFMISC_1:37;
1 in INT by INT_1:def 1;
then A2: {1} c= INT by ZFMISC_1:37;
A3: {0} \/ {1} c= INT by A1, A2, XBOOLE_1:8;
rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) by FUNCT_4:18;
hence rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT by A0, A3, XBOOLE_1:1; :: thesis: verum

end;

then reconsider s = ((Seg (len f)) --> 0) +* ({i} --> 1) as FinSequence of INT by P1, FINSEQ_1:def 4;
len s = len f by P0, FINSEQ_1:def 3;
then reconsider s = s as len f -long integer-valued FinSequence by FINSEQ_1:def 18;
defpred S₁[ Nat, set ] means $2 = (s . $1) * (f /. $1);
P3: for k being Nat st k in Seg (len f) holds
ex x being Element of RS st S₁[k,x] ;
consider w being FinSequence of RS such that
P4: ( dom w = Seg (len f) & ( for i being Nat st i in Seg (len f) holds
S₁[i,w . i] ) ) from FINSEQ_1:sch 5(P3);
P5: len w = len f by P4, FINSEQ_1:def 3;
then reconsider w = w as len f -long FinSequence of RS by FINSEQ_1:def 18;

now

let i be Nat; :: thesis: ( i in Seg (len f) implies w /. i = (s . i) * (f /. i) )
assume A1: i in Seg (len f) ; :: thesis: w /. i = (s . i) * (f /. i)
hence w /. i = w . i by P4, PARTFUN1:def 8
.= (s . i) * (f /. i) by P4, A1 ;
:: thesis: verum

end;

then P6: Sum w in Z_Lin f ;
P7: w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i))

proof

consider w1 being Function such that
B0: w1 = (Seg (len f)) --> (0. RS) ;
B1: dom w1 = Seg (len f) by B0, FUNCOP_1:19;
consider w2 being Function such that
B2: w2 = {i} --> (f /. i) ;
B3: dom w2 = {i} by B2, FUNCOP_1:19;
consider ww being Function such that
B4: ww = w1 +* w2 ;
B5: dom ww = (Seg (len f)) \/ {i} by B1, B3, B4, FUNCT_4:def 1
.= Seg (len f) by AS, ZFMISC_1:46 ;
then reconsider ww = ww as FinSequence by FINSEQ_1:def 2;
rng w1 c= {(0. RS)} by B0, FUNCOP_1:19;
then B9: rng w1 c= the carrier of RS by XBOOLE_1:1;
rng w2 c= {(f /. i)} by B2, FUNCOP_1:19;
then B13: rng w2 c= the carrier of RS by XBOOLE_1:1;
B14: rng ww c= (rng w1) \/ (rng w2) by B4, FUNCT_4:18;
(rng w1) \/ (rng w2) c= the carrier of RS by B9, B13, XBOOLE_1:8;
then rng ww c= the carrier of RS by B14, XBOOLE_1:1;
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; :: thesis: ( j in dom w implies w /. j = ww /. j )
assume C0: j in dom w ; :: thesis: w /. j = ww /. j
C1: dom ({i} --> 1) = {i} by FUNCOP_1:19;

per cases ( j in dom w2 or not j in dom w2 ) ;

suppose C2: j in dom w2 ; :: thesis: w /. j = ww /. j

then C3: j = i by B3, TARSKI:def 1;
then w /. j = w . i by C0, PARTFUN1:def 8;
then C4: w /. j = (s . i) * (f /. i) by P4, C0, C3;
C5: i in {i} by TARSKI:def 1;
then C6: s . i = ({i} --> 1) . i by C1, FUNCT_4:14
.= 1 by C5, FUNCOP_1:13 ;
ww /. j = ww . j by P4, B5, C0, PARTFUN1:def 8
.= w2 . j by B4, C2, FUNCT_4:14
.= f /. i by B2, B3, C2, FUNCOP_1:13 ;
hence w /. j = ww /. j by C4, C6, RLVECT_1:def 11; :: thesis: verum

end;

suppose C7: not j in dom w2 ; :: thesis: w /. j = ww /. j

w /. j = w . j by C0, PARTFUN1:def 8;
then C9: w /. j = (s . j) * (f /. j) by P4, C0;
not j in dom ({i} --> 1) by B3, C7;
then C10: s . j = ((Seg (len f)) --> 0) . j by FUNCT_4:12
.= 0 by P4, C0, FUNCOP_1:13 ;
ww /. j = ww . j by P4, B5, C0, PARTFUN1:def 8
.= w1 . j by B4, C7, FUNCT_4:12
.= 0. RS by P4, B0, C0, FUNCOP_1:13 ;
hence w /. j = ww /. j by C9, C10, RLVECT_1:23; :: thesis: verum

end;

end;

end;

hence w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) by P4, P5, B0, B2, B4, B5, FINSEQ_5:13; :: thesis: verum

end;

i in Seg (len w) by P4, FINSEQ_1:def 3, AS;
hence f /. i in Z_Lin f by P6, P7, SLM0100; :: thesis: verum