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
A7: len p1 = len R and
A8: p1 . (len p1) = R . (len R) and
A9: for n being Nat st 1 <= n & n <= (len p1) - 1 holds
p1 . n = (R . n) - (R . (n + 1)) and
A10: len p2 = len R and
A11: p2 . (len p2) = R . (len R) and
A12: for n being Nat st 1 <= n & n <= (len p2) - 1 holds
p2 . n = (R . n) - (R . (n + 1)) ; :: thesis: p1 = p2
A13: dom p1 = Seg (len R) by A7, FINSEQ_1:def 3;

now :: thesis: for n being Nat st n in dom p1 holds
p1 . n = p2 . n

let n be Nat; :: thesis: ( n in dom p1 implies p1 . n = p2 . n )
set r = R . n;
assume A14: n in dom p1 ; :: thesis: p1 . n = p2 . n
then A15: 1 <= n by A13, FINSEQ_1:1;
A16: n <= len R by A13, A14, FINSEQ_1:1;

now :: thesis: ( ( n = len R & p1 . n = p2 . n ) or ( n <> len R & p1 . n = p2 . n ) )

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

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

hence p1 . n = p2 . n by A7, A8, A10, A11; :: thesis: verum

end;

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

set s = R . (n + 1);
n < len R by A16, A17, XXREAL_0:1;
then n + 1 <= len R by NAT_1:13;
then A18: n <= (len R) - 1 by XREAL_1:19;
then p1 . n = (R . n) - (R . (n + 1)) by A7, A9, A15;
hence p1 . n = p2 . n by A10, A12, A15, A18; :: thesis: verum

end;

end;

end;

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

end;

hence p1 = p2 by A7, A10, FINSEQ_2:9; :: thesis: verum