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 (REAL-NS n) 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 S_{1}[ Nat] means for p being FinSequence of REAL n

for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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: S_{1}[ 0 ]
_{1}[k] holds

S_{1}[k + 1]
_{1}[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 (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 A40, A39; :: thesis: verum

for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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 S

for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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: S

proof

A9:
for k being Nat st S
let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 (REAL-NS n) 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;

then r = 0. (REAL-NS n) by REAL_NS1:def 4;

hence r = Sum q by A4, RLVECT_1:43; :: thesis: verum

end;for q being FinSequence of (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 (REAL-NS n) 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

then
r = 0* n
by A5, A6, FUNCT_1:2;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 A3, A8, RVSUM_1:72;

hence r . x = ((Seg n) --> 0) . x by A5, A7, FUNCOP_1:7; :: thesis: verum

end;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 A3, A8, RVSUM_1:72;

hence r . x = ((Seg n) --> 0) . x by A5, A7, FUNCOP_1:7; :: thesis: verum

then r = 0. (REAL-NS n) by REAL_NS1:def 4;

hence r = Sum q by A4, RLVECT_1:43; :: thesis: verum

S

proof

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

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

_{1}[k + 1]
; :: thesis: verum

end;assume A10: S

now :: thesis: for p being FinSequence of REAL n

for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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

hence
Sfor r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 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 ;

set q1 = q | k;

k + 1 in dom q by A11, A12, FINSEQ_1:def 3;

then q . (k + 1) in rng q by FUNCT_1:3;

then reconsider qk1 = q . (k + 1) as Point of (REAL-NS n) ;

defpred S_{2}[ 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 S_{2}[i,r]

A14: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds

S_{2}[i,r1 . i] ) )
from FINSEQ_1:sch 5(A13);

len r1 = n by A14, FINSEQ_1:def 3;

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 A11, NAT_1:16;

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;

A37: len q = (len (q | k)) + 1 by A16, A11, FINSEQ_1:59;

A38: q | k = q | (dom (q | k)) by A17, A11, FINSEQ_1:def 3;

thus r = (Sum (q | k)) + qk1 by A36, A18, A11, REAL_NS1:2

.= Sum q by A11, A37, A38, RLVECT_1:38 ; :: thesis: verum

end;for q being FinSequence of (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 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 ;

set q1 = q | k;

k + 1 in dom q by A11, A12, FINSEQ_1:def 3;

then q . (k + 1) in rng q by FUNCT_1:3;

then reconsider qk1 = q . (k + 1) as Point of (REAL-NS n) ;

defpred S

( 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 S

proof

consider r1 being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg n implies ex r being Element of REAL st S_{2}[i,r] )

assume i in Seg n ; :: thesis: ex r being Element of REAL st S_{2}[i,r]

reconsider S = Sum ((proj (i,n)) * (p | k)) as Element of REAL by XREAL_0:def 1;

take S ; :: thesis: S_{2}[i,S]

thus S_{2}[i,S]
; :: thesis: verum

end;assume i in Seg n ; :: thesis: ex r being Element of REAL st S

reconsider S = Sum ((proj (i,n)) * (p | k)) as Element of REAL by XREAL_0:def 1;

take S ; :: thesis: S

thus S

A14: ( dom r1 = Seg n & ( for i being Nat st i in Seg n holds

S

len r1 = n by A14, FINSEQ_1:def 3;

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 A11, NAT_1:16;

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

then A36:
r = r1 + pk1
by A19, A20;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 A21, A11;

consider P1i being FinSequence of REAL such that

A23: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A21, A14;

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 A25, A22, RELAT_1:27

.= Seg (len p) by FINSEQ_1:def 3 ;

A27: len p = (len (p | k)) + 1 by A11, A16, FINSEQ_1:59

.= (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 A28, A23, RELAT_1:27

.= Seg (len (p | k)) by FINSEQ_1:def 3 ;

then A30: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A26, A27, FINSEQ_1:def 3;

len (p | k) <= len p by A16, FINSEQ_1:59;

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

Pi . ((len P1i) + k) = <*(pk1 . i)*> . k

hence r . i = (r1 . i) + (pk1 . i) by A22, A23, RVSUM_1:74

.= (r1 + pk1) . i by RVSUM_1:11 ;

:: thesis: verum

end;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 A21, A11;

consider P1i being FinSequence of REAL such that

A23: ( P1i = (proj (i,n)) * (p | k) & r1 . i = Sum P1i ) by A21, A14;

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 A25, A22, RELAT_1:27

.= Seg (len p) by FINSEQ_1:def 3 ;

A27: len p = (len (p | k)) + 1 by A11, A16, FINSEQ_1:59

.= (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 A28, A23, RELAT_1:27

.= Seg (len (p | k)) by FINSEQ_1:def 3 ;

then A30: dom Pi = Seg ((len P1i) + (len <*(pk1 . i)*>)) by A26, A27, FINSEQ_1:def 3;

len (p | k) <= len p by A16, FINSEQ_1:59;

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

for k being Nat st k in dom <*(pk1 . i)*> holds
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 A29, FINSEQ_1:def 3;

thus P1i . k = (proj (i,n)) . ((p | k) . k) by A23, A33, FUNCT_1:12

.= (proj (i,n)) . (p . k) by A34, FUNCT_1:47

.= Pi . k by A22, A33, A29, A26, A31, FUNCT_1:12 ; :: thesis: verum

end;assume A33: k in dom P1i ; :: thesis: Pi . k = P1i . k

then A34: k in dom (p | k) by A29, FINSEQ_1:def 3;

thus P1i . k = (proj (i,n)) . ((p | k) . k) by A23, A33, FUNCT_1:12

.= (proj (i,n)) . (p . k) by A34, FUNCT_1:47

.= Pi . k by A22, A33, A29, A26, A31, FUNCT_1:12 ; :: thesis: verum

Pi . ((len P1i) + k) = <*(pk1 . i)*> . k

proof

then
Pi = P1i ^ <*(pk1 . i)*>
by A32, A30, FINSEQ_1:def 7;
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 FINSEQ_1:2, FINSEQ_1:40;

then A35: j = 1 by TARSKI:def 1;

thus Pi . ((len P1i) + j) = Pi . (k + 1) by A29, A17, A35, FINSEQ_1:def 3

.= (proj (i,n)) . (p . (k + 1)) by A22, A26, A11, FINSEQ_1:4, FUNCT_1:12

.= pk1 . i by PDIFF_1:def 1

.= <*(pk1 . i)*> . j by A35, FINSEQ_1:40 ; :: thesis: verum

end;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 FINSEQ_1:2, FINSEQ_1:40;

then A35: j = 1 by TARSKI:def 1;

thus Pi . ((len P1i) + j) = Pi . (k + 1) by A29, A17, A35, FINSEQ_1:def 3

.= (proj (i,n)) . (p . (k + 1)) by A22, A26, A11, FINSEQ_1:4, FUNCT_1:12

.= pk1 . i by PDIFF_1:def 1

.= <*(pk1 . i)*> . j by A35, FINSEQ_1:40 ; :: thesis: verum

hence r . i = (r1 . i) + (pk1 . i) by A22, A23, RVSUM_1:74

.= (r1 + pk1) . i by RVSUM_1:11 ;

:: thesis: verum

A37: len q = (len (q | k)) + 1 by A16, A11, FINSEQ_1:59;

A38: q | k = q | (dom (q | k)) by A17, A11, FINSEQ_1:def 3;

thus r = (Sum (q | k)) + qk1 by A36, A18, A11, REAL_NS1:2

.= Sum q by A11, A37, A38, RLVECT_1:38 ; :: thesis: verum

let p be FinSequence of REAL n; :: thesis: for r being Element of REAL n

for q being FinSequence of (REAL-NS n) 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 (REAL-NS n) 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 (REAL-NS n); :: 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 A40, A39; :: thesis: verum