let f be Function; :: thesis: ( f is one-to-one implies ~ f is one-to-one )
assume A1: f is one-to-one ; :: thesis: ~ f is one-to-one
let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in proj1 (~ f) or not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
consider X, Y being set such that
A2: dom (~ f) c= [:X,Y:] by FUNCT_4:45;
assume A3: x1 in dom (~ f) ; :: thesis: ( not x2 in proj1 (~ f) or not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
then consider x11, x12 being set such that
x11 in X and
x12 in Y and
A4: x1 = [x11,x12] by A2, ZFMISC_1:103;
assume A5: x2 in dom (~ f) ; :: thesis: ( not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
then consider x21, x22 being set such that
x21 in X and
x22 in Y and
A6: x2 = [x21,x22] by A2, ZFMISC_1:103;
assume A7: (~ f) . x1 = (~ f) . x2 ; :: thesis: x1 = x2
A8: [x12,x11] in dom f by A3, A4, FUNCT_4:43;
A9: [x22,x21] in dom f by A5, A6, FUNCT_4:43;
f . x12,x11 = (~ f) . x11,x12 by A3, A4, FUNCT_4:44
.= (~ f) . x21,x22 by A4, A6, A7
.= f . x22,x21 by A5, A6, FUNCT_4:44 ;
then A10: [x12,x11] = [x22,x21] by A1, A8, A9, FUNCT_1:def 8;
then x12 = x22 by ZFMISC_1:33;
hence x1 = x2 by A4, A6, A10, ZFMISC_1:33; :: thesis: verum