let seq1, seq2 be sequence of X; ( seq1 . 0 = 0. X & ( for k being Nat holds seq1 . (k + 1) = seq . k ) & seq2 . 0 = 0. X & ( for k being Nat holds seq2 . (k + 1) = seq . k ) implies seq1 = seq2 )
assume that
A2:
seq1 . 0 = 0. X
and
A3:
for n being Nat holds seq1 . (n + 1) = seq . n
and
A4:
seq2 . 0 = 0. X
and
A5:
for n being Nat holds seq2 . (n + 1) = seq . n
; seq1 = seq2
defpred S1[ Nat] means seq1 . $1 = seq2 . $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
seq1 . k = seq2 . k
;
S1[k + 1]
thus seq1 . (k + 1) =
seq . k
by A3
.=
seq2 . (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);
then
for n being Element of NAT holds S1[n]
;
hence
seq1 = seq2
by FUNCT_2:63; verum