environ
vocabularies HIDDEN, YELLOW_1, PBOOLE, CARD_3, WAYBEL18, WAYBEL_3, XBOOLE_0, PRE_TOPC, STRUCT_0, ORDERS_2, WAYBEL24, WAYBEL25, RELAT_2, MONOID_0, SUBSET_1, ORDINAL2, FUNCT_1, XXREAL_0, CAT_1, YELLOW_0, NEWTON, TARSKI, YELLOW_9, WAYBEL11, ZFMISC_1, CARD_1, RCOMP_1, FUNCT_3, RELAT_1, WELLORD1, VALUED_1, T_0TOPSP, WAYBEL_0, SEQM_3, BINOP_1, FUNCOP_1, BORSUK_1, GROUP_6, YELLOW16, TOPS_2, REWRITE1, LATTICE3, EQREL_1, FUNCTOR0, WAYBEL_1, FUNCT_6, RLVECT_2, FUNCT_2, CANTOR_1, FUNCT_4, WAYBEL_9, MCART_1, FINSET_1, SETFAM_1, WAYBEL26;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, MCART_1, FINSET_1, RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, TOPS_2, FUNCT_3, FUNCT_4, ORDINAL1, NUMBERS, SETFAM_1, FUNCT_2, FUNCOP_1, STRUCT_0, CARD_3, FUNCT_6, MONOID_0, PRALG_1, FUNCT_7, WELLORD1, ORDERS_2, LATTICE3, PRE_TOPC, CANTOR_1, T_0TOPSP, BORSUK_1, QUANTAL1, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, YELLOW_9, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16;
definitions TARSKI, RELAT_1, YELLOW_0, BORSUK_1, WAYBEL_0, WAYBEL_1, T_0TOPSP, YELLOW16, URYSOHN1, XBOOLE_0;
theorems YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, PRE_TOPC, BORSUK_1, ORDERS_2, YELLOW12, WAYBEL10, WAYBEL24, WAYBEL25, RELAT_1, FUNCT_2, FUNCT_1, TOPS_2, TOPS_3, ENUMSET1, FUNCT_3, WAYBEL_3, PBOOLE, FUNCOP_1, CARD_3, TARSKI, ZFMISC_1, RELSET_1, WELLORD1, TSP_1, TOPS_1, WAYBEL21, QUANTAL1, CANTOR_1, FUNCT_7, YELLOW_9, WAYBEL18, WAYBEL20, MCART_1, YELLOW14, WAYBEL11, FINSET_1, WAYBEL15, PRALG_1, YELLOW16, WAYBEL14, FUNCT_5, CARD_5, SETFAM_1, XBOOLE_0, XBOOLE_1, FUNCT_6, STRUCT_0, PARTFUN1, XTUPLE_0;
schemes FUNCT_1, PBOOLE;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC, BORSUK_1, LATTICE3, YELLOW_0, TSP_1, MONOID_0, WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_1, WAYBEL_2, WAYBEL_3, YELLOW_6, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL18, WAYBEL24, YELLOW14, WAYBEL25, YELLOW16, FUNCT_1, XTUPLE_0;
constructors HIDDEN, TOLER_1, FUNCT_7, TOPS_2, BORSUK_1, T_0TOPSP, CANTOR_1, MONOID_0, QUANTAL1, ORDERS_3, PRALG_3, WAYBEL_1, WAYBEL11, YELLOW_9, WAYBEL18, WAYBEL24, WAYBEL25, YELLOW16, XTUPLE_0, XFAMILY;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities RELAT_1, YELLOW_2, STRUCT_0, ORDINAL1;
expansions TARSKI, RELAT_1, BORSUK_1, WAYBEL_0, YELLOW_2, STRUCT_0;
definition
let X,
Y,
Z be non
empty TopSpace;
let f be
continuous Function of
Y,
Z;
uniqueness
for b1, b2 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st ( for g being continuous Function of X,Y holds b1 . g = f * g ) & ( for g being continuous Function of X,Y holds b2 . g = f * g ) holds
b1 = b2
existence
ex b1 being Function of (oContMaps (X,Y)),(oContMaps (X,Z)) st
for g being continuous Function of X,Y holds b1 . g = f * g
uniqueness
for b1, b2 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st ( for g being continuous Function of Z,X holds b1 . g = g * f ) & ( for g being continuous Function of Z,X holds b2 . g = g * f ) holds
b1 = b2
existence
ex b1 being Function of (oContMaps (Z,X)),(oContMaps (Y,X)) st
for g being continuous Function of Z,X holds b1 . g = g * f
end;
Lm1:
for Z being monotone-convergence T_0-TopSpace
for Y being non empty SubSpace of Z
for f being continuous Function of Z,Y st f is being_a_retraction holds
Y is monotone-convergence