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

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