theorem Th36: :: HILBERT3:37

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)) ")