let x, y be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f is one-to-one & x in dom f & y in dom f & f /. x = f /. y holds
x = y
let f be PartFunc of C,D; :: thesis: ( f is one-to-one & x in dom f & y in dom f & f /. x = f /. y implies x = y )
assume that
A1: f is one-to-one and
A2: x in dom f and
A3: y in dom f ; :: thesis: ( not f /. x = f /. y or x = y )
assume f /. x = f /. y ; :: thesis: x = y
then f . x = f /. y by A2, PARTFUN1:def 6
.= f . y by A3, PARTFUN1:def 6 ;
hence x = y by A1, A2, A3; :: thesis: verum