let X be TopSpace; for Y being non empty TopSpace
for A being open closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y
let Y be non empty TopSpace; for A being open closed Subset of X
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y
let A be open closed Subset of X; for f being continuous Function of (X | A),Y
for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y
let f be continuous Function of (X | A),Y; for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y
let g be continuous Function of (X | (A `)),Y; f +* g is continuous Function of X,Y
A \/ (A `) = [#] X
by PRE_TOPC:2;
then A1:
X | (A \/ (A `)) = TopStruct(# the carrier of X, the topology of X #)
by TSEP_1:93;
A misses A `
by XBOOLE_1:79;
then A2:
f +* g is continuous Function of (X | (A \/ (A `))),Y
by Th11;
TopStruct(# the carrier of Y, the topology of Y #) = TopStruct(# the carrier of Y, the topology of Y #)
;
hence
f +* g is continuous Function of X,Y
by A2, A1, YELLOW12:36; verum