:: deftheorem Def4 defines Permutation HILBERT3:def 4 :
for V being SetValuation
for b₂ being Function holds
( b₂ is Permutation of V iff ( dom b₂ = NAT & ( for n being Element of NAT holds b₂ . n is Permutation of (V . n) ) ) );