environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, PRE_TOPC, EUCLID, XBOOLE_0, ORDINAL2, FUNCT_1, RELAT_1, RCOMP_1, TARSKI, RELAT_2, CONNSP_1, XXREAL_0, TOPMETR, ARYTM_3, REAL_1, STRUCT_0, XXREAL_1, CARD_1, BORSUK_1, FINSEQ_1, PARTFUN1, MCART_1, TOPREAL2, TOPREAL1, TOPS_2, ARYTM_1, SUPINF_2, PSCOMP_1, SPPOL_1, SEQ_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, FINSEQ_1, RLVECT_1, EUCLID, TOPMETR, TOPREAL1, TOPREAL2, TMAP_1, CONNSP_1, SPPOL_1, PSCOMP_1, XXREAL_0;
definitions TARSKI;
theorems BORSUK_1, EUCLID, FUNCT_1, FUNCT_2, PRE_TOPC, RCOMP_1, TARSKI, TOPMETR, TOPS_2, TOPREAL1, TOPREAL2, TOPREAL3, METRIC_1, CONNSP_1, TREAL_1, XREAL_0, PSCOMP_1, TMAP_1, FINSEQ_1, SPPOL_2, JORDAN2B, XBOOLE_0, XBOOLE_1, TSEP_1, XREAL_1, SPPOL_1, XXREAL_0, XXREAL_1, RELAT_1, RLVECT_1;
schemes ;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID, TOPMETR, TOPREAL2, JORDAN2B, MONOID_0, TMAP_1;
constructors HIDDEN, REAL_1, RCOMP_1, CONNSP_1, TOPS_2, COMPTS_1, TMAP_1, TOPMETR, TOPREAL1, TOPREAL2, SPPOL_1, PSCOMP_1, BINOP_2, MONOID_0, PCOMPS_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities STRUCT_0, RLVECT_1;
expansions ;
Lm1:
for X, Y, Z being non empty TopSpace
for f being continuous Function of X,Y
for g being continuous Function of Y,Z holds g * f is continuous Function of X,Z
;