let A, B be non empty set ; :: thesis: for P being Permutation of A

for Q being Permutation of B

for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let P be Permutation of A; :: thesis: for Q being Permutation of B

for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let Q be Permutation of B; :: thesis: for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let f be Function of A,B; :: thesis: ((P => Q) ") . f = ((Q ") * f) * P

reconsider h = f as Element of Funcs (A,B) by FUNCT_2:8;

reconsider g = ((Q ") * f) * P as Function of A,B ;

f in Funcs (A,B) by FUNCT_2:8;

then A1: (((P => Q) ") ") . (((P => Q) ") . f) = f by FUNCT_2:26

.= f * (id A) by FUNCT_2:17

.= f * (P * (P ")) by FUNCT_2:61

.= (f * P) * (P ") by RELAT_1:36

.= (((id B) * f) * P) * (P ") by FUNCT_2:17

.= (((Q * (Q ")) * f) * P) * (P ") by FUNCT_2:61

.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36

.= (Q * (((Q ") * f) * P)) * (P ") by RELAT_1:36

.= (P => Q) . g by Def1

.= (((P => Q) ") ") . (((Q ") * f) * P) by FUNCT_1:43 ;

( ((P => Q) ") . h in Funcs (A,B) & g in Funcs (A,B) ) by FUNCT_2:8;

hence ((P => Q) ") . f = ((Q ") * f) * P by A1, FUNCT_2:19; :: thesis: verum

for Q being Permutation of B

for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let P be Permutation of A; :: thesis: for Q being Permutation of B

for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let Q be Permutation of B; :: thesis: for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P

let f be Function of A,B; :: thesis: ((P => Q) ") . f = ((Q ") * f) * P

reconsider h = f as Element of Funcs (A,B) by FUNCT_2:8;

reconsider g = ((Q ") * f) * P as Function of A,B ;

f in Funcs (A,B) by FUNCT_2:8;

then A1: (((P => Q) ") ") . (((P => Q) ") . f) = f by FUNCT_2:26

.= f * (id A) by FUNCT_2:17

.= f * (P * (P ")) by FUNCT_2:61

.= (f * P) * (P ") by RELAT_1:36

.= (((id B) * f) * P) * (P ") by FUNCT_2:17

.= (((Q * (Q ")) * f) * P) * (P ") by FUNCT_2:61

.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36

.= (Q * (((Q ") * f) * P)) * (P ") by RELAT_1:36

.= (P => Q) . g by Def1

.= (((P => Q) ") ") . (((Q ") * f) * P) by FUNCT_1:43 ;

( ((P => Q) ") . h in Funcs (A,B) & g in Funcs (A,B) ) by FUNCT_2:8;

hence ((P => Q) ") . f = ((Q ") * f) * P by A1, FUNCT_2:19; :: thesis: verum