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;

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 A2, RELAT_1:27;

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)

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;

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 A2, RELAT_1:27;

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

hence
((P => Q) * f) .. (P * g) = Q * (f .. g)
by S1, PRALG_1:def 19; :: thesis: verum
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 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;

B1: x in dom (f .. g) by B2, A5, A1;

thus (Q * (f .. g)) . x = Q . ((f .. g) . x) by A4, A1, A5, FUNCT_1:12

.= Q . (fx . (g . x)) by B1, PRALG_1:def 19

.= (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;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 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;

B1: x in dom (f .. g) by B2, A5, A1;

thus (Q * (f .. g)) . x = Q . ((f .. g) . x) by A4, A1, A5, FUNCT_1:12

.= Q . (fx . (g . x)) by B1, PRALG_1:def 19

.= (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