let D be non empty set ; :: thesis: for f being BinOp of D
for X being set holds
( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) )
let f be BinOp of D; :: thesis: for X being set holds
( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) )
A1: dom f = [:D,D:] by FUNCT_2:def 1;
let X be set ; :: thesis: ( f is [:X,D:] -one-to-one iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) )
thus ( f is [:X,D:] -one-to-one implies for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ) :: thesis: ( ( for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ) implies f is [:X,D:] -one-to-one )

proof

assume A2: f is [:X,D:] -one-to-one ; :: thesis: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 )
let x, y, d1, d2 be set ; :: thesis: ( x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) implies ( x = y & d1 = d2 ) )
assume A3: ( x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) ) ; :: thesis: ( x = y & d1 = d2 )
then ( [x,d1] in [:(X /\ D),(D /\ D):] & [y,d2] in [:(X /\ D),(D /\ D):] ) by ZFMISC_1:def 2;
then A4: ( [x,d1] in [:X,D:] /\ [:D,D:] & [y,d2] in [:X,D:] /\ [:D,D:] ) by ZFMISC_1:100;
[x,d1] = [y,d2] by A1, A2, A4, A3;
hence ( x = y & d1 = d2 ) by XTUPLE_0:1; :: thesis: verum

end;

assume A5: for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) ; :: thesis: f is [:X,D:] -one-to-one

now :: thesis: for x, y being set st x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y holds
x = y

let x, y be set ; :: thesis: ( x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y implies x = y )
assume A6: ( x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y ) ; :: thesis: x = y
then A7: ( x in [:(X /\ D),(D /\ D):] & y in [:(X /\ D),(D /\ D):] & f . x = f . y ) by ZFMISC_1:100, A1;
then consider x1, d1 being object such that
A8: ( x1 in X /\ D & d1 in D & x = [x1,d1] ) by ZFMISC_1:def 2;
consider x2, d2 being object such that
A9: ( x2 in X /\ D & d2 in D & y = [x2,d2] ) by ZFMISC_1:def 2, A7;
( x1 in X /\ D & x2 in X /\ D & d1 in D & d2 in D & f . (x1,d1) = f . (x2,d2) ) by A8, A9, A6;
then ( x1 = x2 & d1 = d2 ) by A5;
hence x = y by A8, A9; :: thesis: verum

end;

hence f is [:X,D:] -one-to-one ; :: thesis: verum