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 ")

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

hence
(P => Q) " = (P ") => (Q ")
; :: thesis: verumlet 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;thus ((P => Q) ") . f = ((Q ") * f) * P by Th25

.= ((Q ") * f) * ((P ") ") by FUNCT_1:43

.= ((P ") => (Q ")) . f by Def1 ; :: thesis: verum