let X be TopSpace; :: thesis: for Y being non empty TopSpace
for A, B being closed Subset of X st A misses B holds
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y
let Y be non empty TopSpace; :: thesis: for A, B being closed Subset of X st A misses B holds
for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y
let A, B be closed Subset of X; :: thesis: ( A misses B implies for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y )
assume A1: A misses B ; :: thesis: for f being continuous Function of (X | A),Y
for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y
let f be continuous Function of (X | A),Y; :: thesis: for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y
let g be continuous Function of (X | B),Y; :: thesis: f +* g is continuous Function of (X | (A \/ B)),Y
the carrier of (X | B) = B by PRE_TOPC:8;
then A2: dom g = B by FUNCT_2:def 1;
the carrier of (X | A) = A by PRE_TOPC:8;
then dom f = A by FUNCT_2:def 1;
hence f +* g is continuous Function of (X | (A \/ B)),Y by A2, A1, Th10, PARTFUN1:56; :: thesis: verum