:: deftheorem Def4 defines PFBrt HEYTING3:def 4 :
for n, k being Nat
for b₃ being Element of Fin (PFuncs (NAT,{k})) holds
( b₃ = PFBrt (n,k) iff for x being object holds
( x in b₃ iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) );