let m, n be Nat; (AckermannFunction (m + 1)) . (n + 1) = (AckermannFunction m) . ((AckermannFunction (m + 1)) . n)
A1:
H1(m + 1,n) = H2(m + 1) . n
by Def3;
thus H2(m + 1) . (n + 1) =
H1(m + 1,n + 1)
by Def3
.=
H1(m,H1(m + 1,n))
by Th7
.=
H2(m) . (H2(m + 1) . n)
by A1, Def3
; verum