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 4 :: thesis: for b₁ being set holds
( not x1 in proj1 f or not b₁ in proj1 f or not f . x1 = f . b₁ or x1 = b₁ )
let x2 be set ; :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A1: x1 in dom f and
A2: x2 in dom f ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
( dom f <> {} implies ( x1 = x & x2 = x ) ) by A1, A2, TARSKI:def 1;
hence ( not f . x1 = f . x2 or x1 = x2 ) by A1; :: thesis: verum