let f be Function; :: thesis: for x being object st f is_one-to-one_at x holds
f <- (f . x) = x
let x be object ; :: thesis: ( f is_one-to-one_at x implies f <- (f . x) = x )
assume f is_one-to-one_at x ; :: thesis: f <- (f . x) = x
then ( x in dom f & f just_once_values f . x ) by Th9;
hence f <- (f . x) = x by Def3; :: thesis: verum