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

proof

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;

[#] (Y | P) <> {} ;
hence f1 is continuous by A4, TOPS_2:43; :: thesis: verum