let f, g be Function; ( ~ [:f,g:] is one-to-one implies [:g,f:] is one-to-one )
assume A1:
~ [:f,g:] is one-to-one
; [:g,f:] is one-to-one
let x1, x2 be object ; FUNCT_1:def 4 ( not x1 in proj1 [:g,f:] or not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
A2:
dom [:g,f:] = [:(dom g),(dom f):]
by FUNCT_3:def 8;
A3:
dom [:f,g:] = [:(dom f),(dom g):]
by FUNCT_3:def 8;
assume
x1 in dom [:g,f:]
; ( not x2 in proj1 [:g,f:] or not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
then consider x11, x12 being object such that
A4:
x11 in dom g
and
A5:
x12 in dom f
and
A6:
x1 = [x11,x12]
by A2, ZFMISC_1:84;
assume
x2 in dom [:g,f:]
; ( not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
then consider x21, x22 being object such that
A7:
x21 in dom g
and
A8:
x22 in dom f
and
A9:
x2 = [x21,x22]
by A2, ZFMISC_1:84;
x1 in dom [:g,f:]
by A2, A4, A5, A6, ZFMISC_1:87;
then A10:
x1 in dom (~ [:f,g:])
by A2, A3, FUNCT_4:46;
x2 in dom [:g,f:]
by A2, A7, A8, A9, ZFMISC_1:87;
then A11:
x2 in dom (~ [:f,g:])
by A2, A3, FUNCT_4:46;
assume A12:
[:g,f:] . x1 = [:g,f:] . x2
; x1 = x2
A13:
[:g,f:] . (x11,x12) = [(g . x11),(f . x12)]
by A4, A5, FUNCT_3:def 8;
A14:
[:g,f:] . (x21,x22) = [(g . x21),(f . x22)]
by A7, A8, FUNCT_3:def 8;
then A15:
f . x22 = f . x12
by A6, A9, A12, A13, XTUPLE_0:1;
A16:
g . x11 = g . x21
by A6, A9, A12, A13, A14, XTUPLE_0:1;
(~ [:f,g:]) . [x11,x12] =
(~ [:f,g:]) . (x11,x12)
.=
[:f,g:] . (x12,x11)
by A6, A10, FUNCT_4:43
.=
[(f . x22),(g . x21)]
by A4, A5, A15, A16, FUNCT_3:def 8
.=
[:f,g:] . (x22,x21)
by A7, A8, FUNCT_3:def 8
.=
(~ [:f,g:]) . (x21,x22)
by A9, A11, FUNCT_4:43
.=
(~ [:f,g:]) . [x21,x22]
;
hence
x1 = x2
by A1, A6, A9, A10, A11; verum