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 ;
A3: dom f = A by FUNCT_2:def 1;
a4: dom g = A by FUNCT_2:def 1;
B2: dom (f .. g) = (dom f) /\ (dom g) by PRALG_1:def 19
.= A by A3, a4 ;
then A4: dom (Q * (f .. g)) = A by ;
set gg = Q * (f .. g);
dom (P * g) = A by FUNCT_2:def 1;
then S1: dom (Q * (f .. g)) = (dom ((P => Q) * f)) /\ (dom (P * g)) by A4, A1;
for x being set st x in dom (Q * (f .. g)) holds
(Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x)
proof
let x be set ; :: thesis: ( x in dom (Q * (f .. g)) implies (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x) )
assume a5: x in dom (Q * (f .. g)) ; :: thesis: (Q * (f .. g)) . x = (((P => Q) * f) . x) . ((P * g) . x)
A5: x in dom ((P => Q) * f) by a5, A4, A1;
reconsider fx = f . x as Function of B,C by ;
g . x in B by ;
then A6: g . x in dom fx by FUNCT_2:def 1;
(P * g) . x in B by ;
then A7: (P * g) . x in dom (P ") by FUNCT_2:def 1;
B1: x in dom (f .. g) by B2, A5, A1;
thus (Q * (f .. g)) . x = Q . ((f .. g) . x) by
.= Q . (fx . (g . x)) by
.= (Q * fx) . (g . x) by
.= (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
.= ((Q * fx) * (P ")) . ((P * g) . x) by
.= ((P => Q) . fx) . ((P * g) . x) by Def1
.= (((P => Q) * f) . x) . ((P * g) . x) by ; :: thesis: verum
end;
hence ((P => Q) * f) .. (P * g) = Q * (f .. g) by ; :: thesis: verum