let A, B be non empty set ; 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; 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; for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P
let f be Function of A,B; ((P => Q) ") . f = ((Q ") * f) * P
reconsider h = f as Element of Funcs (A,B) by FUNCT_2:8;
reconsider g = ((Q ") * f) * P as Function of A,B ;
f in Funcs (A,B)
by FUNCT_2:8;
then A1: (((P => Q) ") ") . (((P => Q) ") . f) =
f
by FUNCT_2:26
.=
f * (id A)
by FUNCT_2:17
.=
f * (P * (P "))
by FUNCT_2:61
.=
(f * P) * (P ")
by RELAT_1:36
.=
(((id B) * f) * P) * (P ")
by FUNCT_2:17
.=
(((Q * (Q ")) * f) * P) * (P ")
by FUNCT_2:61
.=
((Q * ((Q ") * f)) * P) * (P ")
by RELAT_1:36
.=
(Q * (((Q ") * f) * P)) * (P ")
by RELAT_1:36
.=
(P => Q) . g
by Def1
.=
(((P => Q) ") ") . (((Q ") * f) * P)
by FUNCT_1:43
;
( ((P => Q) ") . h in Funcs (A,B) & g in Funcs (A,B) )
by FUNCT_2:8;
hence
((P => Q) ") . f = ((Q ") * f) * P
by A1, FUNCT_2:19; verum