deffunc H_{2}( Nat) -> object = dist ((seq . $1),x);

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H_{2}(n)
from SEQ_1:sch 1();

take s ; :: thesis: 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; :: thesis: verum

consider s being Real_Sequence such that

A1: for n being Nat holds s . n = H

take s ; :: thesis: 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; :: thesis: verum