let f be Function; :: thesis: ( ( for x being object st x in dom f holds
f is_one-to-one_at x ) iff f is one-to-one )
thus ( ( for x being object st x in dom f holds
f is_one-to-one_at x ) implies f is one-to-one ) :: thesis: ( f is one-to-one implies for x being object st x in dom f holds
f is_one-to-one_at x )
proof
assume A1: for x being object st x in dom f holds
f is_one-to-one_at x ; :: thesis: f is one-to-one
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: x1 in dom f and
A3: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
f is_one-to-one_at x1 by A1, A2;
hence x1 = x2 by A3, Th3; :: thesis: verum
end;
assume A4: f is one-to-one ; :: thesis: for x being object st x in dom f holds
f is_one-to-one_at x
let x be object ; :: thesis: ( x in dom f implies f is_one-to-one_at x )
assume A5: x in dom f ; :: thesis: f is_one-to-one_at x
then for z being object st z in dom f & x <> z holds
f . x <> f . z by A4;
hence f is_one-to-one_at x by A5, Th3; :: thesis: verum