let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y holds
( f is continuous iff for x being Point of X holds f is_continuous_at x )
let f be Function of X,Y; :: thesis: ( f is continuous iff for x being Point of X holds f is_continuous_at x )
thus ( f is continuous implies for x being Point of X holds f is_continuous_at x ) ; :: thesis: ( ( for x being Point of X holds f is_continuous_at x ) implies f is continuous )
assume A1: for x being Point of X holds f is_continuous_at x ; :: thesis: f is continuous
thus f is continuous :: thesis: verum

proof

let x be Point of X; :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of f . x ex b₂ being a_neighborhood of x st f .: b₂ c= b₁
let G be a_neighborhood of f . x; :: thesis: ex b₁ being a_neighborhood of x st f .: b₁ c= G
f is_continuous_at x by A1;
hence ex b₁ being a_neighborhood of x st f .: b₁ c= G ; :: thesis: verum

end;