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

proof

let G be Subset of Y; :: thesis: ( G is open implies g " G is open )
[#] (X | K0) = K0 by PRE_TOPC:def 5;
then A4: g " G = ([#] (X | K0)) /\ (f " G) by A2, FUNCT_1:70;
assume G is open ; :: thesis: g " G is open
then f " G is open by A3, A1, TOPS_2:43;
hence g " G is open by A4, TOPS_2:24; :: thesis: verum

end;

hence g is continuous by A3, TOPS_2:43; :: thesis: verum