let S, T be TopSpace; :: thesis: for Y being non empty TopSpace
for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A,the carrier of T:] & f is continuous holds
g is continuous
let Y be non empty TopSpace; :: thesis: for A being Subset of S
for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A,the carrier of T:] & f is continuous holds
g is continuous
let A be Subset of S; :: thesis: for f being Function of [:S,T:],Y
for g being Function of [:(S | A),T:],Y st g = f | [:A,the carrier of T:] & f is continuous holds
g is continuous
let f be Function of [:S,T:],Y; :: thesis: for g being Function of [:(S | A),T:],Y st g = f | [:A,the carrier of T:] & f is continuous holds
g is continuous
let g be Function of [:(S | A),T:],Y; :: thesis: ( g = f | [:A,the carrier of T:] & f is continuous implies g is continuous )
assume that
A1: g = f | [:A,the carrier of T:] and
A2: f is continuous ; :: thesis: g is continuous
set TT = TopStruct(# the carrier of T,the topology of T #);
TopStruct(# the carrier of [:S,T:],the topology of [:S,T:] #) = [:TopStruct(# the carrier of S,the topology of S #),TopStruct(# the carrier of T,the topology of T #):] by Th14;
then A6: TopStruct(# the carrier of [:S,TopStruct(# the carrier of T,the topology of T #):],the topology of [:S,TopStruct(# the carrier of T,the topology of T #):] #) = TopStruct(# the carrier of [:S,T:],the topology of [:S,T:] #) by Th14;
A7: [:(S | A),TopStruct(# the carrier of T,the topology of T #):] = [:(S | A),(TopStruct(# the carrier of T,the topology of T #) | ([#] TopStruct(# the carrier of T,the topology of T #))):] by TSEP_1:3
.= [:S,TopStruct(# the carrier of T,the topology of T #):] | [:A,([#] TopStruct(# the carrier of T,the topology of T #)):] by BORSUK_3:26 ;
TopStruct(# the carrier of [:(S | A),TopStruct(# the carrier of T,the topology of T #):],the topology of [:(S | A),TopStruct(# the carrier of T,the topology of T #):] #) = TopStruct(# the carrier of [:(S | A),T:],the topology of [:(S | A),T:] #) by Th14;
hence g is continuous by A1, A2, A6, A7, TOPMETR:10; :: thesis: verum