let y be set ; :: thesis: for f being Function st f is one-to-one & y in rng f holds
( y = f . ((f " ) . y) & y = (f * (f " )) . y )
let f be Function; :: thesis: ( f is one-to-one & y in rng f implies ( y = f . ((f " ) . y) & y = (f * (f " )) . y ) )
assume A1: f is one-to-one ; :: thesis: ( not y in rng f or ( y = f . ((f " ) . y) & y = (f * (f " )) . y ) )
assume A2: y in rng f ; :: thesis: ( y = f . ((f " ) . y) & y = (f * (f " )) . y )
hence A3: y = f . ((f " ) . y) by A1, Th54; :: thesis: y = (f * (f " )) . y
rng f = dom (f " ) by A1, Th55;
hence y = (f * (f " )) . y by A2, A3, Th23; :: thesis: verum