environ
vocabularies HIDDEN, POLYNOM1, PBOOLE, NAT_1, NUMBERS, FRECHET, PCOMPS_1, REAL_1, CARDFIL2, YELLOW13, CARD_1, XBOOLE_0, SUBSET_1, TARSKI, ORDINAL1, FUNCT_1, PRE_TOPC, STRUCT_0, XXREAL_0, RCOMP_1, METRIC_1, ARYTM_3, YELLOW19, NORMSP_1, NORMSP_2, ARYTM_1, SETFAM_1, ALGSTR_0, ZFMISC_1, SUPINF_2, CONNSP_2, TOPS_1, RELAT_2, RLTOPSP1, FILTER_0, XXREAL_1, ORDERS_2, WAYBEL_0, BINOP_1, RELAT_1, CARD_3, FUNCT_2, FINSUB_1, FINSEQ_1, FINSOP_1, SETWISEO, ORDINAL4, VECTSP_1, SERIES_1, YELLOW_1, TOPGRP_1, GROUP_1, SERIES_3, CARDFIL3, RLVECT_1, GROUP_1A;
notations HIDDEN, CARDFIL2, GROUP_1A, TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, TOPS_1, CONNSP_2, YELLOW13, RUSUB_4, RLTOPSP1, ORDERS_2, WAYBEL_0, METRIC_1, NUMBERS, XCMPLX_0, XREAL_0, NAT_1, XXREAL_0, STRUCT_0, ALGSTR_0, PRE_TOPC, NORMSP_0, NORMSP_1, NORMSP_2, FRECHET, YELLOW19, PCOMPS_1, ZFMISC_1, BINOP_1, PBOOLE, RELAT_1, FINSUB_1, RLVECT_1, FINSEQ_1, FINSOP_1, SETWISEO, VECTSP_1, YELLOW_1, TOPGRP_1, GROUP_1;
definitions YELLOW13;
theorems GROUP_1A, FRECHET, CONNSP_2, YELLOW_8, YELLOW19, TOPMETR, METRIC_1, NORMSP_2, PCOMPS_1, RLTOPSP1, YELLOW13, XBOOLE_0, RUSUB_4, CARD_FIL, RLVECT_1, TOPS_1, TOPGRP_1, FINSUB_1, FINSEQ_1, FINSOP_1, FINSEQ_4, BHSP_5, FVSUM_1, RELAT_1, TARSKI, XBOOLE_1, FUNCT_1, FINSEQ_2, FINSEQ_3, FUNCT_2, PARTFUN1, STRUCT_0, WAYBEL_0, YELLOW_1, GROUP_1, CARDFIL2;
schemes FUNCT_2, BINOP_2;
registrations GROUP_1A, PCOMPS_1, FRECHET, YELLOW19, XXREAL_0, XREAL_0, NAT_1, SUBSET_1, STRUCT_0, XCMPLX_0, CARD_1, METRIC_1, TOPS_1, RLVECT_1, RLTOPSP1, RELAT_1, XBOOLE_0, FUNCT_1, FINSEQ_1, PBOOLE, FINSUB_1, FVSUM_1, OSALG_1, YELLOW_1, TOPGRP_1, GROUP_1, MEMBERED, ORDERS_2;
constructors HIDDEN, YELLOW_8, FRECHET, YELLOW19, TOPS_2, NAT_LAT, NORMSP_2, TOPS_1, RUSUB_4, YELLOW13, FINSOP_1, SETWISEO, FINSEQOP, MEMBERED, NAT_1, BORSUK_1, CARDFIL2, GROUP_1A;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE;
equalities ORDINAL1, ALGSTR_0;
expansions TARSKI, FRECHET, XBOOLE_0, FUNCT_1, RELAT_1, CARDFIL2;
Lm1:
for X being non empty addLoopStr
for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
Lm2:
for X being LinearTopSpace
for x being Point of X
for O being local_base of X holds { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } is non empty Subset-Family of X
Lm3:
for T being LinearTopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for V being local_base of T
for B being Subset-Family of T st [#] L is directed & B = { (x + U) where U is Subset of T : ( U in V & U is a_neighborhood of 0. T ) } holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )