environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, ORDINAL4, XBOOLE_0, SUBSET_1, RELAT_1, BINTREE1, TREES_1, MARGREL1, TARSKI, ORDINAL1, CARD_1, ARYTM_3, PARTFUN1, FUNCT_1, XBOOLEAN, TREES_2, FINSEQ_2, TREES_4, ZFMISC_1, FUNCOP_1, MCART_1, FINSEQ_5, NAT_1, BINARITH, CAT_1, XXREAL_0, EUCLID, FINSET_1, POWER, ARYTM_1, BINARI_3, INT_1, ABIAN, BINTREE2, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XTUPLE_0, MCART_1, NAT_1, NAT_D, ABIAN, SERIES_1, RELAT_1, MARGREL1, DOMAIN_1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, FINSET_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_5, BINARITH, BINARI_3, TREES_1, TREES_2, TREES_4, BINTREE1, EUCLID, XXREAL_0;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, MCART_1, NAT_1, NAT_2, WELLORD2, ZFMISC_1, FUNCT_1, FUNCT_2, CARD_1, CARD_2, POWER, FUNCOP_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSEQ_5, FINSEQ_6, BINARI_3, TREES_1, TREES_2, BINTREE1, XBOOLE_0, XBOOLE_1, XREAL_1, NAT_D, PARTFUN1, XXREAL_0, XREAL_0, TREES_9, RELSET_1;
schemes FUNCT_2, NAT_1, FINSEQ_2, TREES_2, FUNCT_1;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, MARGREL1, TREES_2, TREES_9, BINTREE1, FINSEQ_2, INT_1, XTUPLE_0, CARD_1;
constructors HIDDEN, WELLORD2, DOMAIN_1, NAT_D, FINSEQOP, SERIES_1, BINARITH, FINSEQ_5, TREES_9, ABIAN, EUCLID, BINTREE1, BINARI_3, RELSET_1, XTUPLE_0, BINOP_1, PRE_POLY;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities EUCLID, FINSEQ_2, MARGREL1, XBOOLEAN, BINOP_1;
expansions TARSKI, XBOOLE_0;
Lm1:
for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D
;
Lm2:
for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D
;
Lm3:
for D being non empty set
for f being FinSequence of D holds Rev f is FinSequence of D
;