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₁[ 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[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)

proof

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;

ff1 <> {} by A7;
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) )
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

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;

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

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;

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 ;
hence f5 . d = (f1 . d) - (f2 . (d + 1)) ; :: thesis: verum

end;

end;

end;

len f5 = (len f4) + 1 by FINSEQ_2:16
.= (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;

A33: S₁[ 0 ]

proof

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;

for n being Nat holds S₁[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