environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, PROB_1, XXREAL_0, ARYTM_3, FUNCT_1, XBOOLE_0, TARSKI, NAT_1, RELAT_1, CARD_1, SETFAM_1, EQREL_1, CARD_3, ZFMISC_1, SEQM_3, ORDINAL2, SEQ_2, SETLIM_1;
notations HIDDEN, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, SETFAM_1, PROB_1, FUNCT_2, KURATO_0;
definitions TARSKI;
theorems FUNCT_1, FUNCT_2, PROB_1, NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XCMPLX_1, SETFAM_1, ZFMISC_1, CARD_3, KURATO_0, PROB_2, XREAL_1, ORDINAL1, VALUED_0, RELAT_1;
schemes NAT_1, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, XREAL_0, FUNCT_2, RELAT_1, PROB_1, RELSET_1, NAT_1;
constructors HIDDEN, SETFAM_1, NAT_1, KURATO_0, XREAL_0, RELSET_1, FINSUB_1, PROB_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities SUBSET_1;
expansions TARSKI;
Lm1:
for i, j being Nat holds
( not i <= j or i = j or i + 1 <= j )
theorem Th3:
for
n being
Nat for
x being
object for
Y being
set for
f being
sequence of
Y holds
( ( for
k1 being
Nat holds
x in f . (n + k1) ) iff for
Z being
set st
Z in { (f . k2) where k2 is Nat : n <= k2 } holds
x in Z )
Lm2:
for X being set
for A being Subset of X
for B being SetSequence of X st B is constant & the_value_of B = A holds
for n being Nat holds
( B . n = A & Union B = A & Intersection B = A )