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

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

hence
f is one-to-one
; :: thesis: verumx = 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;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