let f be Function; :: thesis: for x being object holds
( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )
let x be object ; :: thesis: ( f is_one-to-one_at x iff ( x in dom f & f just_once_values f . x ) )
thus ( f is_one-to-one_at x implies ( x in dom f & f just_once_values f . x ) ) :: thesis: ( x in dom f & f just_once_values f . x implies f is_one-to-one_at x )
proof
assume A1: f is_one-to-one_at x ; :: thesis: ( x in dom f & f just_once_values f . x )
hence x in dom f by Th1; :: thesis: f just_once_values f . x
{x} = f " {(f . x)} by A1, Th2;
hence f just_once_values f . x by Th6; :: thesis: verum
end;
assume that
A2: x in dom f and
A3: f just_once_values f . x ; :: thesis: f is_one-to-one_at x
consider z being object such that
A4: f " {(f . x)} = {z} by A3, Th6;
f . x in {(f . x)} by TARSKI:def 1;
then x in {z} by A2, A4, FUNCT_1:def 7;
then x = z by TARSKI:def 1;
hence f is_one-to-one_at x by A2, A4, Th2; :: thesis: verum