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

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, A7, A9, A10; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

hence p1 = p2 by A6, A9, FINSEQ_2:9; :: thesis: verum