let A, B, C be TopSpace; :: thesis: for f being Function of A,C st f is continuous & C is SubSpace of B holds
for h being Function of A,B st h = f holds
h is continuous
let f be Function of A,C; :: thesis: ( f is continuous & C is SubSpace of B implies for h being Function of A,B st h = f holds
h is continuous )
assume that
A1: f is continuous and
A2: C is SubSpace of B ; :: thesis: for h being Function of A,B st h = f holds
h is continuous
let h be Function of A,B; :: thesis: ( h = f implies h is continuous )
assume A3: h = f ; :: thesis: h is continuous
for P being Subset of B st P is closed holds
h " P is closed
proof
let P be Subset of B; :: thesis: ( P is closed implies h " P is closed )
assume A4: P is closed ; :: thesis: h " P is closed
A5: rng h c= the carrier of C by A3, RELAT_1:def 19;
A6: h " P = h " ((rng h) /\ P) by RELAT_1:133
.= h " (((rng h) /\ ([#] C)) /\ P) by A5, XBOOLE_1:28
.= h " ((rng h) /\ (([#] C) /\ P)) by XBOOLE_1:16
.= h " (P /\ ([#] C)) by RELAT_1:133 ;
reconsider C = C as SubSpace of B by A2;
reconsider Q = P /\ ([#] C) as Subset of C ;
Q is closed by A4, Th13;
hence h " P is closed by A1, A3, A6; :: thesis: verum
end;
hence h is continuous ; :: thesis: verum