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