A1: dom f = [:A,B:] by FUNCT_2:def 1;
thus ( f is one-to-one implies for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 ) ) :: thesis: ( ( for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 ) ) implies f is one-to-one )

proof

assume A2: for x, y being set st x in dom f & y in dom f & f . x = f . y holds
x = y ; :: according to FUNCT_1:def 8 :: thesis: for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 )
let a1, a2 be Element of A; :: thesis: for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 )
let b1, b2 be Element of B; :: thesis: ( f . a1,b1 = f . a2,b2 implies ( a1 = a2 & b1 = b2 ) )
( f . a1,b1 = f . [a1,b1] & f . a2,b2 = f . [a2,b2] & [a1,b1] in [:A,B:] & [a2,b2] in [:A,B:] ) by ZFMISC_1:def 2;
then ( f . a1,b1 = f . a2,b2 implies [a1,b1] = [a2,b2] ) by A1, A2;
hence ( f . a1,b1 = f . a2,b2 implies ( a1 = a2 & b1 = b2 ) ) by ZFMISC_1:33; :: thesis: verum

end;

assume A3: for a1, a2 being Element of A
for b1, b2 being Element of B st f . a1,b1 = f . a2,b2 holds
( a1 = a2 & b1 = b2 ) ; :: thesis: f is one-to-one
let x, y be set ; :: according to FUNCT_1:def 8 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume x in dom f ; :: thesis: ( not y in proj1 f or not f . x = f . y or x = y )
then consider a1, b1 being set such that
A4: ( a1 in A & b1 in B & x = [a1,b1] ) by ZFMISC_1:def 2;
assume y in dom f ; :: thesis: ( not f . x = f . y or x = y )
then consider a2, b2 being set such that
A5: ( a2 in A & b2 in B & y = [a2,b2] ) by ZFMISC_1:def 2;
reconsider a1 = a1, a2 = a2 as Element of A by A4, A5;
reconsider b1 = b1, b2 = b2 as Element of B by A4, A5;
assume f . x = f . y ; :: thesis: x = y
then f . a1,b1 = f . a2,b2 by A4, A5;
then ( a1 = a2 & b1 = b2 ) by A3;
hence x = y by A4, A5; :: thesis: verum