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