let m be Nat; :: thesis: dom2tuple (AckermannFunction (m + 1)) = primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)
set f = H₃(H₂(m + 1));
set c = primrec ((0 const H₁(m,1)),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1);
set D = 1 -tuples_on (dom H₂(m + 1));
A1: dom H₃(H₂(m + 1)) = 1 -tuples_on (dom H₂(m + 1)) by Def4;
then A2: dom H₃(H₂(m + 1)) = 1 -tuples_on NAT by FUNCT_2:def 1;
set f1 = 0 const H₁(m,1);
set f2 = (AckermannSequence . m) * <:<*(2 proj 2)*>:>;
arity ((AckermannSequence . m) * <:<*(2 proj 2)*>:>) = 0 + 2 by Th35;
then dom (primrec ((0 const H₁(m,1)),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) = ((arity (0 const H₁(m,1))) + 1) -tuples_on NAT by COMPUT_1:57;
hence dom H₃(H₂(m + 1)) = dom (primrec ((0 const H₁(m,1)),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) by A1, FUNCT_2:def 1; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (dom2tuple (AckermannFunction (m + 1))) or (dom2tuple (AckermannFunction (m + 1))) . b₁ = (primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) . b₁ )
let x be object ; :: thesis: ( not x in dom (dom2tuple (AckermannFunction (m + 1))) or (dom2tuple (AckermannFunction (m + 1))) . x = (primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) . x )
assume x in dom H₃(H₂(m + 1)) ; :: thesis: (dom2tuple (AckermannFunction (m + 1))) . x = (primrec ((0 const (Ackermann (m,1))),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) . x
then consider n being set such that
A3: n in NAT and
A4: x = <*n*> by A2, FINSEQ_2:135;
reconsider n = n as Element of NAT by A3;
dom H₂(m + 1) = NAT by FUNCT_2:def 1;
hence H₃(H₂(m + 1)) . x = H₂(m + 1) . n by A4, Def4
.= H₁(m + 1,n) by Def3
.= (AckermannSequence . (m + 1)) . <*n*> by Th36
.= (primrec ((0 const H₁(m,1)),((AckermannSequence . m) * <:<*(2 proj 2)*>:>),1)) . x by A4, Def13 ;
:: thesis: verum