let S, T be TopSpace; :: thesis: for Y being non empty TopSpace
for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let Y be non empty TopSpace; :: thesis: for A being Subset of T
for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let A be Subset of T; :: thesis: for f being Function of [:S,T:],Y
for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let f be Function of [:S,T:],Y; :: thesis: for g being Function of [:S,(T | A):],Y st g = f | [: the carrier of S,A:] & f is continuous holds
g is continuous
let g be Function of [:S,(T | A):],Y; :: thesis: ( g = f | [: the carrier of S,A:] & f is continuous implies g is continuous )
assume A1: ( g = f | [: the carrier of S,A:] & f is continuous ) ; :: thesis: g is continuous
set SS = TopStruct(# the carrier of S, the topology of S #);
A2: [:TopStruct(# the carrier of S, the topology of S #),(T | A):] = [:(TopStruct(# the carrier of S, the topology of S #) | ([#] TopStruct(# the carrier of S, the topology of S #))),(T | A):] by TSEP_1:3
.= [:TopStruct(# the carrier of S, the topology of S #),T:] | [:([#] TopStruct(# the carrier of S, the topology of S #)),A:] by BORSUK_3:22 ;
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 Th13;
then A3: TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),T:], the topology of [:TopStruct(# the carrier of S, the topology of S #),T:] #) = TopStruct(# the carrier of [:S,T:], the topology of [:S,T:] #) by Th13;
TopStruct(# the carrier of [:TopStruct(# the carrier of S, the topology of S #),(T | A):], the topology of [:TopStruct(# the carrier of S, the topology of S #),(T | A):] #) = TopStruct(# the carrier of [:S,(T | A):], the topology of [:S,(T | A):] #) by Th13;
hence g is continuous by A1, A3, A2, TOPMETR:7; :: thesis: verum