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

( 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_{1} being a_neighborhood of f . x ex b_{2} being a_neighborhood of x st f .: b_{2} c= b_{1}

let G be a_neighborhood of f . x; :: thesis: ex b_{1} being a_neighborhood of x st f .: b_{1} c= G

f is_continuous_at x by A1;

hence ex b_{1} being a_neighborhood of x st f .: b_{1} c= G
; :: thesis: verum

end;let G be a_neighborhood of f . x; :: thesis: ex b

f is_continuous_at x by A1;

hence ex b