per cases
( len R = 0 or len R <> 0 )
;

end;

suppose A1:
len R = 0
; :: thesis: ex b_{1} being FinSequence of REAL st

( len b_{1} = len R & b_{1} . (len b_{1}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{1}) - 1 holds

b_{1} . n = (R . n) - (R . (n + 1)) ) )

( len b

b

reconsider RR = R as FinSequence of REAL by RVSUM_1:145;

take a = RR; :: thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

thus ( len a = len R & a . (len a) = R . (len R) ) ; :: thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1))

let n be Nat; :: thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )

assume ( 1 <= n & n <= (len a) - 1 ) ; :: thesis: a . n = (R . n) - (R . (n + 1))

hence a . n = (R . n) - (R . (n + 1)) by A1; :: thesis: verum

end;take a = RR; :: thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

thus ( len a = len R & a . (len a) = R . (len R) ) ; :: thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1))

let n be Nat; :: thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )

assume ( 1 <= n & n <= (len a) - 1 ) ; :: thesis: a . n = (R . n) - (R . (n + 1))

hence a . n = (R . n) - (R . (n + 1)) by A1; :: thesis: verum

suppose
len R <> 0
; :: thesis: ex b_{1} being FinSequence of REAL st

( len b_{1} = len R & b_{1} . (len b_{1}) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b_{1}) - 1 holds

b_{1} . n = (R . n) - (R . (n + 1)) ) )

( len b

b

then
0 < len R
;

then 0 + 1 <= len R by NAT_1:13;

then max (0,((len R) - 1)) = (len R) - 1 by FINSEQ_2:4;

then reconsider l = (len R) - 1 as Element of NAT by FINSEQ_2:5;

defpred S_{2}[ Nat, object ] means $2 = (R . $1) - (R . ($1 + 1));

set t = R . (len R);

A2: for n being Nat st n in Seg l holds

ex x being Element of REAL st S_{2}[n,x]

A4: ( dom p = Seg l & ( for n being Nat st n in Seg l holds

S_{2}[n,p . n] ) )
from FINSEQ_1:sch 5(A2);

reconsider t = R . (len R) as Element of REAL by XREAL_0:def 1;

take a = p ^ <*t*>; :: thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

thus A5: len a = (len p) + (len <*t*>) by FINSEQ_1:22

.= l + (len <*t*>) by A4, FINSEQ_1:def 3

.= l + 1 by FINSEQ_1:39

.= len R ; :: thesis: ( a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

hence a . (len a) = a . (l + 1)

.= a . ((len p) + 1) by A4, FINSEQ_1:def 3

.= R . (len R) by FINSEQ_1:42 ;

:: thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1))

let n be Nat; :: thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )

assume ( 1 <= n & n <= (len a) - 1 ) ; :: thesis: a . n = (R . n) - (R . (n + 1))

then A6: n in Seg l by A5, FINSEQ_1:1;

then p . n = (R . n) - (R . (n + 1)) by A4;

hence a . n = (R . n) - (R . (n + 1)) by A4, A6, FINSEQ_1:def 7; :: thesis: verum

end;then 0 + 1 <= len R by NAT_1:13;

then max (0,((len R) - 1)) = (len R) - 1 by FINSEQ_2:4;

then reconsider l = (len R) - 1 as Element of NAT by FINSEQ_2:5;

defpred S

set t = R . (len R);

A2: for n being Nat st n in Seg l holds

ex x being Element of REAL st S

proof

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

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

consider x being Real such that

A3: S_{2}[n,x]
;

reconsider x = x as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S_{2}[n,x]

thus S_{2}[n,x]
by A3; :: thesis: verum

end;assume n in Seg l ; :: thesis: ex x being Element of REAL st S

consider x being Real such that

A3: S

reconsider x = x as Element of REAL by XREAL_0:def 1;

take x ; :: thesis: S

thus S

A4: ( dom p = Seg l & ( for n being Nat st n in Seg l holds

S

reconsider t = R . (len R) as Element of REAL by XREAL_0:def 1;

take a = p ^ <*t*>; :: thesis: ( len a = len R & a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

thus A5: len a = (len p) + (len <*t*>) by FINSEQ_1:22

.= l + (len <*t*>) by A4, FINSEQ_1:def 3

.= l + 1 by FINSEQ_1:39

.= len R ; :: thesis: ( a . (len a) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1)) ) )

hence a . (len a) = a . (l + 1)

.= a . ((len p) + 1) by A4, FINSEQ_1:def 3

.= R . (len R) by FINSEQ_1:42 ;

:: thesis: for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n = (R . n) - (R . (n + 1))

let n be Nat; :: thesis: ( 1 <= n & n <= (len a) - 1 implies a . n = (R . n) - (R . (n + 1)) )

assume ( 1 <= n & n <= (len a) - 1 ) ; :: thesis: a . n = (R . n) - (R . (n + 1))

then A6: n in Seg l by A5, FINSEQ_1:1;

then p . n = (R . n) - (R . (n + 1)) by A4;

hence a . n = (R . n) - (R . (n + 1)) by A4, A6, FINSEQ_1:def 7; :: thesis: verum