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

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 = ||.(seq . n).||

thus for n being Nat holds s . n = ||.(seq . n).|| 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 = ||.(seq . n).||

thus for n being Nat holds s . n = ||.(seq . n).|| by A1; :: thesis: verum