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 A1: i in Seg (len f) ; :: thesis: 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)

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:13
.= (Seg (len f)) \/ {i} by FUNCOP_1:13 ;
hence dom (((Seg (len f)) --> 0) +* ({i} --> 1)) = Seg (len f) by A1, ZFMISC_1:40; :: thesis: verum

end;

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

proof

A4: (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) = {0} \/ (rng ({i} --> 1)) by A1, FUNCOP_1:8
.= {0} \/ {1} by FUNCOP_1:8 ;
0 in INT by INT_1:def 1;
then A5: {0} c= INT by ZFMISC_1:31;
1 in INT by INT_1:def 1;
then A6: {1} c= INT by ZFMISC_1:31;
A7: {0} \/ {1} c= INT by A5, A6, XBOOLE_1:8;
rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) by FUNCT_4:17;
hence rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT by A4, A7, XBOOLE_1:1; :: thesis: verum

end;

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 len f -element integer-valued FinSequence by CARD_1:def 7;
defpred S₁[ Nat, set ] means $2 = (s . $1) * (f /. $1);
A8: 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
A9: ( 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(A8);
A10: len w = len f by A9, FINSEQ_1:def 3;
then reconsider w = w as len f -element FinSequence of RS by CARD_1:def 7;

now

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

end;

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

proof

consider w1 being Function such that
A14: w1 = (Seg (len f)) --> (0. RS) ;
A15: dom w1 = Seg (len f) by A14, FUNCOP_1:13;
consider w2 being Function such that
A16: w2 = {i} --> (f /. i) ;
A17: dom w2 = {i} by A16, FUNCOP_1:13;
consider ww being Function such that
A18: ww = w1 +* w2 ;
A19: dom ww = (Seg (len f)) \/ {i} by A15, A17, A18, 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 A14, FUNCOP_1:13;
then A20: rng w1 c= the carrier of RS by XBOOLE_1:1;
rng w2 c= {(f /. i)} by A16, FUNCOP_1:13;
then A21: rng w2 c= the carrier of RS by XBOOLE_1:1;
A22: rng ww c= (rng w1) \/ (rng w2) by A18, FUNCT_4:17;
(rng w1) \/ (rng w2) c= the carrier of RS by A20, A21, XBOOLE_1:8;
then rng ww c= the carrier of RS by A22, 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 A23: j in dom w ; :: thesis: w /. j = ww /. j
A24: dom ({i} --> 1) = {i} by FUNCOP_1:13;

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

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

then A26: j = i by A17, TARSKI:def 1;
then w /. j = w . i by A23, PARTFUN1:def 6;
then A27: w /. j = (s . i) * (f /. i) by A9, A23, A26;
A28: i in {i} by TARSKI:def 1;
then A29: s . i = ({i} --> 1) . i by A24, FUNCT_4:13
.= 1 by A28, FUNCOP_1:7 ;
ww /. j = ww . j by A9, A19, A23, PARTFUN1:def 6
.= w2 . j by A18, A25, FUNCT_4:13
.= f /. i by A16, A17, A25, FUNCOP_1:7 ;
hence w /. j = ww /. j by A27, A29, RLVECT_1:def 8; :: thesis: verum

end;

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

w /. j = w . j by A23, PARTFUN1:def 6;
then A31: w /. j = (s . j) * (f /. j) by A9, A23;
not j in dom ({i} --> 1) by A17, A30;
then A32: s . j = ((Seg (len f)) --> 0) . j by FUNCT_4:11
.= 0 by A9, A23, FUNCOP_1:7 ;
ww /. j = ww . j by A9, A19, A23, PARTFUN1:def 6
.= w1 . j by A18, A30, FUNCT_4:11
.= 0. RS by A9, A14, A23, FUNCOP_1:7 ;
hence w /. j = ww /. j by A31, A32, RLVECT_1:10; :: thesis: verum

end;

end;

end;

hence w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) by A9, A10, A14, A16, A18, A19, FINSEQ_5:12; :: thesis: verum

end;

i in Seg (len w) by A9, A1, FINSEQ_1:def 3;
hence f /. i in Z_Lin f by A12, A13, Th29; :: thesis: verum