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