environ
vocabularies HIDDEN, PRE_TOPC, SUBSET_1, RCOMP_1, SETFAM_1, TARSKI, FINSET_1, XBOOLE_0, CARD_5, RELAT_1, ZFMISC_1, FUNCT_1, STRUCT_0, ORDINAL2, TOPS_2, FUNCT_4, COMPTS_1, PARTFUN1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_3, SETFAM_1, FINSET_1, DOMAIN_1, FUNCT_4, STRUCT_0, PRE_TOPC, TOPS_2;
definitions TARSKI, PARTFUN1, TOPS_2, XBOOLE_0, STRUCT_0, PRE_TOPC;
theorems TARSKI, SETFAM_1, FUNCT_1, FUNCT_3, ZFMISC_1, ORDERS_1, PRE_TOPC, TOPS_1, TOPS_2, RELAT_1, XBOOLE_0, XBOOLE_1, SUBSET_1, FUNCT_2, STRUCT_0, FUNCT_4, RELSET_1, FINSET_1, PARTFUN1;
schemes MCART_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC, TOPS_1, FUNCT_1;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_3, FINSET_1, TOPS_2, FUNCT_4, RELSET_1;
requirements HIDDEN, SUBSET, BOOLE;
equalities SUBSET_1, STRUCT_0;
expansions TARSKI, TOPS_2, XBOOLE_0, PRE_TOPC;
Lm1:
for T, S being non empty TopSpace
for X being set
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) = X & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f | X tolerates g | X holds
f +* g is continuous Function of T,S