let x, Y be set ; :: thesis: for f being PartFunc of {x},Y holds f is one-to-one
let f be PartFunc of {x},Y; :: thesis: f is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for b₁ being set holds
( not x1 in dom f or not b₁ in dom f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then ( ( dom f <> {} implies ( x1 = x & x2 = x ) ) & dom f <> {} ) by TARSKI:def 1;
hence ( not f . x1 = f . x2 or x1 = x2 ) ; :: thesis: verum