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 set ; :: according to FUNCT_1:def 8 :: 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 9;
A3: dom [:f,g:] = [:(dom f),(dom g):] by FUNCT_3:def 9;
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 set such that
A4: x11 in dom g and
A5: x12 in dom f and
A6: x1 = [x11,x12] by A2, ZFMISC_1:103;
assume x2 in dom [:g,f:] ; :: thesis: ( not [:g,f:] . x1 = [:g,f:] . x2 or x1 = x2 )
then consider x21, x22 being set such that
A7: x21 in dom g and
A8: x22 in dom f and
A9: x2 = [x21,x22] by A2, ZFMISC_1:103;
x1 in dom [:g,f:] by A2, A4, A5, A6, ZFMISC_1:106;
then A10: x1 in dom (~ [:f,g:]) by A2, A3, FUNCT_4:47;
x2 in dom [:g,f:] by A2, A7, A8, A9, ZFMISC_1:106;
then A11: x2 in dom (~ [:f,g:]) by A2, A3, FUNCT_4:47;
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 9;
A14: [:g,f:] . x21,x22 = [(g . x21),(f . x22)] by A7, A8, FUNCT_3:def 9;
then A15: f . x22 = f . x12 by A6, A9, A12, A13, ZFMISC_1:33;
A16: g . x11 = g . x21 by A6, A9, A12, A13, A14, ZFMISC_1:33;
(~ [:f,g:]) . [x11,x12] = (~ [:f,g:]) . x11,x12
.= [:f,g:] . x12,x11 by A6, A10, FUNCT_4:44
.= [(f . x22),(g . x21)] by A4, A5, A15, A16, FUNCT_3:def 9
.= [:f,g:] . x22,x21 by A7, A8, FUNCT_3:def 9
.= (~ [:f,g:]) . x21,x22 by A9, A11, FUNCT_4:44
.= (~ [:f,g:]) . [x21,x22] ;
hence x1 = x2 by A1, A6, A9, A10, A11, FUNCT_1:def 8; :: thesis: verum