let m be Nat; :: thesis: dom2tuple (AckermannFunction m) = AckermannSequence . m

per cases ( m = 0 or ex a being Nat st m = a + 1 ) by NAT_1:6;

suppose m = 0 ; :: thesis: dom2tuple (AckermannFunction m) = AckermannSequence . m

hence dom2tuple (AckermannFunction m) = AckermannSequence . m by Def13, Th37; :: thesis: verum

end;

suppose ex a being Nat st m = a + 1 ; :: thesis: dom2tuple (AckermannFunction m) = AckermannSequence . m

then consider a being Nat such that
A1: m = a + 1 ;
dom2tuple H₂(a + 1) = primrec ((0 const H₁(a,1)),((AckermannSequence . a) * <:<*(2 proj 2)*>:>),1) by Th38;
hence dom2tuple (AckermannFunction m) = AckermannSequence . m by A1, Def13; :: thesis: verum

end;

end;