deffunc H₁( object , object ) -> object = [(((L_ $2) \/ (divset ((L_ $2),x,(R_ x),Inv))) \/ (divset ((R_ $2),x,(L_ x),Inv))),(((R_ $2) \/ (divset ((L_ $2),x,(L_ x),Inv))) \/ (divset ((R_ $2),x,(R_ x),Inv)))];
consider f being Function such that
A1: ( dom f = NAT & f . 0 = 1_No & ( 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 = 1_No ) 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)) \/ (divset ((L_ (f . k)),x,(R_ x),Inv))) \/ (divset ((R_ (f . k)),x,(L_ x),Inv)) & (f . (k + 1)) `2 = ((R_ (f . k)) \/ (divset ((L_ (f . k)),x,(L_ x),Inv))) \/ (divset ((R_ (f . k)),x,(R_ x),Inv)) ) ; :: thesis: