let f be Function; :: thesis: for y being object st f just_once_values y holds
f is_one-to-one_at f <- y
let y be object ; :: 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

A2: now :: thesis: for x being object st x in dom f & x <> f <- y holds
f . x <> f . (f <- y)

let x be object ; :: 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;

f <- y in dom f by A1, Def3;
hence f is_one-to-one_at f <- y by A2, Th3; :: thesis: verum