environ
vocabularies HIDDEN, NUMBERS, TREES_2, SUBSET_1, RELAT_1, FINSEQ_1, FUNCT_1, TARSKI, TREES_1, XXREAL_0, ARYTM_3, CARD_1, FUNCOP_1, XBOOLE_0, TREES_3, ZFMISC_1, NAT_1, FINSEQ_2, TREES_A, ORDINAL4, FUNCT_6, FINSEQ_4, MCART_1, PARTFUN1, TREES_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, DOMAIN_1, FUNCOP_1, FUNCT_3, FINSEQ_1, FINSEQ_2, TREES_1, TREES_2, FUNCT_6, TREES_3, XXREAL_0;
definitions TARSKI, FINSEQ_1, TREES_1, TREES_2;
theorems TARSKI, ZFMISC_1, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_6, FINSEQ_2, FINSEQ_3, TREES_1, TREES_2, TREES_3, RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, FUNCT_5, ORDINAL1, CARD_1;
schemes CLASSES1, FINSEQ_1, XBOOLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, FINSEQ_1, TREES_2, TREES_3, CARD_1, FINSEQ_2, FUNCOP_1, TREES_1, XTUPLE_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FUNCT_5, FINSEQ_2, FUNCT_6, TREES_3, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1, TREES_2, FINSEQ_2, FUNCT_6;
expansions TARSKI, FINSEQ_1;
Lm2:
for n being Nat
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )