let f, g, h be Function; ~ (f * [:g,h:]) = (~ f) * [:h,g:]
A1:
now for x being object holds
( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being object st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st
( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )let x be
object ;
( ( x in dom ((~ f) * [:h,g:]) implies ex z1, y1 being object st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) ) ) & ( ex y, z being object st
( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) ) )hereby ( ex y, z being object st
( x = [z,y] & [y,z] in dom (f * [:g,h:]) ) implies x in dom ((~ f) * [:h,g:]) )
assume A2:
x in dom ((~ f) * [:h,g:])
;
ex z1, y1 being object st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )then
x in dom [:h,g:]
by FUNCT_1:11;
then
x in [:(dom h),(dom g):]
by FUNCT_3:def 8;
then consider y1,
z1 being
object such that A3:
(
y1 in dom h &
z1 in dom g )
and A4:
x = [y1,z1]
by ZFMISC_1:84;
A5:
(
[:h,g:] . (
y1,
z1)
= [(h . y1),(g . z1)] &
[:g,h:] . (
z1,
y1)
= [(g . z1),(h . y1)] )
by A3, FUNCT_3:def 8;
[:h,g:] . (
y1,
z1)
in dom (~ f)
by A2, A4, FUNCT_1:11;
then A6:
[:g,h:] . (
z1,
y1)
in dom f
by A5, FUNCT_4:42;
take z1 =
z1;
ex y1 being object st
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )take y1 =
y1;
( x = [y1,z1] & [z1,y1] in dom (f * [:g,h:]) )thus
x = [y1,z1]
by A4;
[z1,y1] in dom (f * [:g,h:])
dom [:g,h:] = [:(dom g),(dom h):]
by FUNCT_3:def 8;
then
[z1,y1] in dom [:g,h:]
by A3, ZFMISC_1:87;
hence
[z1,y1] in dom (f * [:g,h:])
by A6, FUNCT_1:11;
verum
end; given y,
z being
object such that A7:
x = [z,y]
and A8:
[y,z] in dom (f * [:g,h:])
;
x in dom ((~ f) * [:h,g:])A9:
[:g,h:] . (
y,
z)
in dom f
by A8, FUNCT_1:11;
A10:
dom [:g,h:] = [:(dom g),(dom h):]
by FUNCT_3:def 8;
[y,z] in dom [:g,h:]
by A8, FUNCT_1:11;
then A11:
(
y in dom g &
z in dom h )
by A10, ZFMISC_1:87;
then
(
[:g,h:] . (
y,
z)
= [(g . y),(h . z)] &
[:h,g:] . (
z,
y)
= [(h . z),(g . y)] )
by FUNCT_3:def 8;
then A12:
[:h,g:] . x in dom (~ f)
by A7, A9, FUNCT_4:42;
dom [:h,g:] = [:(dom h),(dom g):]
by FUNCT_3:def 8;
then
x in dom [:h,g:]
by A7, A11, ZFMISC_1:87;
hence
x in dom ((~ f) * [:h,g:])
by A12, FUNCT_1:11;
verum end;
now for y, z being object st [y,z] in dom (f * [:g,h:]) holds
((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)let y,
z be
object ;
( [y,z] in dom (f * [:g,h:]) implies ((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z) )assume A13:
[y,z] in dom (f * [:g,h:])
;
((~ f) * [:h,g:]) . (z,y) = (f * [:g,h:]) . (y,z)then
[y,z] in dom [:g,h:]
by FUNCT_1:11;
then
[y,z] in [:(dom g),(dom h):]
by FUNCT_3:def 8;
then A14:
(
y in dom g &
z in dom h )
by ZFMISC_1:87;
[:g,h:] . (
y,
z)
in dom f
by A13, FUNCT_1:11;
then A15:
[(g . y),(h . z)] in dom f
by A14, FUNCT_3:def 8;
[z,y] in [:(dom h),(dom g):]
by A14, ZFMISC_1:87;
then
[z,y] in dom [:h,g:]
by FUNCT_3:def 8;
hence ((~ f) * [:h,g:]) . (
z,
y) =
(~ f) . ([:h,g:] . (z,y))
by FUNCT_1:13
.=
(~ f) . (
(h . z),
(g . y))
by A14, FUNCT_3:def 8
.=
f . (
(g . y),
(h . z))
by A15, FUNCT_4:def 2
.=
f . ([:g,h:] . (y,z))
by A14, FUNCT_3:def 8
.=
(f * [:g,h:]) . (
y,
z)
by A13, FUNCT_1:12
;
verum end;
hence
~ (f * [:g,h:]) = (~ f) * [:h,g:]
by A1, FUNCT_4:def 2; verum