let X be TopStruct ; :: thesis: for Y being non empty TopStruct
for K0 being Subset of X
for f being Function of X,Y
for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
let Y be non empty TopStruct ; :: thesis: for K0 being Subset of X
for f being Function of X,Y
for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
let K0 be Subset of X; :: thesis: for f being Function of X,Y
for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
let f be Function of X,Y; :: thesis: for g being Function of (X | K0),Y st f is continuous & g = f | K0 holds
g is continuous
let g be Function of (X | K0),Y; :: thesis: ( f is continuous & g = f | K0 implies g is continuous )
assume that
A1: f is continuous and
A2: g = f | K0 ; :: thesis: g is continuous
A3: [#] Y <> {} ;
for G being Subset of Y st G is open holds
g " G is open hence g is continuous by A3, TOPS_2:43; :: thesis: verum