environ
vocabularies HIDDEN, NUMBERS, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, SUBSET_1, FINSEQ_1, CARD_1, FUNCT_1, RELAT_1, FINSEQ_4, ZFMISC_1, XBOOLE_0, ORDINAL4, TARSKI, PARTFUN1, RFINSEQ, FINSEQ_5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_4, ZFMISC_1, RFINSEQ, NAT_D, XXREAL_0;
definitions TARSKI, FUNCT_1, XBOOLE_0;
theorems TARSKI, NAT_1, PARTFUN2, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, RFINSEQ, RELAT_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, XREAL_0, NAT_D;
schemes FINSEQ_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_1;
constructors HIDDEN, XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, ZFMISC_1, RFINSEQ, NAT_D, REAL_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1;
expansions FUNCT_1, FINSEQ_1;
Lm1:
for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
Lm2:
for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
Lm3:
for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one