deffunc H₂( Nat) -> Element of the carrier of X = (seq . $1) + x;
consider seq being sequence of X such that
A1: for n being Element of NAT holds seq . n = H₂(n) from FUNCT_2:sch 4();
take seq ; :: thesis: for n being Nat holds seq . n = (seq . n) + x
let n be Nat; :: thesis: seq . n = (seq . n) + x
n in NAT by ORDINAL1:def 12;
hence seq . n = (seq . n) + x by A1; :: thesis: verum