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