let seq1, seq2 be Real_Sequence; ( ( for n being Nat holds seq1 . n = dist ((S . n),x) ) & ( for n being Nat holds seq2 . n = dist ((S . n),x) ) implies seq1 = seq2 )
assume that
A2:
for n being Nat holds seq1 . n = dist ((S . n),x)
and
A3:
for n being Nat holds seq2 . n = dist ((S . n),x)
; seq1 = seq2
hence
seq1 = seq2
by FUNCT_2:63; verum