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 | A) = A & the carrier of (X | B) = B & the carrier of (X | (A \/ B)) = A \/ B ) by PRE_TOPC:29;
then ( dom f = A & dom g = B ) by FUNCT_2:def 1;
hence f +* g is continuous Function of (X | (A \/ B)),Y by A1, Th14, PARTFUN1:138; :: thesis: verum