thus (1,2)->(1,?,2) f in PrimRec by Th88; :: according to COMPUT_1:def 16 :: thesis: (1,2)->(1,?,2) f is 3 -ary
thus arity ((1,2)->(1,?,2) f) = 3 by Def24; :: according to COMPUT_1:def 21 :: thesis: verum