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 ) )
( ( 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
;
FUNCT_1:def 4 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;
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;
( f . (a1,b1) = f . (a2,b2) implies ( a1 = a2 & b1 = b2 ) )
A3:
[a1,b1] in [:A,B:]
by ZFMISC_1:def 2;
[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, A3;
hence
(
f . (
a1,
b1)
= f . (
a2,
b2) implies (
a1 = a2 &
b1 = b2 ) )
by ZFMISC_1:27;
verum
end;
assume A4:
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 )
; f is one-to-one
let x, y be set ; FUNCT_1:def 4 ( 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
; ( not y in proj1 f or not f . x = f . y or x = y )
then consider a1, b1 being set such that
A5:
a1 in A
and
A6:
b1 in B
and
A7:
x = [a1,b1]
by ZFMISC_1:def 2;
assume
y in dom f
; ( not f . x = f . y or x = y )
then consider a2, b2 being set such that
A8:
a2 in A
and
A9:
b2 in B
and
A10:
y = [a2,b2]
by ZFMISC_1:def 2;
reconsider a1 = a1, a2 = a2 as Element of A by A5, A8;
reconsider b1 = b1, b2 = b2 as Element of B by A6, A9;
assume
f . x = f . y
; x = y
then A11:
f . (a1,b1) = f . (a2,b2)
by A7, A10;
then
a1 = a2
by A4;
hence
x = y
by A4, A7, A10, A11; verum