environ
vocabularies HIDDEN, STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, FINSET_1, NAT_1, ARYTM_1, PARTFUN1, AMI_1, ARYTM_3, COMPOS_1, SCMFSA6C, XXREAL_0, SUPINF_2, MEMSTR_0, PBOOLE, GOBRD13, QUANTAL1, SCMFSA9A;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, FUNCT_7, CARD_1, CARD_3, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, NUMBERS, INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, AFINSQ_1, FINSEQ_1, FUNCT_2, DOMAIN_1, VALUED_0, VALUED_1, STRUCT_0, XXREAL_0, MEASURE6;
definitions STRUCT_0, FUNCT_1;
theorems ZFMISC_1, TARSKI, CARD_3, FUNCT_4, FUNCOP_1, FUNCT_1, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, SUBSET_1, FUNCT_7, PARTFUN1, PBOOLE, XREAL_1, NAT_D, NAT_2, STRUCT_0, MEASURE6, XTUPLE_0;
schemes FRAENKEL;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, CARD_3, STRUCT_0, RELSET_1, PBOOLE, NAT_1, CARD_1, MEASURE6;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7, PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities FUNCOP_1, STRUCT_0, FUNCT_4;
expansions STRUCT_0, FUNCT_1;
Lm1:
for N being with_zero set holds the_Values_of (Trivial-Mem N) = 0 .--> NAT
:: na razie wykorzystujemy tylko rejestracje, ze 'with_zero'
:: musi byc 'non empty' i w definicji Trivial-Mem N
:: ale tutaj mozna sie tego pozbyc, biorac zamiast 0
:: the Element of N i potrzebujemy tylko to, ze N jest niepusty