environ
vocabularies HIDDEN, NUMBERS, RELAT_1, TARSKI, XBOOLE_0, FUNCT_1, MEMBERED, SUBSET_1, XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, FUNCOP_1, FUNCT_4, ZFMISC_1, ORDINAL2, ARYTM_3, NAT_1, PARTFUN1, FUNCT_2, SETFAM_1, CARD_1, VALUED_0, PBOOLE, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PBOOLE, ORDINAL1, SETFAM_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, NUMBERS, MEMBERED, XCMPLX_0, XREAL_0, XXREAL_0, RAT_1, NAT_1, INT_1;
definitions TARSKI, FUNCT_1, RELAT_1, PARTFUN2, FUNCT_2;
theorems NUMBERS, XBOOLE_1, RELAT_1, MEMBERED, FUNCT_1, XCMPLX_0, XXREAL_0, XREAL_0, RAT_1, INT_1, ORDINAL1, FUNCT_4, FUNCOP_1, XBOOLE_0, ZFMISC_1, FUNCT_2, NAT_1, XREAL_1, RELSET_1, SETFAM_1, PARTFUN2, PARTFUN1, SUBSET_1;
schemes NAT_1;
registrations MEMBERED, RELAT_1, FUNCOP_1, XREAL_0, RAT_1, ORDINAL1, INT_1, FUNCT_1, XBOOLE_0, RELSET_1, FUNCT_2, SETFAM_1, SUBSET_1, PBOOLE, NAT_1;
constructors HIDDEN, XCMPLX_0, RAT_1, MEMBERED, FUNCOP_1, FUNCT_4, XXREAL_0, PARTFUN1, NAT_1, SETFAM_1, RELSET_1, NUMBERS;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities XBOOLE_0, FUNCOP_1, RELAT_1;
expansions TARSKI, FUNCT_1, RELAT_1, PARTFUN2, FUNCT_2;
Lm1:
for x being non empty set
for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M
::: synonym f is non-zero for f is non-empty;
:::end;