let f be Function; :: thesis: for y being set st f is one-to-one & y in rng f holds
(f " ) . y = f <- y
let y be set ; :: 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 set such that
A3: ( x in dom f & f . x = y ) by A2, FUNCT_1:def 5;
f just_once_values y by A1, A2, Th10;
then x = f <- y by A3, Def3;
hence (f " ) . y = f <- y by A1, A3, FUNCT_1:54; :: thesis: verum