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

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