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

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