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 ;
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 ;
Q is open by ;
then A10: f " Q is open by ;
f1 " P1 c= f " Q by ;
hence f1 " P1 is open by ; :: thesis: verum
end;
[#] (Y | P) <> {} ;
hence f1 is continuous by ; :: thesis: verum