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;

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

hence
p1 = p2
by A7, A10, FINSEQ_2:9; :: thesis: verump1 . 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;

end;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 ) )end;

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