environ
vocabularies HIDDEN, NUMBERS, FUNCT_1, RELAT_1, SETFAM_1, TARSKI, XBOOLE_0, ZFMISC_1, PROB_1, SUBSET_1, FUNCOP_1, CARD_3, ORDINAL2, NAT_1, ARYTM_3, CARD_1, XXREAL_0, SEQ_2, KURATO_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, ZFMISC_1, XXREAL_0, REAL_1, NAT_1, SETFAM_1, MCART_1, DOMAIN_1, RELAT_1, FUNCT_1, INT_1, FINSEQ_1, RELSET_1, FUNCT_2, FUNCOP_1, CARD_3, PROB_1, VALUED_0, FUNCT_6;
definitions XBOOLE_0, TARSKI;
theorems SETFAM_1, XBOOLE_1, NAT_1, FUNCT_2, XBOOLE_0, FUNCT_1, ZFMISC_1, RELAT_1, FUNCT_6, PROB_1, MEASURE2, XXREAL_0, ORDINAL1, VALUED_0, TARSKI;
schemes FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, FUNCT_2, XREAL_0, NAT_1, FUNCOP_1, RELSET_1;
constructors HIDDEN, SETFAM_1, REAL_1, PROB_1, LIMFUNC1, FUNCT_6, FINSEQ_1, DOMAIN_1, NAT_1, RELSET_1;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities SUBSET_1;
expansions ;
theorem Th18:
for
f being
Function st ( for
i being
Nat holds
f . (i + 1) c= f . i ) holds
for
i,
j being
Nat st
i <= j holds
f . j c= f . i