environ
vocabularies HIDDEN, NUMBERS, REAL_1, FUNCT_1, RELAT_1, XBOOLE_0, FUNCT_4, TARSKI, PRE_TOPC, SUBSET_1, BORSUK_1, TOPS_2, CARD_1, ARYTM_3, XXREAL_0, XXREAL_1, TOPMETR, STRUCT_0, ORDINAL2, RCOMP_1, ARYTM_1, PCOMPS_1, METRIC_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, STRUCT_0, PRE_TOPC, TOPS_2, COMPTS_1, RCOMP_1, METRIC_1, PCOMPS_1, TOPMETR, XXREAL_0;
definitions TARSKI;
theorems BORSUK_1, COMPTS_1, FUNCT_1, FUNCT_2, FUNCT_4, HEINE, TOPMETR, PCOMPS_1, PRE_TOPC, RCOMP_1, TARSKI, TOPS_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, XXREAL_2, RELAT_1, XREAL_0;
schemes CLASSES1, FUNCT_2;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, MEMBERED, STRUCT_0, PRE_TOPC, METRIC_1, PCOMPS_1, BORSUK_1, TOPMETR, XXREAL_2, XREAL_0;
constructors HIDDEN, FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_2, COMPTS_1, TOPMETR, XXREAL_2, PCOMPS_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0;
expansions TARSKI;
Lm1:
for f, g being Function st f .: ((dom f) /\ (dom g)) c= rng g holds
(rng f) \ (rng g) c= rng (f +* g)
reconsider dwa = 2 as Real ;