set f = H₃(H₂( 0 ));
set s = 1 succ 1;
set D = 1 -tuples_on (dom H₂( 0 ));
dom H₃(H₂( 0 )) = 1 -tuples_on (dom H₂( 0 )) by Def4;
then A1: dom H₃(H₂( 0 )) = 1 -tuples_on NAT by FUNCT_2:def 1;
hence dom H₃(H₂( 0 )) = dom (1 succ 1) by COMPUT_1:def 7; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (dom2tuple (AckermannFunction 0)) or (dom2tuple (AckermannFunction 0)) . b₁ = (1 succ 1) . b₁ )
let x be object ; :: thesis: ( not x in dom (dom2tuple (AckermannFunction 0)) or (dom2tuple (AckermannFunction 0)) . x = (1 succ 1) . x )
assume A2: x in dom H₃(H₂( 0 )) ; :: thesis: (dom2tuple (AckermannFunction 0)) . x = (1 succ 1) . x
then consider a being set such that
A3: a in NAT and
A4: x = <*a*> by A1, FINSEQ_2:135;
reconsider a = a as Element of NAT by A3;
a in dom H₂( 0 ) by A3, FUNCT_2:def 1;
hence H₃(H₂( 0 )) . x = H₂( 0 ) . a by A4, Def4
.= H₁( 0 ,a) by Def3
.= (<*a*> . 1) + 1 by Def1
.= (1 succ 1) . x by A1, A2, A4, COMPUT_1:def 7 ;
:: thesis: verum