theorem Th38: :: HILBERT3:39

for p, q being Element of HP-WFF
for V being SetValuation
for P being Permutation of V
for f, g being Function of (SetVal (V,p)),(SetVal (V,q)) st f = (Perm (P,(p => q))) . g holds
(Perm (P,q)) * g = f * (Perm (P,p))