let S, T be non empty TopSpace; for X being Subset of S
for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let X be Subset of S; for Y being Subset of T
for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let Y be Subset of T; for f being continuous Function of S,T
for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let f be continuous Function of S,T; for g being Function of (S | X),(T | Y) st g = f | X holds
g is continuous
let g be Function of (S | X),(T | Y); ( g = f | X implies g is continuous )
assume A1:
g = f | X
; g is continuous
set h = f | X;
A2:
( the carrier of (S | X) = X & rng (f | X) c= the carrier of T )
by PRE_TOPC:8;
dom f = the carrier of S
by FUNCT_2:def 1;
then
dom (f | X) = X
by RELAT_1:62;
then reconsider h = f | X as Function of (S | X),T by A2, FUNCT_2:2;
h is continuous
by TOPMETR:7;
hence
g is continuous
by A1, TOPMETR:6; verum