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 :: thesis: for f being Element of Funcs (A,B) holds ((P => Q) ") . f = ((P ") => (Q ")) . f

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

end;

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