let X, Y be non empty TopSpace; :: thesis: for f being Function of X,Y

for P being non empty Subset of Y

for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let f be Function of X,Y; :: thesis: for P being non empty Subset of Y

for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let P be non empty Subset of Y; :: thesis: for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let f1 be Function of X,(Y | P); :: thesis: ( f = f1 & f is continuous implies f1 is continuous )

assume that

A1: f = f1 and

A2: f is continuous ; :: thesis: f1 is continuous

A3: [#] Y <> {} ;

A4: for P1 being Subset of (Y | P) st P1 is open holds

f1 " P1 is open

hence f1 is continuous by A4, TOPS_2:43; :: thesis: verum

for P being non empty Subset of Y

for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let f be Function of X,Y; :: thesis: for P being non empty Subset of Y

for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let P be non empty Subset of Y; :: thesis: for f1 being Function of X,(Y | P) st f = f1 & f is continuous holds

f1 is continuous

let f1 be Function of X,(Y | P); :: thesis: ( f = f1 & f is continuous implies f1 is continuous )

assume that

A1: f = f1 and

A2: f is continuous ; :: thesis: f1 is continuous

A3: [#] Y <> {} ;

A4: for P1 being Subset of (Y | P) st P1 is open holds

f1 " P1 is open

proof

[#] (Y | P) <> {}
;
let P1 be Subset of (Y | P); :: thesis: ( P1 is open implies f1 " P1 is open )

assume P1 is open ; :: thesis: f1 " P1 is open

then P1 in the topology of (Y | P) by PRE_TOPC:def 2;

then consider Q being Subset of Y such that

A5: Q in the topology of Y and

A6: P1 = Q /\ ([#] (Y | P)) by PRE_TOPC:def 4;

reconsider Q = Q as Subset of Y ;

A7: f " Q = f1 " ((rng f1) /\ Q) by A1, RELAT_1:133;

A8: [#] (Y | P) = P by PRE_TOPC:def 5;

then (rng f1) /\ Q c= P /\ Q by XBOOLE_1:26;

then A9: f1 " ((rng f1) /\ Q) c= f1 " P1 by A6, A8, RELAT_1:143;

Q is open by A5, PRE_TOPC:def 2;

then A10: f " Q is open by A3, A2, TOPS_2:43;

f1 " P1 c= f " Q by A1, A6, RELAT_1:143, XBOOLE_1:17;

hence f1 " P1 is open by A10, A7, A9, XBOOLE_0:def 10; :: thesis: verum

end;assume P1 is open ; :: thesis: f1 " P1 is open

then P1 in the topology of (Y | P) by PRE_TOPC:def 2;

then consider Q being Subset of Y such that

A5: Q in the topology of Y and

A6: P1 = Q /\ ([#] (Y | P)) by PRE_TOPC:def 4;

reconsider Q = Q as Subset of Y ;

A7: f " Q = f1 " ((rng f1) /\ Q) by A1, RELAT_1:133;

A8: [#] (Y | P) = P by PRE_TOPC:def 5;

then (rng f1) /\ Q c= P /\ Q by XBOOLE_1:26;

then A9: f1 " ((rng f1) /\ Q) c= f1 " P1 by A6, A8, RELAT_1:143;

Q is open by A5, PRE_TOPC:def 2;

then A10: f " Q is open by A3, A2, TOPS_2:43;

f1 " P1 c= f " Q by A1, A6, RELAT_1:143, XBOOLE_1:17;

hence f1 " P1 is open by A10, A7, A9, XBOOLE_0:def 10; :: thesis: verum

hence f1 is continuous by A4, TOPS_2:43; :: thesis: verum