let K be Field; :: thesis: for n, i being Nat st i in Seg n holds

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 ) )

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

assume AS: i in Seg n ; :: thesis: 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 ) )

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_{1}[ 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_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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: verum

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 ) )

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

assume AS: i in Seg n ; :: thesis: 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 ) )

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

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

proof

P2:
for k being Nat st S
let s be FinSequence of (n -VectSp_over K); :: 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 (n -VectSp_over K) 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. (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: 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;( 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 (n -VectSp_over K) 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. (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: 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

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume AS1: S_{1}[k]
; :: thesis: S_{1}[k + 1]

let s be FinSequence of (n -VectSp_over K); :: 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 (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

( 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;assume AS1: S

let s be FinSequence of (n -VectSp_over K); :: 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 (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

hence
ex si being FinSequence of K st
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 Y1, AS2, FINSEQ_3:25;

end;assume j in dom si ; :: thesis: si . j = (s /. j) . i

then A2: ( 1 <= j & j <= k + 1 ) by Y1, AS2, FINSEQ_3:25;

( 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

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: verum