let S, T be non empty TopSpace; :: thesis: for T1, T2 being SubSpace of T
for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let T1, T2 be SubSpace of T; :: thesis: for p1, p2 being Point of T
for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let p1, p2 be Point of T; :: thesis: for f being Function of T1,S
for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let f be Function of T1,S; :: thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds
f +* g is continuous Function of T,S
let g be Function of T2,S; :: thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 implies f +* g is continuous Function of T,S )
assume A1: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous ) ; :: thesis: ( not f . p1 = g . p1 or not f . p2 = g . p2 or f +* g is continuous Function of T,S )
assume ( f . p1 = g . p1 & f . p2 = g . p2 ) ; :: thesis: f +* g is continuous Function of T,S
then f | {p1,p2} tolerates g | {p1,p2} by PARTFUN1:82;
hence f +* g is continuous Function of T,S by A1, Lm1; :: thesis: verum