let f be Function; :: thesis: for y being object st f is one-to-one & y in rng f holds
(f ") . y = f <- y
let y be object ; :: thesis: ( f is one-to-one & y in rng f implies (f ") . y = f <- y )
assume that
A1: f is one-to-one and
A2: y in rng f ; :: thesis: (f ") . y = f <- y
consider x being object such that
A3: ( x in dom f & f . x = y ) by A2, FUNCT_1:def 3;
f just_once_values y by A1, A2, Th8;
then x = f <- y by A3, Def3;
hence (f ") . y = f <- y by A1, A3, FUNCT_1:32; :: thesis: verum