let n be Nat; :: thesis: for f, f1, f2 being FinSequence of REAL st len f = n + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) )

defpred S_{1}[ Nat] means for f, f1, f2 being FinSequence of REAL st len f = $1 + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ($1 + 1))) - (f2 . 1) );

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A33, A1);

hence for f, f1, f2 being FinSequence of REAL st len f = n + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) ) ; :: thesis: verum

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) )

defpred S

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ($1 + 1))) - (f2 . 1) );

A1: for n being Nat st S

S

proof

A33:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let f, f1, f2 be FinSequence of REAL ; :: thesis: ( len f = (n + 1) + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) implies ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ((n + 1) + 1))) - (f2 . 1) ) )

assume that

A3: len f = (n + 1) + 1 and

A4: len f1 = len f and

A5: len f2 = len f and

A6: for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ; :: thesis: ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ((n + 1) + 1))) - (f2 . 1) )

set ff1 = f1 | (Seg (n + 1));

reconsider ff1 = f1 | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A7: len ff1 = n + 1 by A3, A4, FINSEQ_3:53;

set ff2 = f2 | (Seg (n + 1));

reconsider ff2 = f2 | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A8: f2 = ff2 ^ <*(f2 . ((n + 1) + 1))*> by A3, A5, FINSEQ_3:55;

A9: len ff2 = n + 1 by A3, A5, FINSEQ_3:53;

then ff2 <> {} ;

then 1 in dom ff2 by FINSEQ_5:6;

then A10: ff2 . 1 = f2 . 1 by A8, FINSEQ_1:def 7;

A11: f1 = ff1 ^ <*(f1 . ((n + 1) + 1))*> by A3, A4, FINSEQ_3:55;

(n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:4;

then (n + 1) + 1 in dom f by A3, FINSEQ_1:def 3;

then A12: f . ((n + 1) + 1) = (f1 . ((n + 1) + 1)) - (f2 . ((n + 1) + 1)) by A6;

set f3 = f | (Seg (n + 1));

reconsider f3 = f | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A13: dom f3 = Seg (n + 1) by A3, FINSEQ_3:54;

then A14: len f3 = n + 1 by FINSEQ_1:def 3;

A15: f = f3 ^ <*(f . ((n + 1) + 1))*> by A3, FINSEQ_3:55;

A16: for d being Nat st d in dom f3 holds

f3 . d = (ff1 . d) - (ff2 . d)

then n + 1 in dom ff1 by A7, FINSEQ_5:6;

then ff1 . (n + 1) = f1 . (n + 1) by A11, FINSEQ_1:def 7;

then consider f4 being FinSequence of REAL such that

A21: len f4 = (len f3) - 1 and

A22: for d being Nat st d in dom f4 holds

f4 . d = (ff1 . d) - (ff2 . (d + 1)) and

A23: Sum f3 = ((Sum f4) + (f1 . (n + 1))) - (f2 . 1) by A2, A14, A7, A9, A16, A10;

take f5 = f4 ^ <*((f1 . (n + 1)) - (f2 . (n + 2)))*>; :: thesis: ( f5 is Element of bool [:omega,REAL:] & f5 is FinSequence of REAL & len f5 = (len f) - 1 & ( for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) )

(f1 . (n + 1)) - (f2 . (n + 2)) is Element of REAL by XREAL_0:def 1;

then <*((f1 . (n + 1)) - (f2 . (n + 2)))*> is FinSequence of REAL by FINSEQ_1:74;

then reconsider f5 = f5 as FinSequence of REAL by FINSEQ_1:75;

A24: Sum f = (((Sum f4) + (f1 . (n + 1))) - (f2 . 1)) + (f . ((n + 1) + 1)) by A15, A23, RVSUM_1:74

.= (((Sum f4) + ((f1 . (n + 1)) - (f2 . (n + 2)))) + (f1 . ((n + 1) + 1))) - (f2 . 1) by A12

.= ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) by RVSUM_1:74 ;

A25: (len f4) + 1 = n + 1 by A13, A21, FINSEQ_1:def 3;

A26: for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1))

.= (len f) - 1 by A3, A13, A21, FINSEQ_1:def 3 ;

hence ( f5 is Element of bool [:omega,REAL:] & f5 is FinSequence of REAL & len f5 = (len f) - 1 & ( for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) ) by A26, A24; :: thesis: verum

end;assume A2: S

let f, f1, f2 be FinSequence of REAL ; :: thesis: ( len f = (n + 1) + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) implies ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ((n + 1) + 1))) - (f2 . 1) ) )

assume that

A3: len f = (n + 1) + 1 and

A4: len f1 = len f and

A5: len f2 = len f and

A6: for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ; :: thesis: ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . ((n + 1) + 1))) - (f2 . 1) )

set ff1 = f1 | (Seg (n + 1));

reconsider ff1 = f1 | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A7: len ff1 = n + 1 by A3, A4, FINSEQ_3:53;

set ff2 = f2 | (Seg (n + 1));

reconsider ff2 = f2 | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A8: f2 = ff2 ^ <*(f2 . ((n + 1) + 1))*> by A3, A5, FINSEQ_3:55;

A9: len ff2 = n + 1 by A3, A5, FINSEQ_3:53;

then ff2 <> {} ;

then 1 in dom ff2 by FINSEQ_5:6;

then A10: ff2 . 1 = f2 . 1 by A8, FINSEQ_1:def 7;

A11: f1 = ff1 ^ <*(f1 . ((n + 1) + 1))*> by A3, A4, FINSEQ_3:55;

(n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:4;

then (n + 1) + 1 in dom f by A3, FINSEQ_1:def 3;

then A12: f . ((n + 1) + 1) = (f1 . ((n + 1) + 1)) - (f2 . ((n + 1) + 1)) by A6;

set f3 = f | (Seg (n + 1));

reconsider f3 = f | (Seg (n + 1)) as FinSequence of REAL by FINSEQ_1:18;

A13: dom f3 = Seg (n + 1) by A3, FINSEQ_3:54;

then A14: len f3 = n + 1 by FINSEQ_1:def 3;

A15: f = f3 ^ <*(f . ((n + 1) + 1))*> by A3, FINSEQ_3:55;

A16: for d being Nat st d in dom f3 holds

f3 . d = (ff1 . d) - (ff2 . d)

proof

ff1 <> {}
by A7;
let d be Nat; :: thesis: ( d in dom f3 implies f3 . d = (ff1 . d) - (ff2 . d) )

A17: dom f3 c= dom f by A15, FINSEQ_1:26;

assume A18: d in dom f3 ; :: thesis: f3 . d = (ff1 . d) - (ff2 . d)

then A19: d in dom ff2 by A13, A9, FINSEQ_1:def 3;

d in dom ff1 by A13, A7, A18, FINSEQ_1:def 3;

then A20: f1 . d = ff1 . d by A11, FINSEQ_1:def 7;

f3 . d = f . d by A15, A18, FINSEQ_1:def 7

.= (f1 . d) - (f2 . d) by A6, A18, A17 ;

hence f3 . d = (ff1 . d) - (ff2 . d) by A8, A19, A20, FINSEQ_1:def 7; :: thesis: verum

end;A17: dom f3 c= dom f by A15, FINSEQ_1:26;

assume A18: d in dom f3 ; :: thesis: f3 . d = (ff1 . d) - (ff2 . d)

then A19: d in dom ff2 by A13, A9, FINSEQ_1:def 3;

d in dom ff1 by A13, A7, A18, FINSEQ_1:def 3;

then A20: f1 . d = ff1 . d by A11, FINSEQ_1:def 7;

f3 . d = f . d by A15, A18, FINSEQ_1:def 7

.= (f1 . d) - (f2 . d) by A6, A18, A17 ;

hence f3 . d = (ff1 . d) - (ff2 . d) by A8, A19, A20, FINSEQ_1:def 7; :: thesis: verum

then n + 1 in dom ff1 by A7, FINSEQ_5:6;

then ff1 . (n + 1) = f1 . (n + 1) by A11, FINSEQ_1:def 7;

then consider f4 being FinSequence of REAL such that

A21: len f4 = (len f3) - 1 and

A22: for d being Nat st d in dom f4 holds

f4 . d = (ff1 . d) - (ff2 . (d + 1)) and

A23: Sum f3 = ((Sum f4) + (f1 . (n + 1))) - (f2 . 1) by A2, A14, A7, A9, A16, A10;

take f5 = f4 ^ <*((f1 . (n + 1)) - (f2 . (n + 2)))*>; :: thesis: ( f5 is Element of bool [:omega,REAL:] & f5 is FinSequence of REAL & len f5 = (len f) - 1 & ( for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) )

(f1 . (n + 1)) - (f2 . (n + 2)) is Element of REAL by XREAL_0:def 1;

then <*((f1 . (n + 1)) - (f2 . (n + 2)))*> is FinSequence of REAL by FINSEQ_1:74;

then reconsider f5 = f5 as FinSequence of REAL by FINSEQ_1:75;

A24: Sum f = (((Sum f4) + (f1 . (n + 1))) - (f2 . 1)) + (f . ((n + 1) + 1)) by A15, A23, RVSUM_1:74

.= (((Sum f4) + ((f1 . (n + 1)) - (f2 . (n + 2)))) + (f1 . ((n + 1) + 1))) - (f2 . 1) by A12

.= ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) by RVSUM_1:74 ;

A25: (len f4) + 1 = n + 1 by A13, A21, FINSEQ_1:def 3;

A26: for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1))

proof

len f5 =
(len f4) + 1
by FINSEQ_2:16
let d be Nat; :: thesis: ( d in dom f5 implies f5 . d = (f1 . d) - (f2 . (d + 1)) )

assume d in dom f5 ; :: thesis: f5 . d = (f1 . d) - (f2 . (d + 1))

then d in Seg (len f5) by FINSEQ_1:def 3;

then d in Seg ((len f4) + 1) by FINSEQ_2:16;

then d in (Seg (len f4)) \/ {((len f4) + 1)} by FINSEQ_1:9;

then A27: ( d in Seg (len f4) or d in {((len f4) + 1)} ) by XBOOLE_0:def 3;

end;assume d in dom f5 ; :: thesis: f5 . d = (f1 . d) - (f2 . (d + 1))

then d in Seg (len f5) by FINSEQ_1:def 3;

then d in Seg ((len f4) + 1) by FINSEQ_2:16;

then d in (Seg (len f4)) \/ {((len f4) + 1)} by FINSEQ_1:9;

then A27: ( d in Seg (len f4) or d in {((len f4) + 1)} ) by XBOOLE_0:def 3;

per cases
( d in Seg (len f4) or d = (len f4) + 1 )
by A27, TARSKI:def 1;

end;

suppose A28:
d in Seg (len f4)
; :: thesis: f5 . d = (f1 . d) - (f2 . (d + 1))

then
d + 1 in Seg ((len f4) + 1)
by FINSEQ_1:60;

then d + 1 in Seg (len ff2) by A3, A5, A14, A21, FINSEQ_3:53;

then A29: d + 1 in dom ff2 by FINSEQ_1:def 3;

A30: d in dom f4 by A28, FINSEQ_1:def 3;

len f4 <= len ff1 by A14, A7, A21, XREAL_1:147;

then dom f4 c= dom ff1 by FINSEQ_3:30;

then A31: f1 . d = ff1 . d by A11, A30, FINSEQ_1:def 7;

f5 . d = f4 . d by A30, FINSEQ_1:def 7

.= (ff1 . d) - (ff2 . (d + 1)) by A22, A30 ;

hence f5 . d = (f1 . d) - (f2 . (d + 1)) by A8, A31, A29, FINSEQ_1:def 7; :: thesis: verum

end;then d + 1 in Seg (len ff2) by A3, A5, A14, A21, FINSEQ_3:53;

then A29: d + 1 in dom ff2 by FINSEQ_1:def 3;

A30: d in dom f4 by A28, FINSEQ_1:def 3;

len f4 <= len ff1 by A14, A7, A21, XREAL_1:147;

then dom f4 c= dom ff1 by FINSEQ_3:30;

then A31: f1 . d = ff1 . d by A11, A30, FINSEQ_1:def 7;

f5 . d = f4 . d by A30, FINSEQ_1:def 7

.= (ff1 . d) - (ff2 . (d + 1)) by A22, A30 ;

hence f5 . d = (f1 . d) - (f2 . (d + 1)) by A8, A31, A29, FINSEQ_1:def 7; :: thesis: verum

suppose A32:
d = (len f4) + 1
; :: thesis: f5 . d = (f1 . d) - (f2 . (d + 1))

1 in Seg 1
by FINSEQ_1:2, TARSKI:def 1;

then 1 in dom <*((f1 . (n + 1)) - (f2 . (n + 2)))*> by FINSEQ_1:38;

then f5 . d = <*((f1 . (n + 1)) - (f2 . (n + 2)))*> . 1 by A32, FINSEQ_1:def 7

.= (f1 . d) - (f2 . (d + 1)) by A25, A32, FINSEQ_1:40 ;

hence f5 . d = (f1 . d) - (f2 . (d + 1)) ; :: thesis: verum

end;then 1 in dom <*((f1 . (n + 1)) - (f2 . (n + 2)))*> by FINSEQ_1:38;

then f5 . d = <*((f1 . (n + 1)) - (f2 . (n + 2)))*> . 1 by A32, FINSEQ_1:def 7

.= (f1 . d) - (f2 . (d + 1)) by A25, A32, FINSEQ_1:40 ;

hence f5 . d = (f1 . d) - (f2 . (d + 1)) ; :: thesis: verum

.= (len f) - 1 by A3, A13, A21, FINSEQ_1:def 3 ;

hence ( f5 is Element of bool [:omega,REAL:] & f5 is FinSequence of REAL & len f5 = (len f) - 1 & ( for d being Nat st d in dom f5 holds

f5 . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum f5) + (f1 . ((n + 1) + 1))) - (f2 . 1) ) by A26, A24; :: thesis: verum

proof

for n being Nat holds S
let f, f1, f2 be FinSequence of REAL ; :: thesis: ( len f = 0 + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) implies ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (0 + 1))) - (f2 . 1) ) )

assume that

A34: len f = 0 + 1 and

len f1 = len f and

len f2 = len f and

A35: for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ; :: thesis: ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (0 + 1))) - (f2 . 1) )

take <*> REAL ; :: thesis: ( len (<*> REAL) = (len f) - 1 & ( for d being Nat st d in dom (<*> REAL) holds

(<*> REAL) . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum (<*> REAL)) + (f1 . (0 + 1))) - (f2 . 1) )

0 + 1 in Seg (0 + 1) by FINSEQ_1:4;

then 1 in dom f by A34, FINSEQ_1:def 3;

then f . 1 = (f1 . 1) - (f2 . 1) by A35;

then f = <*((f1 . 1) - (f2 . 1))*> by A34, FINSEQ_1:40;

hence ( len (<*> REAL) = (len f) - 1 & ( for d being Nat st d in dom (<*> REAL) holds

(<*> REAL) . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum (<*> REAL)) + (f1 . (0 + 1))) - (f2 . 1) ) by A34, RVSUM_1:72, RVSUM_1:73; :: thesis: verum

end;f . d = (f1 . d) - (f2 . d) ) implies ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (0 + 1))) - (f2 . 1) ) )

assume that

A34: len f = 0 + 1 and

len f1 = len f and

len f2 = len f and

A35: for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ; :: thesis: ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (0 + 1))) - (f2 . 1) )

take <*> REAL ; :: thesis: ( len (<*> REAL) = (len f) - 1 & ( for d being Nat st d in dom (<*> REAL) holds

(<*> REAL) . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum (<*> REAL)) + (f1 . (0 + 1))) - (f2 . 1) )

0 + 1 in Seg (0 + 1) by FINSEQ_1:4;

then 1 in dom f by A34, FINSEQ_1:def 3;

then f . 1 = (f1 . 1) - (f2 . 1) by A35;

then f = <*((f1 . 1) - (f2 . 1))*> by A34, FINSEQ_1:40;

hence ( len (<*> REAL) = (len f) - 1 & ( for d being Nat st d in dom (<*> REAL) holds

(<*> REAL) . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum (<*> REAL)) + (f1 . (0 + 1))) - (f2 . 1) ) by A34, RVSUM_1:72, RVSUM_1:73; :: thesis: verum

hence for f, f1, f2 being FinSequence of REAL st len f = n + 1 & len f1 = len f & len f2 = len f & ( for d being Nat st d in dom f holds

f . d = (f1 . d) - (f2 . d) ) holds

ex fr being FinSequence of REAL st

( len fr = (len f) - 1 & ( for d being Nat st d in dom fr holds

fr . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum fr) + (f1 . (n + 1))) - (f2 . 1) ) ; :: thesis: verum