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;
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; :: thesis: verum