let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) holds
f is one-to-one
let f be PartFunc of C,D; :: thesis: ( ( for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ) implies f is one-to-one )
assume A1: for c1, c2 being Element of C st c1 in dom f & c2 in dom f & f /. c1 = f /. c2 holds
c1 = c2 ; :: thesis: f is one-to-one

now :: thesis: for x, y being object st x in dom f & y in dom f & f . x = f . y holds
x = y

let x, y be object ; :: thesis: ( x in dom f & y in dom f & f . x = f . y implies x = y )
assume that
A2: x in dom f and
A3: y in dom f and
A4: f . x = f . y ; :: thesis: x = y
reconsider y1 = y as Element of C by A3;
reconsider x1 = x as Element of C by A2;
f /. x1 = f . y1 by A2, A4, PARTFUN1:def 6;
then f /. x1 = f /. y1 by A3, PARTFUN1:def 6;
hence x = y by A1, A2, A3; :: thesis: verum

end;

hence f is one-to-one ; :: thesis: verum