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 A1: ( g = f | [:A, the carrier of T:] & f is continuous ) ; :: thesis: g is continuous

set TT = TopStruct(# the carrier of T, the topology of T #);

A2: [:(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: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 [: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 Th13;

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 Th13;

hence g is continuous by A1, A3, A2, TOPMETR:7; :: thesis: verum

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 A1: ( g = f | [:A, the carrier of T:] & f is continuous ) ; :: thesis: g is continuous

set TT = TopStruct(# the carrier of T, the topology of T #);

A2: [:(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: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 [: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 Th13;

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 Th13;

hence g is continuous by A1, A3, A2, TOPMETR:7; :: thesis: verum