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:11;
reconsider g = ((Q ") * f) * P as Function of A,B ;
f in Funcs (A,B) by FUNCT_2:11;
then A1: (((P => Q) ") ") . (((P => Q) ") . f) = f by FUNCT_2:32
.= f * (id A) by FUNCT_2:23
.= f * (P * (P ")) by FUNCT_2:88
.= (f * P) * (P ") by RELAT_1:55
.= (((id B) * f) * P) * (P ") by FUNCT_2:23
.= (((Q * (Q ")) * f) * P) * (P ") by FUNCT_2:88
.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:55
.= (Q * (((Q ") * f) * P)) * (P ") by RELAT_1:55
.= (P => Q) . g by Def1
.= (((P => Q) ") ") . (((Q ") * f) * P) by FUNCT_1:65 ;
( ((P => Q) ") . h in Funcs (A,B) & g in Funcs (A,B) ) by FUNCT_2:11;
hence ((P => Q) ") . f = ((Q ") * f) * P by A1, FUNCT_2:25; :: thesis: verum