let X, Y be non empty TopSpace; :: thesis: for Y0 being non empty SubSpace of Y
for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let Y0 be non empty SubSpace of Y; :: thesis: for f being Function of X,Y
for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let f be Function of X,Y; :: thesis: for g being Function of X,Y0 st f = g & f is continuous holds
g is continuous
let g be Function of X,Y0; :: thesis: ( f = g & f is continuous implies g is continuous )
assume that
A1: f = g and
A2: f is continuous ; :: thesis: g is continuous
let W be Point of X; :: according to BORSUK_1:def 1 :: thesis: for b₁ being a_neighborhood of g . W ex b₂ being a_neighborhood of W st g .: b₂ c= b₁
let G be a_neighborhood of g . W; :: thesis: ex b₁ being a_neighborhood of W st g .: b₁ c= G
consider V being Subset of Y0 such that
A3: V is open and
A4: V c= G and
A5: g . W in V by CONNSP_2:6;
( g . W in [#] Y0 & [#] Y0 c= [#] Y ) by PRE_TOPC:def 4;
then reconsider p = g . W as Point of Y ;
consider C being Subset of Y such that
A6: C is open and
A7: C /\ ([#] Y0) = V by A3, TOPS_2:24;
p in C by A5, A7, XBOOLE_0:def 4;
then C is a_neighborhood of p by A6, CONNSP_2:3;
then consider H being a_neighborhood of W such that
A8: f .: H c= C by A1, A2;
take H ; :: thesis: g .: H c= G
g .: H c= V by A1, A7, A8, XBOOLE_1:19;
hence g .: H c= G by A4; :: thesis: verum