environ
vocabularies HIDDEN, PROB_1, MEASURE1, FUNCT_1, NUMBERS, RELAT_1, SUPINF_2, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, CARD_1, ARYTM_3, XXREAL_0, NAT_1, ZFMISC_1, VALUED_0, ORDINAL2, MEASURE2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, NAT_1, SETFAM_1, PROB_1, SUPINF_2, MEASURE1;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, FUNCT_2, ZFMISC_1, NAT_1, SETFAM_1, SUPINF_2, MEASURE1, ENUMSET1, PROB_2, XBOOLE_0, XBOOLE_1, PROB_1, ORDINAL1, XXREAL_0, RELAT_1;
schemes NAT_1, RECDEF_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XXREAL_0, MEASURE1, MEMBERED, RELSET_1, NAT_1, XCMPLX_0;
constructors HIDDEN, PARTFUN1, NAT_1, PROB_2, MEASURE1, SUPINF_1, XREAL_0, RELSET_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities SUPINF_2;
expansions TARSKI, XBOOLE_0;
theorem Th18:
for
N being
Function st ( for
n being
Nat holds
N . n c= N . (n + 1) ) holds
for
m,
n being
Nat st
n <= m holds
N . n c= N . m