let A, B, C be non empty set ; :: thesis: for f being Function of A,(Funcs (B,C))
for g being Function of A,B
for P being Permutation of B
for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
let f be Function of A,(Funcs (B,C)); :: thesis: for g being Function of A,B
for P being Permutation of B
for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
let g be Function of A,B; :: thesis: for P being Permutation of B
for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
let P be Permutation of B; :: thesis: for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
let Q be Permutation of C; :: thesis: ((P => Q) * f) .. (P * g) = Q * (f .. g)
A1: dom ((P => Q) * f) = A by FUNCT_2:def 1;
A2: ( dom Q = C & rng (f .. g) c= C ) by Th20, FUNCT_2:def 1;
A3: dom f = A by FUNCT_2:def 1;
then dom (f .. g) = A by PRALG_1:def 17;
then A4: dom (Q * (f .. g)) = A by A2, RELAT_1:27;
for x being set st x in dom ((P => Q) * f) holds
(Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x)

proof

let x be set ; :: thesis: ( x in dom ((P => Q) * f) implies (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x) )
assume A5: x in dom ((P => Q) * f) ; :: thesis: (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x)
reconsider fx = f . x as Function of B,C by A1, A5, FUNCT_2:5, FUNCT_2:66;
g . x in B by A1, A5, FUNCT_2:5;
then A6: g . x in dom fx by FUNCT_2:def 1;
(P * g) . x in B by A1, A5, FUNCT_2:5;
then A7: (P * g) . x in dom (P ") by FUNCT_2:def 1;
thus (Q * (f .. g)) . x = Q . ((f .. g) . x) by A4, A1, A5, FUNCT_1:12
.= Q . (fx . (g . x)) by A3, A1, A5, PRALG_1:def 17
.= (Q * fx) . (g . x) by A6, FUNCT_1:13
.= (Q * fx) . (((id B) * g) . x) by FUNCT_2:17
.= (Q * fx) . ((((P ") * P) * g) . x) by FUNCT_2:61
.= (Q * fx) . (((P ") * (P * g)) . x) by RELAT_1:36
.= (Q * fx) . ((P ") . ((P * g) . x)) by A1, A5, FUNCT_2:15
.= ((Q * fx) * (P ")) . ((P * g) . x) by A7, FUNCT_1:13
.= ((P => Q) . fx) . ((P * g) . x) by Def1
.= (((P => Q) * f) . x) . ((P * g) . x) by A1, A5, FUNCT_2:15 ; :: thesis: verum

end;

hence ((P => Q) * f) .. (P * g) = Q * (f .. g) by A4, A1, PRALG_1:def 17; :: thesis: verum