theorem Th35: :: ACKERMAN:35

for m being Nat holds arity ((AckermannSequence . m) * <:<*(2 proj 2)*>:>) = 2