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