let m be Nat; arity ((AckermannSequence . m) * <:<*(2 proj 2)*>:>) = 2
set p1 = 2 proj 2;
set g1 = <:<*(2 proj 2)*>:>;
set f2 = (AckermannSequence . m) * <:<*(2 proj 2)*>:>;
A1:
(AckermannSequence . m) * <:<*(2 proj 2)*>:> is Element of HFuncs NAT
by COMPUT_1:28;
A2:
m in NAT
by ORDINAL1:def 12;
dom AckermannSequence = NAT
by PARTFUN1:def 2;
then A3:
AckermannSequence . m in rng AckermannSequence
by A2, FUNCT_1:def 3;
2 proj 2 is Element of HFuncs NAT
by COMPUT_1:28;
then
<*(2 proj 2)*> is FinSequence of HFuncs NAT
by FINSEQ_1:74;
hence arity ((AckermannSequence . m) * <:<*(2 proj 2)*>:>) =
arity <*(2 proj 2)*>
by A1, A3, COMPUT_1:44
.=
arity (2 proj 2)
by COMPUT_1:43
.=
2
;
verum