let p, q be Element of HP-WFF ; :: thesis: for V being SetValuation
for P being Permutation of V
for f, g being Function of (SetVal V,p),(SetVal V,q) st f = (Perm P,(p => q)) . g holds
(Perm P,q) * g = f * (Perm P,p)
let V be SetValuation; :: thesis: for P being Permutation of V
for f, g being Function of (SetVal V,p),(SetVal V,q) st f = (Perm P,(p => q)) . g holds
(Perm P,q) * g = f * (Perm P,p)
let P be Permutation of V; :: thesis: for f, g being Function of (SetVal V,p),(SetVal V,q) st f = (Perm P,(p => q)) . g holds
(Perm P,q) * g = f * (Perm P,p)
let f, g be Function of (SetVal V,p),(SetVal V,q); :: thesis: ( f = (Perm P,(p => q)) . g implies (Perm P,q) * g = f * (Perm P,p) )
assume A1: f = (Perm P,(p => q)) . g ; :: thesis: (Perm P,q) * g = f * (Perm P,p)
thus (Perm P,q) * g = ((Perm P,q) * g) * (id (SetVal V,p)) by FUNCT_2:23
.= ((Perm P,q) * g) * (((Perm P,p) " ) * (Perm P,p)) by FUNCT_2:88
.= (((Perm P,q) * g) * ((Perm P,p) " )) * (Perm P,p) by RELAT_1:55
.= f * (Perm P,p) by A1, Th37 ; :: thesis: verum