let K be Field; :: thesis:
let n, i be Nat; :: thesis:
assume AS: i in Seg n ; :: thesis:
XP1: addLoopStr(# the carrier of (n -VectSp_over K), the addF of (n -VectSp_over K), the ZeroF of (n -VectSp_over K) #) = n -Group_over K by PRVECT_1:def 5;
XP2: n -Group_over K = addLoopStr(# (n -tuples_on the carrier of K),(product ( the addF of K,n)),(n |-> (0. K)) #) by PRVECT_1:def 3;
defpred S₁[ Nat] means for s being FinSequence of (n -VectSp_over K) st len s = $1 holds
ex si being FinSequence of K st
( len si = len s & (Sum s) . i = Sum si & ( for k being Nat st k in dom si holds
si . k = (s /. k) . i ) );
P1: S₁[ 0 ]

proof

let s be FinSequence of (n -VectSp_over K); :: thesis:
assume AS1: len s = 0 ; :: thesis:
P1: s = <*> the carrier of (n -VectSp_over K) by AS1;
set si = <*> the carrier of K;
take <*> the carrier of K ; :: thesis:
thus len (<*> the carrier of K) = len s by AS1; :: thesis:
(0. (n -VectSp_over K)) . i = 0. K by XP1, XP2, FUNCOP_1:7, AS;
hence (Sum s) . i = 0. K by P1, RLVECT_1:43
.= Sum (<*> the carrier of K) by RLVECT_1:43 ;
:: thesis:
thus for k being Nat st k in dom (<*> the carrier of K) holds
(<*> the carrier of K) . k = (s /. k) . i ; :: thesis:

end;

P2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume AS1: S₁[k] ; :: thesis:
let s be FinSequence of (n -VectSp_over K); :: thesis:
assume AS2: len s = k + 1 ; :: thesis:
reconsider s0 = s | k as FinSequence of the carrier of (n -VectSp_over K) ;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A70: k + 1 in dom s by AS2, FINSEQ_1:def 3;
then s . (k + 1) in rng s by FUNCT_1:3;
then reconsider sk1 = s . (k + 1) as Element of the carrier of (n -VectSp_over K) ;
P1: len s0 = k by FINSEQ_1:59, AS2, NAT_1:11;
then P4: dom s0 = Seg k by FINSEQ_1:def 3;
A9: len s = (len s0) + 1 by AS2, FINSEQ_1:59, NAT_1:11;
s0 = s | (dom s0) by P1, FINSEQ_1:def 3;
then P3: Sum s = (Sum s0) + sk1 by AS2, A9, RLVECT_1:38;
consider si0 being FinSequence of K such that
P1F: ( len si0 = len s0 & (Sum s0) . i = Sum si0 & ( for k being Nat st k in dom si0 holds
si0 . k = (s0 /. k) . i ) ) by P1, AS1;
s /. (k + 1) in the carrier of (n -VectSp_over K) ;
then s /. (k + 1) in n -tuples_on the carrier of K by MATRIX13:102;
then consider ss being Element of the carrier of K * such that
XP4: ( s /. (k + 1) = ss & len ss = n ) ;
XP5: dom ss = Seg n by XP4, FINSEQ_1:def 3;
reconsider ss = ss as FinSequence of the carrier of K ;
ss . i in rng ss by XP5, AS, FUNCT_1:3;
then reconsider si0k1 = (s /. (k + 1)) . i as Element of K by XP4;
P2F: sk1 . i = si0k1 by A70, PARTFUN1:def 6;
reconsider si = si0 ^ <*si0k1*> as FinSequence of K ;
Y0: Sum si = (Sum si0) + (Sum <*si0k1*>) by RLVECT_1:41
.= (Sum si0) + si0k1 by RLVECT_1:44 ;
Y1: len si = (len si0) + (len <*si0k1*>) by FINSEQ_1:22
.= (len si0) + 1 by FINSEQ_1:39
.= len s by AS2, P1F, FINSEQ_1:59, NAT_1:11 ;
for j being Nat st j in dom si holds
si . j = (s /. j) . i

proof

let j be Nat; :: thesis:
assume j in dom si ; :: thesis:
then A2: ( 1 <= j & j <= k + 1 ) by Y1, AS2, FINSEQ_3:25;

per cases ;

suppose j <= k ; :: thesis:

then Q50: j in Seg k by A2;
then Q5: j in dom si0 by P1, P1F, FINSEQ_1:def 3;
hence si . j = si0 . j by FINSEQ_1:def 7
.= (s0 /. j) . i by P1F, Q5
.= (s /. j) . i by P4, Q50, PARTFUN1:80 ;
:: thesis:

end;

suppose j > k ; :: thesis:

then k + 1 <= j by NAT_1:13;
then j = k + 1 by A2, XXREAL_0:1;
hence si . j = (s /. j) . i by P1, P1F, FINSEQ_1:42; :: thesis:

end;

hence ex si being FinSequence of K st
( len si = len s & (Sum s) . i = Sum si & ( for k being Nat st k in dom si holds
si . k = (s /. k) . i ) ) by Y1, P3, P1F, P2F, AS, Y0, LMThGM25; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(P1, P2);
hence for s being FinSequence of (n -VectSp_over K) ex si being FinSequence of K st
( len si = len s & (Sum s) . i = Sum si & ( for k being Nat st k in dom si holds
si . k = (s /. k) . i ) ) ; :: thesis: