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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[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 ;
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 ;
A9: len ff2 = n + 1 by ;
then ff2 <> {} ;
then 1 in dom ff2 by FINSEQ_5:6;
then A10: ff2 . 1 = f2 . 1 by ;
A11: f1 = ff1 ^ <*(f1 . ((n + 1) + 1))*> by ;
(n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:4;
then (n + 1) + 1 in dom f by ;
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 ;
then A14: len f3 = n + 1 by FINSEQ_1:def 3;
A15: f = f3 ^ <*(f . ((n + 1) + 1))*> by ;
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 ;
assume A18: d in dom f3 ; :: thesis: f3 . d = (ff1 . d) - (ff2 . d)
then A19: d in dom ff2 by ;
d in dom ff1 by ;
then A20: f1 . d = ff1 . d by ;
f3 . d = f . d by
.= (f1 . d) - (f2 . d) by A6, A18, A17 ;
hence f3 . d = (ff1 . d) - (ff2 . d) by ; :: thesis: verum
end;
ff1 <> {} by A7;
then n + 1 in dom ff1 by ;
then ff1 . (n + 1) = f1 . (n + 1) by ;
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 & 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
.= (((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 ;
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 ;
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 ;
then A29: d + 1 in dom ff2 by FINSEQ_1:def 3;
A30: d in dom f4 by ;
len f4 <= len ff1 by ;
then dom f4 c= dom ff1 by FINSEQ_3:30;
then A31: f1 . d = ff1 . d by ;
f5 . d = f4 . d by
.= (ff1 . d) - (ff2 . (d + 1)) by ;
hence f5 . d = (f1 . d) - (f2 . (d + 1)) by ; :: thesis: verum
end;
suppose A32: d = (len f4) + 1 ; :: thesis: f5 . d = (f1 . d) - (f2 . (d + 1))
1 in Seg 1 by ;
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
.= (f1 . d) - (f2 . (d + 1)) by ;
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 ;
hence ( f5 is Element of bool & 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 ; :: thesis: verum
end;
A33: S1[ 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 () = (len f) - 1 & ( for d being Nat st d in dom () holds
() . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum ()) + (f1 . (0 + 1))) - (f2 . 1) )

0 + 1 in Seg (0 + 1) by FINSEQ_1:4;
then 1 in dom f by ;
then f . 1 = (f1 . 1) - (f2 . 1) by A35;
then f = <*((f1 . 1) - (f2 . 1))*> by ;
hence ( len () = (len f) - 1 & ( for d being Nat st d in dom () holds
() . d = (f1 . d) - (f2 . (d + 1)) ) & Sum f = ((Sum ()) + (f1 . (0 + 1))) - (f2 . 1) ) by ; :: thesis: verum
end;
for n being Nat holds S1[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