let f, g be Function; ( f is one-to-one & g is one-to-one implies (~ [:f,g:]) " = ~ ([:g,f:] ") )
assume that
A1:
f is one-to-one
and
A2:
g is one-to-one
; (~ [:f,g:]) " = ~ ([:g,f:] ")
A3:
[:g,f:] " = [:(g "),(f "):]
by A1, A2, Th6;
then A4:
dom ([:g,f:] ") = [:(dom (g ")),(dom (f ")):]
by FUNCT_3:def 8;
A5:
dom [:f,g:] = [:(dom f),(dom g):]
by FUNCT_3:def 8;
A6:
dom [:g,f:] = [:(dom g),(dom f):]
by FUNCT_3:def 8;
A7:
[:g,f:] is one-to-one
by A1, A2;
A8:
~ [:f,g:] is one-to-one
by Th8, A1, A2;
A9:
[:f,g:] " = [:(f "),(g "):]
by A1, A2, Th6;
A10: dom (~ ([:g,f:] ")) =
[:(dom (f ")),(dom (g ")):]
by A4, FUNCT_4:46
.=
dom [:(f "),(g "):]
by FUNCT_3:def 8
.=
rng [:f,g:]
by A1, A2, A9, FUNCT_1:32
.=
rng (~ [:f,g:])
by A5, FUNCT_4:47
;
now for y, x being object holds
( ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y implies ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) ) & ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) ) )let y,
x be
object ;
( ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y implies ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y ) ) & ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) ) )hereby ( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y implies ( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y ) )
assume that A11:
y in rng (~ [:f,g:])
and A12:
x = (~ ([:g,f:] ")) . y
;
( x in dom (~ [:f,g:]) & (~ [:f,g:]) . x = y )
y in rng [:f,g:]
by A5, A11, FUNCT_4:47;
then
y in [:(rng f),(rng g):]
by FUNCT_3:67;
then consider y1,
y2 being
object such that A13:
y1 in rng f
and A14:
y2 in rng g
and A15:
y = [y1,y2]
by ZFMISC_1:84;
set x1 =
(f ") . y1;
set x2 =
(g ") . y2;
A16:
y2 in dom (g ")
by A2, A14, FUNCT_1:32;
A17:
y1 in dom (f ")
by A1, A13, FUNCT_1:32;
then
[y2,y1] in dom ([:g,f:] ")
by A4, A16, ZFMISC_1:87;
then A18:
(~ ([:g,f:] ")) . (
y1,
y2) =
[:(g "),(f "):] . (
y2,
y1)
by A3, FUNCT_4:def 2
.=
[((g ") . y2),((f ") . y1)]
by A16, A17, FUNCT_3:def 8
;
A19:
y1 in dom (f ")
by A1, A13, FUNCT_1:32;
A20:
y2 in dom (g ")
by A2, A14, FUNCT_1:32;
A21:
(f ") . y1 in rng (f ")
by A19, FUNCT_1:def 3;
A22:
(g ") . y2 in rng (g ")
by A20, FUNCT_1:def 3;
A23:
(f ") . y1 in dom f
by A1, A21, FUNCT_1:33;
A24:
(g ") . y2 in dom g
by A2, A22, FUNCT_1:33;
then A25:
[((g ") . y2),((f ") . y1)] in dom [:g,f:]
by A6, A23, ZFMISC_1:87;
then A26:
[((g ") . y2),((f ") . y1)] in dom (~ [:f,g:])
by A5, A6, FUNCT_4:46;
thus
x in dom (~ [:f,g:])
by A5, A6, A12, A15, A18, A25, FUNCT_4:46;
(~ [:f,g:]) . x = yA27:
f . ((f ") . y1) = y1
by A1, A13, FUNCT_1:32;
A28:
g . ((g ") . y2) = y2
by A2, A14, FUNCT_1:32;
thus (~ [:f,g:]) . x =
(~ [:f,g:]) . (
((g ") . y2),
((f ") . y1))
by A12, A15, A18
.=
[:f,g:] . (
((f ") . y1),
((g ") . y2))
by A26, FUNCT_4:43
.=
y
by A15, A23, A24, A27, A28, FUNCT_3:def 8
;
verum
end; assume that A29:
x in dom (~ [:f,g:])
and A30:
(~ [:f,g:]) . x = y
;
( y in rng (~ [:f,g:]) & x = (~ ([:g,f:] ")) . y )thus
y in rng (~ [:f,g:])
by A29, A30, FUNCT_1:def 3;
x = (~ ([:g,f:] ")) . y
x in dom [:g,f:]
by A5, A6, A29, FUNCT_4:46;
then consider x1,
x2 being
object such that A31:
x1 in dom g
and A32:
x2 in dom f
and A33:
x = [x1,x2]
by A6, ZFMISC_1:84;
A34:
(~ [:f,g:]) . (
x1,
x2) =
[:f,g:] . (
x2,
x1)
by A29, A33, FUNCT_4:43
.=
[(f . x2),(g . x1)]
by A31, A32, FUNCT_3:def 8
;
A35:
g . x1 in rng g
by A31, FUNCT_1:def 3;
f . x2 in rng f
by A32, FUNCT_1:def 3;
then
[(g . x1),(f . x2)] in [:(rng g),(rng f):]
by A35, ZFMISC_1:87;
then
[(g . x1),(f . x2)] in rng [:g,f:]
by FUNCT_3:67;
then A36:
[(g . x1),(f . x2)] in dom ([:g,f:] ")
by A7, FUNCT_1:33;
[x1,x2] in dom [:g,f:]
by A6, A31, A32, ZFMISC_1:87;
hence x =
([:g,f:] ") . ([:g,f:] . (x1,x2))
by A1, A2, A33, FUNCT_1:34
.=
([:g,f:] ") . (
(g . x1),
(f . x2))
by A31, A32, FUNCT_3:def 8
.=
(~ ([:g,f:] ")) . (
(f . x2),
(g . x1))
by A36, FUNCT_4:def 2
.=
(~ ([:g,f:] ")) . y
by A30, A33, A34
;
verum end;
hence
(~ [:f,g:]) " = ~ ([:g,f:] ")
by A8, A10, FUNCT_1:32; verum