deffunc H₂( Element of NAT ) -> Element of the carrier of X = (seq . $1) + x;
ex seq being sequence of X st
for n being Element of NAT holds seq . n = H₂(n) from FUNCT_2:sch 4();
hence ex b₁ being sequence of X st
for n being Element of NAT holds b₁ . n = (seq . n) + x ; :: thesis: verum