let A, B, C be non empty set ; 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)); 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; 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; for Q being Permutation of C holds ((P => Q) * f) .. (P * g) = Q * (f .. g)
let Q be Permutation of C; ((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
let x be
set ;
( 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))
;
(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
;
verum
end;
hence
((P => Q) * f) .. (P * g) = Q * (f .. g)
by S1, PRALG_1:def 19; verum