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 Th36
.= ((Perm P,q) * g) * ((Perm P,p) " ) by Def1 ; :: thesis: verum