let D, C 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

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

end;

hence f is one-to-one by FUNCT_1:def 8; :: thesis: verum