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 )
A1: [#] Y <> {} ;
assume A2: ( f is continuous & g = f | K0 ) ; :: thesis: g is continuous
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 )
assume G is open ; :: thesis: g " G is open
then A3: f " G is open by A1, A2, TOPS_2:55;
[#] (X | K0) = K0 by PRE_TOPC:def 10;
then g " G = ([#] (X | K0)) /\ (f " G) by A2, FUNCT_1:139;
hence g " G is open by A3, TOPS_2:32; :: thesis: verum

end;

hence g is continuous by A1, TOPS_2:55; :: thesis: verum