theorem :: HILBERT3:34

for n being Element of NAT
for V being SetValuation
for P being Permutation of V holds Perm (P,(prop n)) = P . n by Def5;