let seq1, seq2 be Real_Sequence; :: thesis: ( ( for n being Nat holds seq1 . n = dist ((S . n),(T . n)) ) & ( for n being Nat holds seq2 . n = dist ((S . n),(T . n)) ) implies seq1 = seq2 )
assume that
A2: for n being Nat holds seq1 . n = dist ((S . n),(T . n)) and
A3: for n being Nat holds seq2 . n = dist ((S . n),(T . n)) ; :: thesis: seq1 = seq2

now :: thesis: for n being Element of NAT holds seq1 . n = seq2 . n

let n be Element of NAT ; :: thesis: seq1 . n = seq2 . n
seq1 . n = dist ((S . n),(T . n)) by A2;
hence seq1 . n = seq2 . n by A3; :: thesis: verum

end;

hence seq1 = seq2 by FUNCT_2:63; :: thesis: verum