let n be Element of NAT ; :: thesis: for E being Element of REAL n
for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
E = Sum p
let E be Element of REAL n; :: thesis: for p being FinSequence of REAL n st ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) holds
E = Sum p
defpred S₁[ Nat] means for p being FinSequence of REAL n
for r being Element of REAL n st len p = $1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p;
A1: S₁[ 0 ]

proof

let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n st len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p
let r be Element of REAL n; :: thesis: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p )
assume A2: ( len p = 0 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; :: thesis: r = Sum p
A3: p = {} by A2;
len r = n by CARD_1:def 7;
then A4: dom r = Seg n by FINSEQ_1:def 3;
A5: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13;

A6: now :: thesis: for x being object st x in dom r holds
r . x = ((Seg n) --> 0) . x

let x be object ; :: thesis: ( x in dom r implies r . x = ((Seg n) --> 0) . x )
assume A7: x in dom r ; :: thesis: r . x = ((Seg n) --> 0) . x
then reconsider i = x as Element of NAT ;
set P = proj (i,n);
consider Pi being FinSequence of REAL such that
A8: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A2, A4, A7;
r . x = 0 by A3, A8, RVSUM_1:72;
hence r . x = ((Seg n) --> 0) . x by A4, A7, FUNCOP_1:7; :: thesis: verum

end;

Sum p = 0* n by A2, EUCLID_7:def 11;
hence r = Sum p by A6, A4, A5, FUNCT_1:2; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A10: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for p being FinSequence of REAL n
for r being Element of REAL n st len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p

let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n st len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) holds
r = Sum p
let r be Element of REAL n; :: thesis: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) implies r = Sum p )
assume A11: ( len p = k + 1 & ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & r . i = Sum Pi ) ) ) ; :: thesis: r = Sum p
set p1 = p | k;
k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom p by A11, FINSEQ_1:def 3;
then p . (k + 1) in rng p by FUNCT_1:3;
then reconsider pk1 = p . (k + 1) as Element of REAL n ;
defpred S₂[ Nat, set ] means ex P1i being FinSequence of REAL st
( P1i = (proj ($1,n)) * (p | k) & $2 = Sum P1i );
A12: for i being Nat st i in Seg n holds
ex r being Element of REAL st S₂[i,r]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S₂[i,r] )
assume i in Seg n ; :: thesis: ex r being Element of REAL st S₂[i,r]
reconsider S = Sum ((proj (i,n)) * (p | k)) as Element of REAL by XREAL_0:def 1;
take S ; :: thesis: S₂[i,S]
thus S₂[i,S] ; :: thesis: verum

end;

consider r1 being FinSequence of REAL such that
A13: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds
S₂[i,r1 . i] ) ) from FINSEQ_1:sch 5(A12);
len r1 = n by A13, FINSEQ_1:def 3;
then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92;
A14: for i being Element of NAT st i in Seg n holds
ex P1i being FinSequence of REAL st
( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A13;
A15: k <= len p by A11, NAT_1:16;
then A16: len (p | k) = k by FINSEQ_1:59;
A17: len r = n by CARD_1:def 7;
A18: len (r1 + pk1) = n by CARD_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= n holds
r . i = (r1 + pk1) . i

let i be Nat; :: thesis: ( 1 <= i & i <= n implies r . i = (r1 + pk1) . i )
set P = proj (i,n);
assume ( 1 <= i & i <= n ) ; :: thesis: r . i = (r1 + pk1) . i
then A19: i in Seg n ;
consider Pi being FinSequence of REAL such that
A20: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by A19, A11;
consider P1i being FinSequence of REAL such that
A21: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A19, A13;
A22: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then A23: rng p c= dom (proj (i,n)) ;
A24: dom Pi = dom p by A23, A20, RELAT_1:27
.= Seg (len p) by FINSEQ_1:def 3 ;
A25: len p = (len (p | k)) + (len <*(pk1 . i)*>) by A11, A16, FINSEQ_1:40;
A26: rng (p | k) c= dom (proj (i,n)) by A22;
A27: dom P1i = dom (p | k) by A26, A21, RELAT_1:27
.= Seg (len (p | k)) by FINSEQ_1:def 3 ;
then A28: len P1i = len (p | k) by FINSEQ_1:def 3;
A29: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A24, A25, A27, FINSEQ_1:def 3;
len (p | k) <= len p by A15, FINSEQ_1:59;
then A30: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5;
A31: for k being Nat st k in dom P1i holds
Pi . k = P1i . k

proof

let k be Nat; :: thesis: ( k in dom P1i implies Pi . k = P1i . k )
assume A32: k in dom P1i ; :: thesis: Pi . k = P1i . k
then A33: k in dom (p | k) by A27, FINSEQ_1:def 3;
thus P1i . k = (proj (i,n)) . ((p | k) . k) by A21, A32, FUNCT_1:12
.= (proj (i,n)) . (p . k) by A33, FUNCT_1:47
.= Pi . k by A20, A32, A24, A27, A30, FUNCT_1:12 ; :: thesis: verum

end;

for k being Nat st k in dom <*(pk1 . i)*> holds
Pi . ((len P1i) + k) = <*(pk1 . i)*> . k

proof

let j be Nat; :: thesis: ( j in dom <*(pk1 . i)*> implies Pi . ((len P1i) + j) = <*(pk1 . i)*> . j )
assume j in dom <*(pk1 . i)*> ; :: thesis: Pi . ((len P1i) + j) = <*(pk1 . i)*> . j
then j in Seg (len <*(pk1 . i)*>) by FINSEQ_1:def 3;
then j in Seg 1 by FINSEQ_1:40;
then A34: j = 1 by FINSEQ_1:2, TARSKI:def 1;
hence Pi . ((len P1i) + j) = (proj (i,n)) . (p . (k + 1)) by A20, A24, A11, A28, A16, FINSEQ_1:4, FUNCT_1:12
.= pk1 . i by PDIFF_1:def 1
.= <*(pk1 . i)*> . j by A34 ;
:: thesis: verum

end;

then Pi = P1i ^ <*(pk1 . i)*> by A31, A29, FINSEQ_1:def 7;
hence r . i = (r1 . i) + (pk1 . i) by A20, A21, RVSUM_1:74
.= (r1 + pk1) . i by RVSUM_1:11 ;
:: thesis: verum

end;

then A35: r = r1 + pk1 by A17, A18;
ex v being Element of REAL n st
( v = p . (len p) & Sum p = (Sum (p | k)) + v ) by A16, A11, PDIFF_6:15;
hence r = Sum p by A11, A35, A10, A14, A16; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A36: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A9);
let p be FinSequence of REAL n; :: thesis: ( ( for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ) implies E = Sum p )
assume A37: for i being Element of NAT st i in Seg n holds
ex Pi being FinSequence of REAL st
( Pi = (proj (i,n)) * p & E . i = Sum Pi ) ; :: thesis: E = Sum p
len p = len p ;
hence E = Sum p by A37, A36; :: thesis: verum