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 object ; :: according to FUNCT_1:def 4 :: 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:44;
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 object such that
x11 in X and
x12 in Y and
A4: x1 = [x11,x12] by A2, ZFMISC_1:84;
assume A5: x2 in dom (~ f) ; :: thesis: ( not (~ f) . x1 = (~ f) . x2 or x1 = x2 )
then consider x21, x22 being object such that
x21 in X and
x22 in Y and
A6: x2 = [x21,x22] by A2, ZFMISC_1:84;
assume A7: (~ f) . x1 = (~ f) . x2 ; :: thesis: x1 = x2
A8: [x12,x11] in dom f by A3, A4, FUNCT_4:42;
A9: [x22,x21] in dom f by A5, A6, FUNCT_4:42;
f . (x12,x11) = (~ f) . (x11,x12) by A3, A4, FUNCT_4:43
.= (~ f) . (x21,x22) by A4, A6, A7
.= f . (x22,x21) by A5, A6, FUNCT_4:43 ;
then A10: [x12,x11] = [x22,x21] by A1, A8, A9;
then x12 = x22 by XTUPLE_0:1;
hence x1 = x2 by A4, A6, A10, XTUPLE_0:1; :: thesis: verum