let f be Function; :: thesis: ( [:f,f:] is one-to-one implies f is one-to-one )
assume A1: [:f,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 )
assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f . x1 = f . x2 ; :: thesis: x1 = x2
A5: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def 8;
then A6: [x1,x1] in dom [:f,f:] by A2, ZFMISC_1:87;
A7: [x2,x2] in dom [:f,f:] by A3, A5, ZFMISC_1:87;
[:f,f:] . (x1,x1) = [(f . x2),(f . x2)] by A4, A5, A6, FUNCT_3:65
.= [:f,f:] . (x2,x2) by A5, A7, FUNCT_3:65 ;
then [x1,x1] = [x2,x2] by A1, A6, A7;
hence x1 = x2 by XTUPLE_0:1; :: thesis: verum