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 set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 ; :: thesis: x1 = x2
A4: dom [:f,f:] = [:(dom f),(dom f):] by FUNCT_3:def 9;
then A5: ( [x1,x1] in dom [:f,f:] & [x2,x2] in dom [:f,f:] ) by A2, ZFMISC_1:106;
then [:f,f:] . x1,x1 = [(f . x2),(f . x2)] by A3, A4, FUNCT_3:86
.= [:f,f:] . x2,x2 by A4, A5, FUNCT_3:86 ;
then [x1,x1] = [x2,x2] by A1, A5, FUNCT_1:def 8;
hence x1 = x2 by ZFMISC_1:33; :: thesis: verum