set g = f | {x};
per cases ( x in dom f or not x in dom f ) ;
suppose x in dom f ; :: thesis: for b1 being Function st b1 = f | {x} holds
b1 is one-to-one
then f | {x} = x .--> (f . x) by FUNCT_7:6;
hence for b1 being Function st b1 = f | {x} holds
b1 is one-to-one ; :: thesis: verum
end;
suppose not x in dom f ; :: thesis: for b1 being Function st b1 = f | {x} holds
b1 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 for b1 being Function st b1 = f | {x} holds
b1 is one-to-one ; :: thesis: verum
end;
end;