:: deftheorem defines Perm HILBERT3:def 6 :
for V being SetValuation
for P being Permutation of V
for p being Element of HP-WFF holds Perm (P,p) = (Perm P) . p;