deffunc H2( Nat) -> object = dist ((seq . $1),x);
consider s being Real_Sequence such that
A1:
for n being Nat holds s . n = H2(n)
from SEQ_1:sch 1();
take
s
; for n being Nat holds s . n = dist ((seq . n),x)
thus
for n being Nat holds s . n = dist ((seq . n),x)
by A1; verum