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 Def1 ; :: thesis: verum