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

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