let X, Y be set ; :: thesis: for f being PartFunc of X,Y st ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ) holds
f is one-to-one
let f be PartFunc of X,Y; :: thesis: ( ( for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ) implies f is one-to-one )
assume for x1, x2 being Element of X st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ; :: thesis: f is one-to-one
then for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2 ;
hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum