let s1, s2 be ExtREAL_sequence; ( s1 . 0 = s . 0 & ( for n being Nat holds s1 . (n + 1) = (s1 . n) + (s . (n + 1)) ) & s2 . 0 = s . 0 & ( for n being Nat holds s2 . (n + 1) = (s2 . n) + (s . (n + 1)) ) implies s1 = s2 )
assume that
A2:
s1 . 0 = s . 0
and
A3:
for n being Nat holds s1 . (n + 1) = (s1 . n) + (s . (n + 1))
and
A4:
s2 . 0 = s . 0
and
A5:
for n being Nat holds s2 . (n + 1) = (s2 . n) + (s . (n + 1))
; s1 = s2
defpred S1[ Nat] means s1 . $1 = s2 . $1;
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume
s1 . k = s2 . k
;
S1[k + 1]
hence s1 . (k + 1) =
(s2 . k) + (s . (k + 1))
by A3
.=
s2 . (k + 1)
by A5
;
verum
end;
A7:
S1[ 0 ]
by A2, A4;
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A6);
hence
s1 = s2
; verum