deffunc H₁( Element of NAT ) -> Element of NAT = IFGT ($1,(n1 + 1),($1 + n2),$1);
ex f being sequence of NAT st
for n being Element of NAT holds f . n = H₁(n) from FUNCT_2:sch 4();
hence ex b₁ being sequence of NAT st
for n being Element of NAT holds b₁ . n = IFGT (n,(n1 + 1),(n + n2),n) ; :: thesis: verum