theorem Th37: :: HILBERT3:38

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