let f be Function; :: thesis: for y being set st f just_once_values y holds
f is_one-to-one_at f <- y
let y be set ; :: thesis: ( f just_once_values y implies f is_one-to-one_at f <- y )
assume A1: f just_once_values y ; :: thesis: f is_one-to-one_at f <- y
then A2: f <- y in dom f by Def3;

now

let x be set ; :: thesis: ( x in dom f & x <> f <- y implies f . x <> f . (f <- y) )
assume ( x in dom f & x <> f <- y ) ; :: thesis: f . x <> f . (f <- y)
then f . x <> y by A1, Def3;
hence f . x <> f . (f <- y) by A1, Def3; :: thesis: verum

end;

hence f is_one-to-one_at f <- y by A2, Th4; :: thesis: verum