:: deftheorem defines =>> HEYTING2:def 3 :
for V being set
for C being finite set
for A, B being Element of Fin (PFuncs (V,C)) holds A =>> B = (PFuncs (V,C)) /\ { (union { ((f . i) \ i) where i is Element of PFuncs (V,C) : i in A } ) where f is Element of PFuncs (A,B) : dom f = A } ;