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 object ; :: according to FUNCT_1:def 4 :: thesis: for x2 being object st x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 holds
x1 = x2
let x2 be object ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) & (f | X) . x1 = (f | X) . x2 implies x1 = x2 )
assume that
A2: x1 in dom (f | X) and
A3: x2 in dom (f | X) ; :: thesis: ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 )
x1 in (dom f) /\ X by A2, RELAT_1:61;
then A4: x1 in dom f by XBOOLE_0:def 4;
x2 in (dom f) /\ X by A3, RELAT_1:61;
then A5: x2 in dom f by XBOOLE_0:def 4;
( (f | X) . x1 = f . x1 & (f | X) . x2 = f . x2 ) by A2, A3, Th46;
hence ( not (f | X) . x1 = (f | X) . x2 or x1 = x2 ) by A1, A4, A5; :: thesis: verum