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 ;
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 ;
A16: n <= len R by ;
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 ;
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 ; :: thesis: verum