let n be Element of NAT ; :: thesis: for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of () st p = q & ( 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 q

defpred S1[ Nat] means for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of () st len p = \$1 & p = q & ( 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 q;
A1: S1[ 0 ]
proof
let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n
for q being FinSequence of () st len p = 0 & p = q & ( 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 q

let r be Element of REAL n; :: thesis: for q being FinSequence of () st len p = 0 & p = q & ( 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 q

let q be FinSequence of (); :: thesis: ( len p = 0 & p = q & ( 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 q )

assume A2: ( len p = 0 & p = q & ( 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 q
then A3: p = {} ;
A4: q = <*> the carrier of () by A2;
len r = n by CARD_1:def 7;
then A5: dom r = Seg n by FINSEQ_1:def 3;
A6: dom ((Seg n) --> 0) = Seg n by FUNCOP_1:13;
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, A5, A7;
r . x = 0 by ;
hence r . x = ((Seg n) --> 0) . x by ; :: thesis: verum
end;
then r = 0* n by ;
then r = 0. () by REAL_NS1:def 4;
hence r = Sum q by ; :: thesis: verum
end;
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for p being FinSequence of REAL n
for r being Element of REAL n
for q being FinSequence of () st len p = k + 1 & p = q & ( 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 q
let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n
for q being FinSequence of () st len p = k + 1 & p = q & ( 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 q

let r be Element of REAL n; :: thesis: for q being FinSequence of () st len p = k + 1 & p = q & ( 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 q

let q be FinSequence of (); :: thesis: ( len p = k + 1 & p = q & ( 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 q )

assume A11: ( len p = k + 1 & p = q & ( 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 q
set p1 = p | k;
A12: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom p by ;
then p . (k + 1) in rng p by FUNCT_1:3;
then reconsider pk1 = p . (k + 1) as Element of REAL n ;
set q1 = q | k;
k + 1 in dom q by ;
then q . (k + 1) in rng q by FUNCT_1:3;
then reconsider qk1 = q . (k + 1) as Point of () ;
defpred S2[ Nat, set ] means ex P1i being FinSequence of REAL st
( P1i = (proj (\$1,n)) * (p | k) & \$2 = Sum P1i );
A13: for i being Nat st i in Seg n holds
ex r being Element of REAL st S2[i,r]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S2[i,r] )
assume i in Seg n ; :: thesis: ex r being Element of REAL st S2[i,r]
reconsider S = Sum ((proj (i,n)) * (p | k)) as Element of REAL by XREAL_0:def 1;
take S ; :: thesis: S2[i,S]
thus S2[i,S] ; :: thesis: verum
end;
consider r1 being FinSequence of REAL such that
A14: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds
S2[i,r1 . i] ) ) from len r1 = n by ;
then reconsider r1 = r1 as Element of REAL n by FINSEQ_2:92;
A15: 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 A14;
A16: k <= len p by ;
then A17: len (p | k) = k by FINSEQ_1:59;
A18: r1 = Sum (q | k) by A10, A11, A15, A17;
A19: len r = n by CARD_1:def 7;
A20: 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 A21: i in Seg n ;
consider Pi being FinSequence of REAL such that
A22: ( Pi = (proj (i,n)) * p & r . i = Sum Pi ) by ;
consider P1i being FinSequence of REAL such that
A23: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by ;
A24: dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then A25: rng p c= dom (proj (i,n)) ;
A26: dom Pi = dom p by
.= Seg (len p) by FINSEQ_1:def 3 ;
A27: len p = (len (p | k)) + 1 by
.= (len (p | k)) + (len <*(pk1 . i)*>) by FINSEQ_1:40 ;
A28: rng (p | k) c= dom (proj (i,n)) by A24;
A29: dom P1i = dom (p | k) by
.= Seg (len (p | k)) by FINSEQ_1:def 3 ;
then A30: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by ;
len (p | k) <= len p by ;
then A31: Seg (len (p | k)) c= Seg (len p) by FINSEQ_1:5;
A32: 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 A33: k in dom P1i ; :: thesis: Pi . k = P1i . k
then A34: k in dom (p | k) by ;
thus P1i . k = (proj (i,n)) . ((p | k) . k) by
.= (proj (i,n)) . (p . k) by
.= Pi . k by ; :: 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 {1} by ;
then A35: j = 1 by TARSKI:def 1;
thus Pi . ((len P1i) + j) = Pi . (k + 1) by
.= (proj (i,n)) . (p . (k + 1)) by
.= pk1 . i by PDIFF_1:def 1
.= <*(pk1 . i)*> . j by ; :: thesis: verum
end;
then Pi = P1i ^ <*(pk1 . i)*> by ;
hence r . i = (r1 . i) + (pk1 . i) by
.= (r1 + pk1) . i by RVSUM_1:11 ;
:: thesis: verum
end;
then A36: r = r1 + pk1 by ;
A37: len q = (len (q | k)) + 1 by ;
A38: q | k = q | (dom (q | k)) by ;
thus r = (Sum (q | k)) + qk1 by
.= Sum q by ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A39: for k being Nat holds S1[k] from NAT_1:sch 2(A1, A9);
let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n
for q being FinSequence of () st p = q & ( 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 q

let r be Element of REAL n; :: thesis: for q being FinSequence of () st p = q & ( 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 q

let q be FinSequence of (); :: thesis: ( p = q & ( 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 q )

assume A40: ( p = q & ( 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 q
thus r = Sum q by ; :: thesis: verum