deffunc H₁( Nat) -> object = dist ((S . $1),(T . $1));
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),(T . n))
thus for n being Nat holds seq . n = dist ((S . n),(T . n)) by A1; :: thesis: verum