per cases ( len R = 0 or len R <> 0 ) ;
suppose A1: len R = 0 ; :: thesis: ex b1 being FinSequence of REAL st
( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) )
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;
suppose len R <> 0 ; :: thesis: ex b1 being FinSequence of REAL st
( len b1 = len R & b1 . (len b1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len b1) - 1 holds
b1 . n = (R . n) - (R . (n + 1)) ) )
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 S2[ 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 S2[n,x]
proof
let n be Nat; :: thesis: ( n in Seg l implies ex x being Element of REAL st S2[n,x] )
assume n in Seg l ; :: thesis: ex x being Element of REAL st S2[n,x]
consider x being Real such that
A3: S2[n,x] ;
reconsider x = x as Element of REAL by XREAL_0:def 1;
take x ; :: thesis: S2[n,x]
thus S2[n,x] by A3; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A4: ( dom p = Seg l & ( for n being Nat st n in Seg l holds
S2[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;
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;
end;