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:18;
then A1: ( X | (A \/ (A ` )) = TopStruct(# the carrier of X,the topology of X #) & TopStruct(# the carrier of Y,the topology of Y #) = TopStruct(# the carrier of Y,the topology of Y #) ) by TSEP_1:100;
A misses A ` by XBOOLE_1:79;
then f +* g is continuous Function of (X | (A \/ (A ` ))),Y by Th15;
hence f +* g is continuous Function of X,Y by A1, YELLOW12:36; :: thesis: verum