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

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