let C, D be non empty set ; :: thesis: for c being Element of C

for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let c be Element of C; :: thesis: for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let d be Element of D; :: thesis: for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let f be PartFunc of C,D; :: thesis: ( f is one-to-one implies ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) )

A1: f " = f " ;

assume f is one-to-one ; :: thesis: ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

hence ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) by A1, FUNCT_1:32; :: thesis: verum

for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let c be Element of C; :: thesis: for d being Element of D

for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let d be Element of D; :: thesis: for f being PartFunc of C,D st f is one-to-one holds

( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

let f be PartFunc of C,D; :: thesis: ( f is one-to-one implies ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) )

A1: f " = f " ;

assume f is one-to-one ; :: thesis: ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) )

hence ( d in rng f & c = (f ") . d iff ( c in dom f & d = f . c ) ) by A1, FUNCT_1:32; :: thesis: verum