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 b1 being a_neighborhood of f . x ex b2 being a_neighborhood of x st f .: b2 c= b1
let G be a_neighborhood of f . x; :: thesis: ex b1 being a_neighborhood of x st f .: b1 c= G
f is_continuous_at x by A1;
hence ex b1 being a_neighborhood of x st f .: b1 c= G ; :: thesis: verum
end;