let X be set ; :: thesis: for f being Function st f is one-to-one holds
f | X is one-to-one
let f be Function; :: thesis: ( f is one-to-one implies f | X is one-to-one )
assume A1: f is one-to-one ; :: thesis: f | X is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for x2 being set st x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 holds
x1 = x2
let x2 be set ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 implies x1 = x2 )
assume A2: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 )
then ( x1 in (dom f) /\ X & x2 in (dom f) /\ X ) by RELAT_1:90;
then ( x1 in dom f & x2 in dom f & (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by A2, Th70, XBOOLE_0:def 4;
hence ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 ) by A1, Def8; :: thesis: verum