environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, FUNCT_1, RELAT_1, XBOOLE_0, ORDINAL1, XXREAL_0, VALUED_0, RAT_1, COMPLEX1, ARYTM_1, ARYTM_3, MEMBERED, PARTFUN1, TARSKI, SUBSET_1, CARD_1, XCMPLX_0, INT_1, SQUARE_1, FUNCT_4, FINSET_1, NAT_1, ORDINAL2, VALUED_1, AMISTD_1, FUNCOP_1, AMISTD_2, AMISTD_3, ORDINAL4, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FINSET_1, CARD_1, XCMPLX_0, NUMBERS, COMPLEX1, XXREAL_0, XXREAL_2, FUNCOP_1, XREAL_0, RAT_1, INT_1, INT_2, SQUARE_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4, FINSEQ_1, MEMBERED, NAT_1, VALUED_0;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, VALUED_0, WELLORD2;
theorems FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, VALUED_0, COMPLEX1, FINSEQ_1, XBOOLE_0, TARSKI, GRFUNC_1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, INT_1, ORDINAL1, XXREAL_0, FUNCOP_1, ZFMISC_1, XXREAL_2, XBOOLE_1, CARD_1, CARD_2, RAT_1, XTUPLE_0, XREAL_1, FINSEQ_3;
schemes FUNCT_1, CLASSES1, FRAENKEL, RECDEF_1, NAT_1;
registrations ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, VALUED_0, RAT_1, INT_1, NAT_1, FUNCT_1, FINSET_1, XXREAL_0, RELAT_1, XXREAL_2, FUNCOP_1, FUNCT_4, CARD_1, FINSEQ_1;
constructors HIDDEN, PARTFUN1, RAT_1, VALUED_0, SQUARE_1, MEMBERED, INT_2, FINSEQ_1, NAT_1, FUNCT_4, NAT_D, RELSET_1, XXREAL_2, FUNCOP_1, DOMAIN_1, WELLORD2, FINSEQ_3, REAL_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities XBOOLE_0, XCMPLX_0, SQUARE_1, FINSEQ_1, FUNCOP_1;
expansions TARSKI, XBOOLE_0, FUNCT_1, FINSEQ_1, VALUED_0, WELLORD2;
Lm1:
for f being FinSequence
for h being Function st dom h = dom f holds
h is FinSequence
Lm2:
for f, g being FinSequence
for h being Function st dom h = (dom f) /\ (dom g) holds
h is FinSequence
Lm3:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 - f2) = C
Lm4:
for C being set
for D1, D2 being non empty complex-membered set
for f1 being Function of C,D1
for f2 being Function of C,D2 holds dom (f1 /" f2) = C
Lm5:
for i being Nat
for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (Shift (p,i)) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
Lm6:
for j, k, l being Nat st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds
( 1 <= j & j <= l + k )
Lm7:
for i being Nat
for p, q being FinSubsequence st q c= p holds
dom (Shift (q,i)) c= dom (Shift (p,i))
Lm8:
for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))