deffunc H₁( Nat, set ) -> set = f . ($2,(x . ($1 + 2)));
consider f1 being Function such that
A1: ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = H₁(n,f1 . n) ) ) from NAT_1:sch 11();
take f1 ; :: thesis: ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = f . ((f1 . n),(x . (n + 2))) ) )
thus ( dom f1 = NAT & f1 . 0 = x . 1 & ( for n being Nat holds f1 . (n + 1) = f . ((f1 . n),(x . (n + 2))) ) ) by A1; :: thesis: verum