set g = f | {x};

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: f | {x} is one-to-one

then f | {x} = x .--> (f . x) by FUNCT_7:6;
hence f | {x} is one-to-one ; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f | {x} is one-to-one

then reconsider gg = f | {x} as empty Function by RELAT_1:152, ZFMISC_1:50;
gg is one-to-one ;
hence f | {x} is one-to-one ; :: thesis: verum

end;

end;