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;
A1: ((P => Q) " ) . h in Funcs A,B ;
reconsider g = ((Q " ) * f) * P as Function of A,B ;
A2: g in Funcs A,B by FUNCT_2:11;
f in Funcs A,B by FUNCT_2:11;
then (((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 ;
hence ((P => Q) " ) . f = ((Q " ) * f) * P by A1, A2, FUNCT_2:25; :: thesis: verum