environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, ZFMISC_1, XBOOLE_0, FINSEQ_5, RELAT_1, ORDINAL4, NAT_1, TARSKI, FUNCT_1, XXREAL_0, SUBSET_1, ARYTM_3, FINSEQ_4, ARYTM_1, CARD_1, RFINSEQ, PARTFUN1, FINSEQ_6, JORDAN3;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, ZFMISC_1, REAL_1, NAT_1, NAT_D, RELAT_1, PARTFUN1, RELSET_1, FUNCT_1, FINSEQ_1, FINSEQ_4, RFINSEQ, FINSEQ_5;
definitions TARSKI, XBOOLE_0;
theorems NAT_1, FINSEQ_1, FINSEQ_4, FINSEQ_3, FINSEQ_2, FUNCT_1, ZFMISC_1, FINSEQ_5, RELAT_1, RFINSEQ, TARSKI, ENUMSET1, PARTFUN2, GRFUNC_1, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, PARTFUN1, NAT_D, XREAL_0, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, INT_1, FINSEQ_1, FINSEQ_5, ORDINAL1, NAT_1, CARD_1, XXREAL_0;
constructors HIDDEN, XXREAL_0, NAT_1, INT_1, PARTFUN1, FINSEQ_4, RFINSEQ, BINARITH, FINSEQ_5, REAL_1, RELSET_1, NAT_D, ENUMSET1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI, XBOOLE_0;
Lm1:
for x, y being set holds rng <*x,y*> = {x,y}
Lm2:
for x, y, z being set holds rng <*x,y,z*> = {x,y,z}
theorem Th21:
for
p1,
p2,
p3 being
set holds
p1 .. <*p1,p2,p3*> = 1
theorem Th22:
for
p1,
p2,
p3 being
set st
p1 <> p2 holds
p2 .. <*p1,p2,p3*> = 2
theorem Th23:
for
p1,
p2,
p3 being
set st
p1 <> p3 &
p2 <> p3 holds
p3 .. <*p1,p2,p3*> = 3
Lm3:
for i being Nat
for D being non empty set
for p being Element of D
for f being FinSequence of D st p in rng f & p .. f > i holds
i + (p .. (f /^ i)) = p .. f
theorem Th117:
for
D being non
empty set for
f being
FinSequence of
D for
k1,
k2 being
Nat st 1
<= k1 &
k1 <= len f & 1
<= k2 &
k2 <= len f holds
(
(mid (f,k1,k2)) . 1
= f . k1 & (
k1 <= k2 implies (
len (mid (f,k1,k2)) = (k2 -' k1) + 1 & ( for
i being
Nat st 1
<= i &
i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) ) ) ) & (
k1 > k2 implies (
len (mid (f,k1,k2)) = (k1 -' k2) + 1 & ( for
i being
Nat st 1
<= i &
i <= len (mid (f,k1,k2)) holds
(mid (f,k1,k2)) . i = f . ((k1 -' i) + 1) ) ) ) )
theorem Th121:
for
D being non
empty set for
f being
FinSequence of
D for
k1,
k2,
i being
Nat st 1
<= k1 &
k1 <= k2 &
k2 <= len f & 1
<= i & (
i <= (k2 -' k1) + 1 or
i <= (k2 - k1) + 1 or
i <= (k2 + 1) - k1 ) holds
(
(mid (f,k1,k2)) . i = f . ((i + k1) -' 1) &
(mid (f,k1,k2)) . i = f . ((i -' 1) + k1) &
(mid (f,k1,k2)) . i = f . ((i + k1) - 1) &
(mid (f,k1,k2)) . i = f . ((i - 1) + k1) )