let x be object ; :: thesis: for f being Function st f is one-to-one & x in dom f holds
( x = (f ") . (f . x) & x = ((f ") * f) . x )
let f be Function; :: thesis: ( f is one-to-one & x in dom f implies ( x = (f ") . (f . x) & x = ((f ") * f) . x ) )
assume A1: f is one-to-one ; :: thesis: ( not x in dom f or ( x = (f ") . (f . x) & x = ((f ") * f) . x ) )
assume A2: x in dom f ; :: thesis: ( x = (f ") . (f . x) & x = ((f ") * f) . x )
hence x = (f ") . (f . x) by A1, Th31; :: thesis: x = ((f ") * f) . x
hence x = ((f ") * f) . x by A2, Th13; :: thesis: verum