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