let p1, p2 be FinSequence of REAL ; :: thesis: ( len p1 = len R & p1 . (len p1) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p1) - 1 holds
p1 . n = (R . n) - (R . (n + 1)) ) & len p2 = len R & p2 . (len p2) = R . (len R) & ( for n being Nat st 1 <= n & n <= (len p2) - 1 holds
p2 . n = (R . n) - (R . (n + 1)) ) implies p1 = p2 )
assume that
A6: ( len p1 = len R & p1 . (len p1) = R . (len R) ) and
A7: for n being Nat st 1 <= n & n <= (len p1) - 1 holds
p1 . n = (R . n) - (R . (n + 1)) and
A8: ( len p2 = len R & p2 . (len p2) = R . (len R) ) and
A9: for n being Nat st 1 <= n & n <= (len p2) - 1 holds
p2 . n = (R . n) - (R . (n + 1)) ; :: thesis: p1 = p2
X: dom p1 = Seg (len R) by A6, FINSEQ_1:def 3;

now

let n be Nat; :: thesis: ( n in dom p1 implies p1 . n = p2 . n )
assume n in dom p1 ; :: thesis: p1 . n = p2 . n
then A10: ( 1 <= n & n <= len R ) by X, FINSEQ_1:3;
set r = R . n;

now

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

case n = len R ; :: thesis: p1 . n = p2 . n

hence p1 . n = p2 . n by A6, A8; :: thesis: verum

end;

case n <> len R ; :: thesis: p1 . n = p2 . n

then ( n < len R & n <= n + 1 ) by A10, NAT_1:11, XXREAL_0:1;
then A11: ( 1 <= n + 1 & n + 1 <= len R ) by A10, NAT_1:13;
set s = R . (n + 1);
n <= (len R) - 1 by A11, XREAL_1:21;
then ( p1 . n = (R . n) - (R . (n + 1)) & p2 . n = (R . n) - (R . (n + 1)) ) by A6, A7, A8, A9, A10;
hence p1 . n = p2 . n ; :: thesis: verum

end;

end;

end;

hence p1 . n = p2 . n ; :: thesis: verum

end;

hence p1 = p2 by A6, A8, FINSEQ_2:10; :: thesis: verum