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 Z1: 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 C1: ( 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 C2: ( [x,d1] in [:X,D:] /\ [:D,D:] & [y,d2] in [:X,D:] /\ [:D,D:] ) by ZFMISC_1:100;
[x,d1] = [y,d2] by DefInj2, A1, Z1, C2, C1;
hence ( x = y & d1 = d2 ) by ZFMISC_1:27; :: thesis: verum

end;

assume B2: 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

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 Z1: ( x in [:X,D:] /\ (dom f) & y in [:X,D:] /\ (dom f) & f . x = f . y ) ; :: thesis: x = y
then C1: ( x in [:(X /\ D),(D /\ D):] & y in [:(X /\ D),(D /\ D):] & f . x = f . y ) by A1, ZFMISC_1:100;
then consider x1, d1 being set such that
C2: ( x1 in X /\ D & d1 in D & x = [x1,d1] ) by ZFMISC_1:def 2;
consider x2, d2 being set such that
C3: ( x2 in X /\ D & d2 in D & y = [x2,d2] ) by C1, ZFMISC_1:def 2;
( x1 in X /\ D & x2 in X /\ D & d1 in D & d2 in D & f . (x1,d1) = f . (x2,d2) ) by C2, C3, Z1;
then ( x1 = x2 & d1 = d2 ) by B2;
hence x = y by C2, C3; :: thesis: verum

end;

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