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 Q = C
by FUNCT_2:def 1;
A2:
rng (f .. g) c= C
by Th20;
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 A1, A2, RELAT_1:46;
A5:
dom ((P => Q) * f) = A
by FUNCT_2:def 1;
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 A6:
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 A5, A6, FUNCT_2:7, FUNCT_2:121;
g . x in B
by A5, A6, FUNCT_2:7;
then A7:
g . x in dom fx
by FUNCT_2:def 1;
(P * g) . x in B
by A5, A6, FUNCT_2:7;
then A8:
(P * g) . x in dom (P " )
by FUNCT_2:def 1;
thus (Q * (f .. g)) . x =
Q . ((f .. g) . x)
by A4, A5, A6, FUNCT_1:22
.=
Q . (fx . (g . x))
by A3, A5, A6, PRALG_1:def 17
.=
(Q * fx) . (g . x)
by A7, FUNCT_1:23
.=
(Q * fx) . (((id B) * g) . x)
by FUNCT_2:23
.=
(Q * fx) . ((((P " ) * P) * g) . x)
by FUNCT_2:88
.=
(Q * fx) . (((P " ) * (P * g)) . x)
by RELAT_1:55
.=
(Q * fx) . ((P " ) . ((P * g) . x))
by A5, A6, FUNCT_2:21
.=
((Q * fx) * (P " )) . ((P * g) . x)
by A8, FUNCT_1:23
.=
((P => Q) . fx) . ((P * g) . x)
by Def1
.=
(((P => Q) * f) . x) . ((P * g) . x)
by A5, A6, FUNCT_2:21
;
:: thesis: verum
end;
hence
((P => Q) * f) .. (P * g) = Q * (f .. g)
by A4, A5, PRALG_1:def 17; :: thesis: verum