:: deftheorem Def2 defines PFArt HEYTING3:def 2 :
for n, k being Nat
for b₃ being Element of PFuncs (NAT,{k}) holds
( b₃ = PFArt (n,k) iff for x being object holds
( x in b₃ iff ( ex m being odd Element of NAT st
( m <= 2 * n & [m,k] = x ) or [(2 * n),k] = x ) ) );