set f = H₂(m);
let a be Nat; :: according to SEQM_3:def 1 :: thesis: for b₁ being set holds
( not a in dom (AckermannFunction m) or not b₁ in dom (AckermannFunction m) or b₁ <= a or not (AckermannFunction m) . b₁ <= (AckermannFunction m) . a )
let b be Nat; :: thesis: ( not a in dom (AckermannFunction m) or not b in dom (AckermannFunction m) or b <= a or not (AckermannFunction m) . b <= (AckermannFunction m) . a )
( H₂(m) . a = H₁(m,a) & H₂(m) . b = H₁(m,b) ) by Def3;
hence ( not a in dom (AckermannFunction m) or not b in dom (AckermannFunction m) or b <= a or not (AckermannFunction m) . b <= (AckermannFunction m) . a ) by Th18; :: thesis: verum