let x be object ; :: thesis: for Y being set
for f being PartFunc of {x},Y holds f is one-to-one
let 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, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom 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