let m be Nat; :: thesis: (AckermannFunction (m + 1)) . 0 = (AckermannFunction m) . 1
thus H₂(m + 1) . 0 = H₁(m + 1, 0 ) by Def3
.= H₁(m,1) by Th6
.= H₂(m) . 1 by Def3 ; :: thesis: verum