deffunc H_{1}( Nat) -> set = (S . $1) - x;

consider S being Real_Sequence such that

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

take S ; :: thesis: for n being Nat holds S . n = (S . n) - x

let n be Nat; :: thesis: S . n = (S . n) - x

thus S . n = (S . 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 = (S . n) - x

let n be Nat; :: thesis: S . n = (S . n) - x

thus S . n = (S . n) - x by A1; :: thesis: verum