let seq1, seq2 be Functional_Sequence of REAL ,REAL ; ( seq1 . 0 = f & ( for n being Nat holds seq1 . (n + 1) = cD (seq1 . n),h ) & seq2 . 0 = f & ( for n being Nat holds seq2 . (n + 1) = cD (seq2 . n),h ) implies seq1 = seq2 )
assume that
A3:
seq1 . 0 = f
and
A4:
for n being Nat holds seq1 . (n + 1) = cD (seq1 . n),h
and
A5:
seq2 . 0 = f
and
A6:
for n being Nat holds seq2 . (n + 1) = cD (seq2 . n),h
; seq1 = seq2
defpred S1[ Nat] means seq1 . $1 = seq2 . $1;
A7:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
thus seq1 . (k + 1) =
cD (seq1 . k),
h
by A4
.=
seq2 . (k + 1)
by A6, A8
;
verum
end;
A9:
S1[ 0 ]
by A3, A5;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A9, A7);
hence
seq1 = seq2
by FUNCT_2:113; verum