let p, q be Element of HP-WFF ; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ((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 ; :: thesis: verum