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:17
.= ((Perm (P,q)) * g) * (((Perm (P,p)) ") * (Perm (P,p))) by FUNCT_2:61
.= (((Perm (P,q)) * g) * ((Perm (P,p)) ")) * (Perm (P,p)) by RELAT_1:36
.= f * (Perm (P,p)) by A1, Th36 ; :: thesis: verum