let X be set ; :: thesis: for f being Function holds
( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y )
let f be Function; :: thesis: ( f is X -one-to-one iff for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y )
set g = f | X;
thus ( f is X -one-to-one implies for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y ) :: thesis: ( ( for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y ) implies f is X -one-to-one )

proof

assume f is X -one-to-one ; :: thesis: for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y
then B1: f | X is one-to-one by DefInj1;
let x, y be set ; :: thesis: ( x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y implies x = y )
assume x in (dom f) /\ X ; :: thesis: ( not y in (dom f) /\ X or not f . x = f . y or x = y )
then C3: x in dom (f | X) by RELAT_1:61;
assume y in (dom f) /\ X ; :: thesis: ( not f . x = f . y or x = y )
then C4: y in dom (f | X) by RELAT_1:61;
assume f . x = f . y ; :: thesis: x = y
then ( (f | X) . x = f . x & (f | X) . y = f . y & f . x = f . y ) by C3, C4, FUNCT_1:47;
hence x = y by B1, C3, C4, FUNCT_1:def 4; :: thesis: verum

end;

assume A1: for x, y being set st x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y holds
x = y ; :: thesis: f is X -one-to-one

now

let x, y be set ; :: thesis: ( x in dom (f | X) & y in dom (f | X) & (f | X) . x = (f | X) . y implies x = y )
assume B1: ( x in dom (f | X) & y in dom (f | X) & (f | X) . x = (f | X) . y ) ; :: thesis: x = y
then ( (f | X) . x = f . x & (f | X) . y = f . y & (f | X) . x = (f | X) . y ) by FUNCT_1:47;
then ( x in (dom f) /\ X & y in (dom f) /\ X & f . x = f . y ) by B1, RELAT_1:61;
hence x = y by A1; :: thesis: verum

end;

then f | X is one-to-one by FUNCT_1:def 4;
hence f is X -one-to-one by DefInj1; :: thesis: verum