let A, B be non empty set ; :: thesis: for P being Permutation of A
for Q being Permutation of B holds (P => Q) " = (P " ) => (Q " )
let P be Permutation of A; :: thesis: for Q being Permutation of B holds (P => Q) " = (P " ) => (Q " )
let Q be Permutation of B; :: thesis: (P => Q) " = (P " ) => (Q " )

now

let f be Element of Funcs A,B; :: thesis: ((P => Q) " ) . f = ((P " ) => (Q " )) . f
thus ((P => Q) " ) . f = ((Q " ) * f) * P by Th26
.= ((Q " ) * f) * ((P " ) " ) by FUNCT_1:65
.= ((P " ) => (Q " )) . f by Def1 ; :: thesis: verum

end;

hence (P => Q) " = (P " ) => (Q " ) by FUNCT_2:113; :: thesis: verum