let S, T be non empty TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: ( g = f | X implies g is continuous )
assume A1: g = f | X ; :: thesis: g is continuous
set h = f | X;
dom f = the carrier of S by FUNCT_2:def 1;
then A2: dom (f | X) = X by RELAT_1:91;
A3: the carrier of (S | X) = X by PRE_TOPC:29;
rng (f | X) c= the carrier of T ;
then reconsider h = f | X as Function of (S | X),T by A2, A3, FUNCT_2:4;
h is continuous by TOPMETR:10;
hence g is continuous by A1, TOPMETR:9; :: thesis: verum