environ
vocabularies HIDDEN, NUMBERS, NAT_1, CARD_1, ARYTM_3, XBOOLE_0, XXREAL_0, TARSKI, STRUCT_0, FUNCT_1, SUPINF_2, FUNCOP_1, SUBSET_1, FINSEQ_1, RELAT_1, AFINSQ_1, ALGSEQ_1, POLYNOM1, FINSET_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, MEMBERED, XCMPLX_0, NAT_1, XXREAL_2, RELAT_1, FUNCT_1, FUNCOP_1, STRUCT_0, FUNCT_2, XXREAL_0, POLYNOM1;
definitions TARSKI, XBOOLE_0, POLYNOM1;
theorems TARSKI, ZFMISC_1, FUNCT_1, FUNCT_2, NAT_1, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, POLYNOM1, XXREAL_2;
schemes FUNCT_2, NAT_1;
registrations ORDINAL1, RELSET_1, XREAL_0, STRUCT_0, FINSET_1, CARD_1, XXREAL_2, MEMBERED;
constructors HIDDEN, FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, RLVECT_1, RELSET_1, POLYNOM1, XXREAL_2;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0;
expansions ;
Lm1:
for R being non empty ZeroStr
for p being AlgSequence of R ex m being Nat st m is_at_least_length_of p
Lm2:
for R being non empty ZeroStr
for p being AlgSequence of R st p = <%(0. R)%> holds
len p = 0