let f, g be Function; :: thesis: ( ~ [:f,g:] is one-to-one implies [:g,f:] is one-to-one )
assume A1: ~ [:f,g:] is one-to-one ; :: thesis: [:g,f:] is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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:] ; :: thesis: ( 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:] ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum