let y be object ; :: 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, Th31; :: thesis: y = (f * (f ")) . y
rng f = dom (f ") by A1, Th32;
hence y = (f * (f ")) . y by A2, A3, Th13; :: thesis: verum