:: deftheorem Def5 defines Perm HILBERT3:def 5 :
for V being SetValuation
for P being Permutation of V
for b₃ being ManySortedFunction of SetVal V, SetVal V holds
( b₃ = Perm P iff ( b₃ . VERUM = id 1 & ( for n being Element of NAT holds b₃ . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b₃ . p & q9 = b₃ . q & b₃ . (p '&' q) = [:p9,q9:] & b₃ . (p => q) = p9 => q9 ) ) ) );