let K be Field; :: thesis: for n, i being Nat st i in Seg n holds
for s being FinSequence of () 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 ) )

let n, i be Nat; :: thesis: ( i in Seg n implies for s being FinSequence of () 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 ) ) )

assume AS: i in Seg n ; :: thesis: for s being FinSequence of () 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 ) )

XP1: addLoopStr(# the carrier of (), the addF of (), the ZeroF of () #) = 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 S1[ Nat] means for s being FinSequence of () 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: S1[ 0 ]
proof
let s be FinSequence of (); :: thesis: ( len s = 0 implies 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 ) ) )

assume AS1: len s = 0 ; :: thesis: 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 = <*> the carrier of () by AS1;
set si = <*> the carrier of K;
take <*> the carrier of K ; :: thesis: ( len (<*> the carrier of K) = len s & (Sum s) . i = Sum (<*> the carrier of K) & ( for k being Nat st k in dom (<*> the carrier of K) holds
(<*> the carrier of K) . k = (s /. k) . i ) )

thus len (<*> the carrier of K) = len s by AS1; :: thesis: ( (Sum s) . i = Sum (<*> the carrier of K) & ( for k being Nat st k in dom (<*> the carrier of K) holds
(<*> the carrier of K) . k = (s /. k) . i ) )

(0. ()) . i = 0. K by ;
hence (Sum s) . i = 0. K by
.= Sum (<*> the carrier of K) by RLVECT_1:43 ;
:: thesis: for k being Nat st k in dom (<*> the carrier of K) holds
(<*> the carrier of K) . k = (s /. k) . i

thus for k being Nat st k in dom (<*> the carrier of K) holds
(<*> the carrier of K) . k = (s /. k) . i ; :: thesis: verum
end;
P2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume AS1: S1[k] ; :: thesis: S1[k + 1]
let s be FinSequence of (); :: thesis: ( len s = k + 1 implies 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 ) ) )

assume AS2: len s = k + 1 ; :: thesis: 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 ) )

reconsider s0 = s | k as FinSequence of the carrier of () ;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then A70: k + 1 in dom s by ;
then s . (k + 1) in rng s by FUNCT_1:3;
then reconsider sk1 = s . (k + 1) as Element of the carrier of () ;
P1: len s0 = k by ;
then P4: dom s0 = Seg k by FINSEQ_1:def 3;
A9: len s = (len s0) + 1 by ;
s0 = s | (dom s0) by ;
then P3: Sum s = (Sum s0) + sk1 by ;
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 ;
s /. (k + 1) in the carrier of () ;
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 ;
reconsider ss = ss as FinSequence of the carrier of K ;
ss . i in rng ss by ;
then reconsider si0k1 = (s /. (k + 1)) . i as Element of K by XP4;
P2F: sk1 . i = si0k1 by ;
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 ;
for j being Nat st j in dom si holds
si . j = (s /. j) . i
proof
let j be Nat; :: thesis: ( j in dom si implies si . j = (s /. j) . i )
assume j in dom si ; :: thesis: si . j = (s /. j) . i
then A2: ( 1 <= j & j <= k + 1 ) by ;
per cases ( j <= k or j > k ) ;
suppose j <= k ; :: thesis: si . j = (s /. j) . i
then Q50: j in Seg k by A2;
then Q5: j in dom si0 by ;
hence si . j = si0 . j by FINSEQ_1:def 7
.= (s0 /. j) . i by
.= (s /. j) . i by ;
:: thesis: verum
end;
suppose j > k ; :: thesis: si . j = (s /. j) . i
then k + 1 <= j by NAT_1:13;
then j = k + 1 by ;
hence si . j = (s /. j) . i by ; :: thesis: verum
end;
end;
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: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(P1, P2);
hence for s being FinSequence of () 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: verum