let p, q be 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))
let V be 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))
let P be 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))
let g be Function of (SetVal (V,p)),(SetVal (V,q)); ((Perm (P,(p => q))) ") . g = (((Perm (P,q)) ") * g) * (Perm (P,p))
thus ((Perm (P,(p => q))) ") . g =
(((Perm (P,p)) => (Perm (P,q))) ") . g
by Th35
.=
(((Perm (P,q)) ") * g) * (Perm (P,p))
by Th25
; verum