deffunc H₁( object , object ) -> object = [((L_ $2) \/ (sqrt (x,(L_ $2),(R_ $2)))),(((R_ $2) \/ (sqrt (x,(L_ $2),(L_ $2)))) \/ (sqrt (x,(R_ $2),(R_ $2))))];
consider f being Function such that
A1: ( dom f = NAT & f . 0 = x0 & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 11();
take f ; :: thesis:
thus ( dom f = omega & f . 0 = x0 ) by A1; :: thesis:
let k be Nat; :: thesis:
thus f . k is pair :: thesis:

proof

per cases ;

suppose k = 0 ; :: thesis:

hence f . k is pair by A1; :: thesis:

end;

suppose k > 0 ; :: thesis:

then reconsider k1 = k - 1 as Nat by NAT_1:20;
f . (k1 + 1) = H₁(k1,f . k1) by A1;
hence f . k is pair ; :: thesis:

end;

end;

end;

f . (k + 1) = H₁(k,f . k) by A1;
hence ( (f . (k + 1)) `1 = (L_ (f . k)) \/ (sqrt (x,(L_ (f . k)),(R_ (f . k)))) & (f . (k + 1)) `2 = ((R_ (f . k)) \/ (sqrt (x,(L_ (f . k)),(L_ (f . k))))) \/ (sqrt (x,(R_ (f . k)),(R_ (f . k)))) ) ; :: thesis: