let X be TopSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: verum