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 ;
rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT
proof
A4: rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) by FUNCT_4:17;
Seg (len f) <> {} by A1;
then A5: ( rng ((Seg (len f)) --> 0) = {0} & rng ({i} --> 1) = {1} ) by FUNCOP_1:8;
( 1 in INT & 0 in INT ) by INT_1:def 2;
then ( rng ((Seg (len f)) --> 0) c= INT & rng ({i} --> 1) c= INT ) by A5, ZFMISC_1:31;
then (rng ((Seg (len f)) --> 0)) \/ (rng ({i} --> 1)) c= INT by XBOOLE_1:8;
hence rng (((Seg (len f)) --> 0) +* ({i} --> 1)) c= INT by A4; :: 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 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;
now :: thesis: for i being Nat st i in Seg (len f) holds
w /. i = (s . i) * (f /. i)
let i be Nat; :: thesis: ( i in Seg (len f) implies w /. i = (s . i) * (f /. i) )
assume A9: i in Seg (len f) ; :: thesis: w /. i = (s . i) * (f /. i)
hence w /. i = w . i by A7, PARTFUN1:def 6
.= (s . i) * (f /. i) by A7, A9 ;
:: thesis: verum
end;
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; :: thesis: ( j in dom w implies w /. j = ww /. j )
assume A21: j in dom w ; :: thesis: 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 ; :: thesis: w /. j = ww /. j
then 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; :: thesis: verum
end;
suppose A28: not j in dom w2 ; :: thesis: 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; :: thesis: verum
end;
end;
end;
hence w = ((Seg (len w)) --> (0. RS)) +* ({i} --> (f /. i)) by A7, A8, A12, A14, A16, A17, FINSEQ_5:12; :: thesis: 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; :: thesis: verum