let s, t be Real_Sequence; :: thesis: ( ( for n being Nat holds s . n = dist ((seq . n),x) ) & ( for n being Nat holds t . n = dist ((seq . n),x) ) implies s = t )

assume that

A2: for n being Nat holds s . n = dist ((seq . n),x) and

A3: for n being Nat holds t . n = dist ((seq . n),x) ; :: thesis: s = t

assume that

A2: for n being Nat holds s . n = dist ((seq . n),x) and

A3: for n being Nat holds t . n = dist ((seq . n),x) ; :: thesis: s = t

now :: thesis: for n being Element of NAT holds s . n = t . n

hence
s = t
by FUNCT_2:63; :: thesis: verumlet n be Element of NAT ; :: thesis: s . n = t . n

s . n = dist ((seq . n),x) by A2;

hence s . n = t . n by A3; :: thesis: verum

end;s . n = dist ((seq . n),x) by A2;

hence s . n = t . n by A3; :: thesis: verum