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

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

hence
g is continuous
by A3, TOPS_2:43; :: thesis: verum
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;[#] (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