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