:: Basic Properties and Concept of Selected Subsequence of Zero Based Finite
:: Sequences
:: by Yatsuka Nakamura and Hisashi Ito
::
:: Received June 27, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, FUNCT_1, NAT_1, TARSKI, MEMBERED, ORDINAL1,
FINSET_1, RELAT_1, AFINSQ_1, ARYTM_1, ARYTM_3, FINSEQ_1, XXREAL_0,
CARD_1, XBOOLE_0, ORDINAL4, FINSEQ_5, RFINSEQ, JORDAN3, CARD_3, XCMPLX_0,
AFINSQ_2, BINOP_1, SETWISEO, FINSOP_1, FUNCOP_1, BINOP_2, VALUED_0,
FUNCT_2, INT_1, PRGCOR_2, XREAL_0, SEQ_1, SERIES_1, VALUED_1, RAT_1,
SQUARE_1, COMPLEX1, PARTFUN3, PRE_POLY, AMISTD_1, AMISTD_2, REAL_1,
ORDINAL2;
notations TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, ORDINAL1, CARD_1, NUMBERS,
RELAT_1, FUNCT_1, XCMPLX_0, NAT_1, FINSET_1, XXREAL_0, NAT_D, AFINSQ_1,
SEQ_1, MEMBERED, VALUED_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, INT_1,
BINOP_1, BINOP_2, SETWISEO, FINSOP_1, FINSEQ_1, RECDEF_1, VALUED_0,
SERIES_1, RAT_1, PARTFUN3, RFINSEQ, ORDINAL2;
constructors SERIES_1, PARTFUN3, WELLORD2, SETWISEO, FINSOP_1, NAT_D,
RECDEF_1, BINOP_2, RELSET_1, AFINSQ_1, FUNCOP_1, SQUARE_1, BINOP_1,
XTUPLE_0, RFINSEQ, ORDINAL2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1,
NUMBERS, XXREAL_0, XREAL_0, NAT_1, BINOP_2, CARD_1, FINSEQ_1, AFINSQ_1,
ORDINAL2, RELSET_1, ORDINAL3, VALUED_1, VALUED_0, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities VALUED_1, BINOP_1, ORDINAL1;
expansions TARSKI, XBOOLE_0, FUNCT_1, BINOP_1, ORDINAL1, FINSEQ_1;
theorems TARSKI, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, CARD_2, XBOOLE_0,
XBOOLE_1, FINSET_1, ORDINAL1, CARD_1, XREAL_1, AFINSQ_1, XXREAL_0, NAT_2,
FINSEQ_2, WELLORD2, MEMBERED, VALUED_0, VALUED_1, XREAL_0, NAT_D,
SERIES_1, PARTFUN3, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1, FINSOP_1,
FINSEQ_1, FUNCT_2, XCMPLX_0, GRFUNC_1, RAT_1, INT_1, FINSEQ_3, RFINSEQ,
ORDINAL2, FINSEQ_5;
schemes NAT_1, AFINSQ_1, FUNCT_2, BINOP_1;
begin :: Preparation
reserve i,j,k,n,m for Nat,
x,y,z,y1,y2 for object, X,Y,D for set,
p,q for XFinSequence;
Lm1:
for X,Y be finite set,F be Function of X,Y st card X=card Y
holds F is onto iff F is one-to-one
proof
let X,Y be finite set,F be Function of X,Y such that
A1: card X=card Y;
thus F is onto implies F is one-to-one
proof
assume
A2: F is onto;
assume F is not one-to-one;
then consider x1,x2 be object such that
A3: x1 in dom F and
A4: x2 in dom F and
A5: F.x1=F.x2 and
A6: x1<>x2;
reconsider Xx=X\{x1} as finite set;
Y c= F.:Xx
proof
let Fy be object;
assume Fy in Y;
then Fy in rng F by A2,FUNCT_2:def 3;
then consider y being object such that
A7: y in dom F and
A8: F.y=Fy by FUNCT_1:def 3;
now
per cases;
suppose
A9: y=x1;
x2 in Xx by A4,A6,ZFMISC_1:56;
hence thesis by A4,A5,A8,A9,FUNCT_1:def 6;
end;
suppose
y<>x1;
then y in Xx by A7,ZFMISC_1:56;
hence thesis by A7,A8,FUNCT_1:def 6;
end;
end;
hence thesis;
end;
then
A10: Segm card Y c= Segm card Xx by CARD_1:66;
{x1} meets X by A3,ZFMISC_1:48;
then A11:Xx <>X by XBOOLE_1:83;
Xx c< X by A11;
hence thesis by A1,A10,NAT_1:39,CARD_2:48;
end;
thus F is one-to-one implies F is onto
proof
assume F is one-to-one; then
A12: card dom F=card (F.:dom F) by CARD_1:5,CARD_1:33;
assume F is not onto;
then not rng F = Y by FUNCT_2:def 3;
then not Y c= rng F;
then consider y being object such that
A13: y in Y and
A14: not y in rng F;
A15: card rng F <=card (Y\{y}) by A14,NAT_1:43,ZFMISC_1:34;
A16: F.:dom F= rng F by RELAT_1:113;
{y} meets Y by A13,ZFMISC_1:48;
then A17:Y\{y} <>Y by XBOOLE_1:83;
Y\{y} c< Y by A17;
then card (Y\{y})< card Y by CARD_2:48;
hence thesis by A1,A13,A15,A12,A16,FUNCT_2:def 1;
end;
end;
theorem Th1:
x in i implies x is Element of NAT
proof
i c= NAT;
hence thesis;
end;
begin
theorem Th2:
for X0 being finite natural-membered set holds ex n st X0 c= Segm n
proof
let X0 be finite natural-membered set;
consider p being Function such that
A1: rng p = X0 and
A2: dom p in NAT by FINSET_1:def 1;
reconsider np=dom p as Element of NAT by A2;
np=dom p;
then reconsider p as XFinSequence by AFINSQ_1:5;
X0 c= NAT by MEMBERED:6;
then reconsider p as XFinSequence of NAT by A1,RELAT_1:def 19;
defpred P[Nat] means ex n st for i st i in Segm $1 & $1-'1 in
dom p holds p.i in n;
A3: for k st P[k] holds P[k+1]
proof
let k;
assume P[k];
then consider n such that
A4: for i st i in k & k-'1 in dom p holds p.i in n;
per cases;
suppose
A5: k+1-1 =k;
m=len p;
k+1-'1=k by NAT_D:34;
then
for i st i in (k+1) & (k+1)-'1 in dom p holds p.i in 2
by A12,AFINSQ_1:86;
hence thesis;
end;
end;
for i st i in 0 & 0-'1 in dom p holds p.i in 0;
then
A13: P[0];
for k holds P[k] from NAT_1:sch 2(A13,A3);
then consider n such that
A14: for i st i in Segm len p & len p -'1 in dom p holds p.i in n;
rng p c= Segm n
proof
let y be object;
assume y in rng p;
then consider x being object such that
A15: x in dom p and
A16: y=p.x by FUNCT_1:def 3;
A17: len p -1Nat,D()->non empty set,F(set)->Element of D()}:
ex p being XFinSequence of D() st len p = i() &
for j st j in i() holds p.j = F(j)
proof
consider z being XFinSequence such that
A1: len z = i() and
A2: for i st i in i() holds z.i = F(i) from
AFINSQ_1:sch 2;
for j be Nat st j in i() holds z.j in D()
proof
let j be Nat;
reconsider j0=j as Element of NAT by ORDINAL1:def 12;
assume j in i();
then z.j0 = F(j0) by A2;
hence thesis;
end;
then reconsider z as XFinSequence of D() by A1,Th4;
take z;
thus len z = i() by A1;
let j be Nat;
thus thesis by A2;
end;
registration
cluster empty natural-valued for XFinSequence;
existence
proof
take the empty XFinSequence of NAT;
thus thesis;
end;
let p be complex-valued Sequence-like Function;
cluster -p -> Sequence-like;
coherence
proof
dom p = dom -p & dom p is ordinal by VALUED_1:8;
hence thesis;
end;
cluster p" -> Sequence-like;
coherence
proof
dom p = dom (p") by VALUED_1:def 7;
hence thesis;
end;
cluster p^2 -> Sequence-like;
coherence
proof
dom p = dom (p^2) by VALUED_1:11;
hence thesis;
end;
cluster abs p -> Sequence-like;
coherence
proof
dom p = dom abs p by VALUED_1:def 11;
hence thesis;
end;
let q be complex-valued Sequence-like Function;
cluster p+q -> Sequence-like;
coherence
proof
dom (p+q)=dom p /\dom q & dom p is ordinal & dom q is ordinal
by VALUED_1:def 1;
hence thesis;
end;
cluster p-q -> Sequence-like;
coherence;
cluster p(#)q -> Sequence-like;
coherence
proof
dom (p(#)q)=dom p /\dom q & dom p is ordinal & dom q is ordinal
by VALUED_1:def 4;
hence thesis;
end;
cluster p/"q -> Sequence-like;
coherence;
end;
registration
let p be complex-valued finite Function;
cluster -p -> finite;
coherence
proof
dom p = dom -p by VALUED_1:8;
hence thesis by FINSET_1:10;
end;
cluster p" -> finite;
coherence
proof
dom p = dom (p") by VALUED_1:def 7;
hence thesis by FINSET_1:10;
end;
cluster p^2 -> finite;
coherence
proof
dom p = dom (p^2) by VALUED_1:11;
hence thesis by FINSET_1:10;
end;
cluster abs p -> finite;
coherence
proof
dom p = dom abs p by VALUED_1:def 11;
hence thesis by FINSET_1:10;
end;
let q be complex-valued Function;
cluster p+q -> finite;
coherence
proof
dom (p+q)=dom p /\dom q by VALUED_1:def 1;
hence thesis by FINSET_1:10;
end;
cluster p-q -> finite;
coherence;
cluster p(#)q -> finite;
coherence
proof
dom (p(#)q)=dom p /\dom q by VALUED_1:def 4;
hence thesis by FINSET_1:10;
end;
cluster p/"q -> finite;
coherence;
cluster q/"p -> finite;
coherence;
end;
registration
let p be complex-valued Sequence-like Function;
let c be Complex;
cluster c+p -> Sequence-like;
coherence
proof
dom p = dom (c+p) by VALUED_1:def 2;
hence thesis;
end;
cluster p-c -> Sequence-like;
coherence;
cluster c(#)p -> Sequence-like;
coherence
proof
dom p = dom (c(#)p) by VALUED_1:def 5;
hence thesis;
end;
end;
registration
let p be complex-valued finite Function;
let c be Complex;
cluster c+p -> finite;
coherence
proof
dom p = dom (c+p) by VALUED_1:def 2;
hence thesis by FINSET_1:10;
end;
cluster p-c -> finite;
coherence;
cluster c(#)p -> finite;
coherence
proof
dom p = dom (c(#)p) by VALUED_1:def 5;
hence thesis by FINSET_1:10;
end;
end;
definition
let p;
func Rev p -> XFinSequence means
:Def1:
len it = len p & for i st i in dom it holds it.i = p.(len p - (i + 1));
existence
proof
deffunc F(Nat) = p.(len p - ($1 + 1));
ex q st len q = len p & for k
st k in len p holds q.k = F(k) from AFINSQ_1:sch 2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be XFinSequence such that
A1: len f1 = len p and
A2: for i st i in dom f1 holds f1.i = p.(len p -(i + 1)) and
A3: len f2 = len p and
A4: for i st i in dom f2 holds f2.i = p.(len p -(i + 1));
now
let i;
assume
A5: i in dom p;
then f1.i = p.(len p - (i + 1)) by A1,A2;
hence f1.i = f2.i by A3,A4,A5;
end;
hence thesis by A1,A3;
end;
end;
theorem Th5: ::from FINSEQ_5:60
dom p = dom Rev p & rng p = rng Rev p
proof
thus
A1: dom p = len p
.= len (Rev p) by Def1
.= dom(Rev p);
A2: len p = len(Rev p) by Def1;
hereby
let x be object;
assume x in rng p;
then consider z being object such that
A3: z in dom p and
A4: p.z = x by FUNCT_1:def 3;
reconsider i=z as Element of NAT by A3;
i+1<=len p by NAT_1:13,A3,AFINSQ_1:86;
then len p -'(i+1)=len p -(i+1) by XREAL_1:233;
then reconsider j = len p - (i + 1) as Element of NAT;
A5: j in len (Rev p) by A2,AFINSQ_1:86,XREAL_1:44;
then (Rev p).j = p.(len p - (j + 1)) by Def1;
hence x in rng(Rev p) by A4,A5,FUNCT_1:def 3;
end;
let x be object;
assume x in rng(Rev p);
then consider z being object such that
A6: z in dom(Rev p) and
A7: (Rev p).z = x by FUNCT_1:def 3;
reconsider i=z as Element of NAT by A6;
i < len p by A2,A6,AFINSQ_1:86;
then i+1<=len p by NAT_1:13;
then len p -'(i+1)=len p -(i+1) by XREAL_1:233;
then reconsider j = len p - (i + 1) as Element of NAT;
len p -(i+1) D -valued;
coherence
proof
rng f=rng (Rev f) by Th5;
hence thesis by RELAT_1:def 19;
end;
end;
definition
let p,n;
func p /^ n -> XFinSequence means :Def2:
len it = len p -' n & for m st m in dom it holds it.m = p.(m+n);
existence
proof
thus ex p1 be XFinSequence st len p1 = len p -' n & for m st m in
dom p1 holds p1.m = p.(m+n)
proof
deffunc F(Nat)=p.($1+n);
set k = len p -' n;
consider q such that
A1: len q = k & for m2 be Nat st m2 in k holds q.m2 = F(
m2) from AFINSQ_1:sch 2;
take q;
thus thesis by A1;
end;
end;
uniqueness
proof
let p1,p2 be XFinSequence;
thus (len p1 = len p -' n & for m be Nat st m in dom p1 holds p1.m = p.(m+
n)) & (len p2 = len p -' n & for m be Nat st m in dom p2 holds p2.m = p.(m+n))
implies p1 = p2
proof
assume that
A2: len p1 = len p -' n and
A3: for m st m in dom p1 holds p1.m = p.(m+n) and
A4: len p2 = len p -' n and
A5: for m st m in dom p2 holds p2.m = p.(m+n);
now
let m;
assume
A6: m in dom p1;
then p1.m = p.(m+n) by A3;
hence p1.m = p2.m by A2,A4,A5,A6;
end;
hence thesis by A2,A4;
end;
end;
end;
theorem Th6:
n >= len p implies p/^n={}
proof
assume n>=len p;
then len p-'n=0 by NAT_2:8;
then len (p/^n)=0 by Def2;
hence thesis;
end;
theorem Th7:
n < len p implies len (p/^n) = len p -n
proof
assume n < len p;
then len p-'n=len p-n by XREAL_0:def 2,XREAL_1:48;
hence thesis by Def2;
end;
theorem Th8:
m+n one-to-one;
coherence
proof
let x,y be object;
assume that
A1: x in dom (f/^n) and
A2: y in dom (f/^n) and
A3: (f/^n).x=(f/^n).y;
reconsider nx=x,ny=y as Nat by A1,A2;
A4: nxlen f;
then f/^n={} by Th6;
hence thesis by A1;
end;
end;
end;
theorem Th9:
rng (p/^n) c= rng p
proof
thus rng (p/^n) c= rng p
proof
let z be object;
assume z in rng (p/^n);
then consider x being object such that
A1: x in dom (p/^n) and
A2: z=(p/^n).x by FUNCT_1:def 3;
reconsider nx=x as Element of NAT by A1;
nx=len p;
then (p/^n)={} by Th6;
hence thesis by A1;
end;
end;
end;
theorem Th10: ::FINSEQ_5:31
p/^0 = p
proof
per cases;
suppose
A1: 0 =len p;
then p/^0 ={} by Th6;
hence thesis by A3;
end;
end;
theorem Th11: ::FINSEQ_5:39
(p^q)/^(len p + i) = q/^i
proof
A1: len(p^q) = len p + len q by AFINSQ_1:17;
per cases;
suppose
A2: i < len q;
then len p + i < len p + len q by XREAL_1:6;
then len p +i= len q;
hence (p^q)/^(len p+i) = {} by Th6,A1,XREAL_1:6
.= q/^i by A7,Th6;
end;
end;
theorem Th12: ::FINSEQ_5:40
(p^q)/^(len p) = q
proof
thus (p^q)/^(len p) = (p^q)/^(len p + (0 qua Element of NAT))
.= q/^0 by Th11
.= q by Th10;
end;
theorem Th13: ::RFINSEQ:21
(p|n)^(p/^n) = p
proof
set pn = p/^n;
now
per cases;
case
A1: len p<=n;
p/^n = {} by A1,Th6;
hence thesis by A1,AFINSQ_1:52;
end;
case
A2: n empty;
coherence;
let n be Nat;
cluster f/^(dom f + n) -> empty;
coherence
proof
len f <= len f + n + 0 by NAT_1:11; then
(len f) - (len f + n) <= 0 by XREAL_1:20; then
(len f) -' (len f + n) = 0 by XREAL_0:def 2; then
len (f/^(dom f + n)) = 0 by Def2;
hence thesis;
end;
reduce f|(len f + n) to f;
reducibility
proof
len f + n >= len f + 0 by XREAL_1:6;
hence thesis by AFINSQ_1:52;
end;
reduce (f|n)^(f/^n) to f;
reducibility by Th13;
end;
registration
let D be set, f be XFinSequence of D, n;
cluster f /^ n -> D -valued;
coherence
proof
deffunc F(Element of NAT)=f.($1+n);
set p = f /^ n;
per cases;
suppose
A1: nD by Th6;
hence thesis;
end;
end;
end;
reserve k1,k2 for Nat;
definition
let p,k1,k2;
func mid(p,k1,k2) -> XFinSequence equals
(p|k2)/^(k1-'1);
coherence;
end;
theorem Th14:
k1>k2 implies mid(p,k1,k2) = {}
proof
set k21=k2;
A1: len (p|k21)<=k21 by AFINSQ_1:55;
assume
A2: k1>k2;
then k1>= (0 qua Nat) +1 by NAT_1:13;
then
A3: k1-'1=k1-1 by XREAL_1:233;
k1>=k2+1 by A2,NAT_1:13;
then k1-1>=k2+1-1 by XREAL_1:9;
hence thesis by A3,A1,Th6,XXREAL_0:2;
end;
theorem
1<=k1 & k2<=len p implies mid(p,k1,k2) = (p/^(k1-'1))|(k2+1-'k1)
proof
assume that
A1: 1<=k1 and
A2: k2<=len p;
set k11=k1,k21=k2;
A3: len (p|k21)=k21 by A2,AFINSQ_1:54;
k1k2;
then k2+1<=k1 by NAT_1:13;
then
A18: k2+1-'k1=0 by NAT_2:8;
mid(p,k1,k2)={} by A17,Th14;
hence thesis by A18;
end;
end;
theorem Th16: :: FINSEQ_8:5
mid(p,1,k)=p|k
proof
1-'1=0 by XREAL_1:232;
hence thesis by Th10;
end;
theorem :: FINSEQ_8:6
len p<=k implies mid(p,1,k)=p
proof
assume
A1: len p<=k;
thus mid(p,1,k)=p|k by Th16
.=p by A1,AFINSQ_1:52;
end;
theorem :: FINSEQ_8:8
mid(p,0,k)=mid(p,1,k)
proof
A1: 0-'1=0 by NAT_2:8;
mid(p,1,k) = (p|k) by Th16;
hence thesis by A1,Th10;
end;
theorem :: FINSEQ_8:9
mid(p^q,len p+1,len p+len q)=q
proof
A1: (len p +1)-'1=len p by NAT_D:34;
len (p^q)=len p + len q by AFINSQ_1:17;
hence thesis by A1,Th12;
end;
registration
let D be set, f be XFinSequence of D, k1,k2;
cluster mid(f,k1,k2) -> D-valued;
coherence;
end;
begin :: Selected Subsequences
definition
let X be finite natural-membered set;
func Sgm0 X -> XFinSequence of NAT means :Def4:
rng it = X & for l,m,k1,k2 being Nat st
l < m & m < len it & k1=it.l & k2=it.m holds k1 < k2;
existence
proof
defpred P[Nat] means for X being set st X c= Segm $1
ex p being XFinSequence of
NAT st rng p = X & for l,m,k1,k2 being Nat st ( l < m & m < len p & k1=p.l & k2
=p.m) holds k1 < k2;
A1: ex k being Nat st X c= Segm k by Th2;
A2: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A3: for X being set st X c= Segm k
ex p being XFinSequence of NAT
st rng p = X & for l,m,k1,k2 be Nat st l < m & m < len p & k1=p.l & k2=p.m
holds k1 < k2;
let X be set;
assume
A4: X c= Segm(k+1);
now
set Y=X\{k};
assume not X c= k;
then consider x being object such that
A5: x in X and
A6: not x in Segm k;
reconsider n=x as Element of NAT by A4,A5,Th1;
nk by TARSKI:def 1;
m;
A16: for l,m,k1,k2 be Nat st l < m & m < len q & k1=q.l & k2=q.m holds
k1 < k2
proof
let l,m,k1,k2 be Nat;
assume that
A17: l < m and
A18: m < len q and
A19: k1=q.l and
A20: k2=q.m;
m+1<=len q by A18,NAT_1:13;
then
A21: m<=len q -1 by XREAL_1:19;
then l < len (p^<% k %>) -1 by A15,A17,XXREAL_0:2;
then l < len p + len <% k %> -1 by AFINSQ_1:17;
then l < len p + 1 -1 by AFINSQ_1:34;
then
A22: l in dom p by AFINSQ_1:86;
A23: m<=len q-'1 by A21,XREAL_0:def 2;
A24: now
A25: k1 = p.l by A15,A19,A22,AFINSQ_1:def 3;
assume m <> len q -'1;
then m < len (p^<% k %>) -'1 by A15,A23,XXREAL_0:1;
then m < len p + len <% k %> -'1 by AFINSQ_1:17;
then m < len p + 1 -'1 by AFINSQ_1:34;
then
A26: m < len p by NAT_D:34;
then m in dom p by AFINSQ_1:86;
then k2 = p.m by A15,A20,AFINSQ_1:def 3;
hence thesis by A14,A17,A26,A25;
end;
now
assume m=len q -'1;
then
A27: q.m = (p^<% k %>).((len p + len <% k %>)-'1) by A15,AFINSQ_1:17
.= (p^<% k %>).((len p + 1)-'1) by AFINSQ_1:34
.=(p^<% k %>).(len p) by NAT_D:34
.= k by AFINSQ_1:36;
k1 = p.l by A15,A19,A22,AFINSQ_1:def 3;
then k1 in Y by A13,A22,FUNCT_1:def 3;
hence thesis by A9,A20,A27,NAT_1:44;
end;
hence thesis by A24;
end;
A28: {k} c= X by A5,A8,ZFMISC_1:31;
rng q = rng p \/ rng <% k %> by A15,AFINSQ_1:26
.= Y \/ {k} by A13,AFINSQ_1:33
.= X \/ {k} by XBOOLE_1:39
.= X by A28,XBOOLE_1:12;
hence thesis by A16;
end;
hence thesis by A3;
end;
A29: P[0]
proof
let X be set;
assume
A30: X c= Segm 0;
take <%>(NAT);
thus rng <%>(NAT) = X by A30;
thus thesis;
end;
for k2 being Nat holds P[k2] from NAT_1:sch 2(A29,A2);
hence thesis by A1;
end;
uniqueness
proof
defpred S[XFinSequence] means for X st ex k being Nat st X c= k holds ($1
is XFinSequence of NAT & rng $1 = X & for l,m,k1,k2 being Nat st ( l < m & m <
len $1 & k1=$1.l & k2=$1.m) holds k1 < k2) implies for q being XFinSequence of
NAT st rng q = X & for l,m,k1,k2 being Nat st ( l < m & m < len q & k1=q.l & k2
=q.m) holds k1 < k2 holds q=$1;
let p,q be XFinSequence of NAT such that
A31: rng p = X and
A32: for l,m,k1,k2 being Nat st l < m & m < len p & k1=p.l & k2=p.m
holds k1 < k2 and
A33: rng q = X and
A34: for l,m,k1,k2 being Nat st l < m & m < len q & k1=q.l & k2=q.m
holds k1 < k2;
A35: for p being XFinSequence,x be object st S[p] holds S[p^<% x %>]
proof
let p be XFinSequence,x be object;
assume
A36: S[p];
let X be set;
given k being Nat such that
A37: X c= k;
assume that
A38: p^<% x %> is XFinSequence of NAT and
A39: rng (p^<% x %>) = X and
A40: for l,m,k1,k2 being Nat st l < m & m < len(p^<%x%>) & k1=(p^<%
x %>).l & k2=(p^<% x %>).m holds k1 < k2;
let q be XFinSequence of NAT;
assume that
A41: rng q = X and
A42: for l,m,k1,k2 being Nat st l < m & m < len q & k1=q.l & k2=q.m
holds k1 < k2;
deffunc F(Nat) = q.$1;
len q <> 0
proof
assume len q = 0;
then p^<%x%> = {} by A39,A41,AFINSQ_1:15,RELAT_1:38;
then 0 = len (p^<%x%>)
.= len p + len <%x%> by AFINSQ_1:17
.= 1 + len p by AFINSQ_1:34;
hence contradiction;
end;
then consider n be Nat such that
A43: len q = n+1 by NAT_1:6;
A44: ex m being Nat st m=x & for l being Nat st l in X & l <> x holds l
< m
proof
<%x%> is XFinSequence of NAT by A38,AFINSQ_1:31;
then rng <%x%> c= NAT by RELAT_1:def 19;
then {x} c= NAT by AFINSQ_1:33;
then reconsider m=x as Element of NAT by ZFMISC_1:31;
take m;
thus m=x;
thus for l being Nat st l in X & l <> x holds l < m
proof
len <%x%>=1 by AFINSQ_1:34;
then
A45: m= (p^<%x%>).(len p + len <%x%> -1) by AFINSQ_1:36
.= (p^<%x%>).(len(p^<%x%>) -1) by AFINSQ_1:17;
len(p^<%x %>)) +1 by XREAL_1:29;
then
A46: len(p^<%x%>)-1 < len(p^<%x %>) by XREAL_1:19;
let l be Nat;
assume that
A47: l in X and
A48: l <> x;
consider y being object such that
A49: y in dom (p^<%x%>) and
A50: l=(p^<%x%>).y by A39,A47,FUNCT_1:def 3;
reconsider k=y as Element of NAT by A49;
k < len (p^<%x%>) by A49,AFINSQ_1:86;
then k < len p + len <%x%> by AFINSQ_1:17;
then k < len p + 1 by AFINSQ_1:34;
then
A51: k<=len p by NAT_1:13;
k <> len p by A48,A50,AFINSQ_1:36;
then k< len p +1-1 by A51,XXREAL_0:1;
then k < len p + len <%x%>-1 by AFINSQ_1:34;
then
A52: k < len(p^<%x%>)-1 by AFINSQ_1:17;
then len(p^<%x %>) -'1=len(p^<%x %>)-1 by XREAL_0:def 2;
hence thesis by A40,A50,A52,A46,A45;
end;
end;
then reconsider m = x as Nat;
A53: not x in rng p
proof
len p + 1 = len p + len <%x%> by AFINSQ_1:34
.= len (p^<%x%>) by AFINSQ_1:17;
then
A54: len p < len (p^<%x%>) by XREAL_1:29;
A55: m = (p^<%x%>).(len p ) by AFINSQ_1:36;
assume x in rng p;
then consider y being object such that
A56: y in dom p and
A57: x=p.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A56;
A58: y < len p by A56,AFINSQ_1:86;
m = (p^<%x%>).y by A56,A57,AFINSQ_1:def 3;
hence contradiction by A40,A58,A54,A55;
end;
A59: for z being object holds z in rng p \/ {x} \ {x} iff z in rng p
proof
let z be object;
thus z in rng p \/ {x} \ {x} implies z in rng p
proof
assume
A60: z in rng p \/ {x} \ {x};
then not z in {x} by XBOOLE_0:def 5;
hence thesis by A60,XBOOLE_0:def 3;
end;
assume
A61: z in rng p;
then
A62: z in rng p \/ {x} by XBOOLE_0:def 3;
not z in {x} by A53,A61,TARSKI:def 1;
hence thesis by A62,XBOOLE_0:def 5;
end;
deffunc Q(set) =q.$1;
consider q9 being XFinSequence such that
A63: len q9 = n and
A64: for m be Nat st m in n holds q9.m = Q(m)
from AFINSQ_1:sch 2;
now
let x be object;
assume x in rng q9;
then consider y being object such that
A65: y in dom q9 and
A66: x=q9.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A65;
q.y in NAT;
hence x in NAT by A63,A64,A65,A66;
end;
then rng q9 c= NAT;
then reconsider f=q9 as XFinSequence of NAT by RELAT_1:def 19;
A67: p is XFinSequence of NAT by A38,AFINSQ_1:31;
A68: for m be Nat st m in dom <%x%> holds q.(len q9 + m)
= <%x%>.m
proof
let m be Nat;
assume m in dom <%x%>;
then m in len <%x%>;
then
A69: m in 1 by AFINSQ_1:34;
Segm(0+1)= Segm 0 \/ {0} by AFINSQ_1:2;
then
A70: m=0 by A69,TARSKI:def 1;
q.(len q9 + m) = x
proof
x in {x} by TARSKI:def 1;
then x in rng <%x%> by AFINSQ_1:33;
then x in rng p \/ rng <%x%> by XBOOLE_0:def 3;
then x in rng q by A39,A41,AFINSQ_1:26;
then consider y being object such that
A71: y in dom q and
A72: x=q.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A71;
y+1<=len q by NAT_1:13,A71,AFINSQ_1:86;
then
A73: y <= len q -1 by XREAL_1:19;
len qx holds l x;
then k < d by A43,A63,A70,A77,A74;
hence contradiction by A42,A43,A76,A72,A75;
end;
hence thesis by A70;
end;
A78: dom q = (len q9 + len <%x%>) by A43,A63,AFINSQ_1:34;
then
A79: q9^<%x%> = q by A63,A64,A68,AFINSQ_1:def 3;
A80: not x in rng f
proof
len f + 1 = len f + len <%x%> by AFINSQ_1:34
.= len (f^<%x%>) by AFINSQ_1:17;
then
A81: len f < len (f^<%x%>) by XREAL_1:29;
A82: m = q.(len f) by A79,AFINSQ_1:36;
assume x in rng f;
then consider y being object such that
A83: y in dom f and
A84: x=f.y by FUNCT_1:def 3;
reconsider y as Element of NAT by A83;
A85: y < len f by A83,AFINSQ_1:86;
m = q.y by A63,A64,A83,A84;
hence contradiction by A42,A79,A85,A81,A82;
end;
A86: for z being object holds z in rng f \/ {x} \ {x} iff z in rng f
proof
let z be object;
thus z in rng f \/ {x} \ {x} implies z in rng f
proof
assume
A87: z in rng f \/ {x} \ {x};
then not z in {x} by XBOOLE_0:def 5;
hence thesis by A87,XBOOLE_0:def 3;
end;
assume
A88: z in rng f;
then
A89: z in rng f \/ {x} by XBOOLE_0:def 3;
not z in {x} by A80,A88,TARSKI:def 1;
hence thesis by A89,XBOOLE_0:def 5;
end;
X = rng p \/ rng <%x%> by A39,AFINSQ_1:26
.= rng p \/ {x} by AFINSQ_1:33;
then
A90: rng p = X\{x} by A59,TARSKI:2;
A91: for l,m,k1,k2 being Nat st l < m & m < len p & k1=p.l & k2=p.m
holds k1 < k2
proof
let l,m,k1,k2 be Nat;
assume that
A92: l < m and
A93: m < len p and
A94: k1=p.l and
A95: k2=p.m;
l < len p by A92,A93,XXREAL_0:2;
then l in dom p by AFINSQ_1:86;
then
A96: k1 = (p^<%x%>).l by A94,AFINSQ_1:def 3;
len p < len p + 1 by XREAL_1:29;
then m < len p + 1 by A93,XXREAL_0:2;
then m < len p + len <%x%> by AFINSQ_1:34;
then
A97: m < len (p^<%x%>) by AFINSQ_1:17;
m in dom p by A93,AFINSQ_1:86;
then k2 = (p^<%x%>).m by A95,AFINSQ_1:def 3;
hence thesis by A40,A92,A96,A97;
end;
A98: for l,m,k1,k2 being Nat st l < m & m < len f & k1=f.l & k2=f.m
holds k1 < k2
proof
let l,m,k1,k2 be Nat;
assume that
A99: l < m and
A100: m < len f and
A101: k1=f.l and
A102: k2=f.m;
A103: k2 = q.m by A64,A102,A63,A100,AFINSQ_1:86;
l < n by A63,A99,A100,XXREAL_0:2;
then l in Segm n by NAT_1:44;
then
A104: k1 = q.l by A64,A101;
m < len q by A43,A63,A100,NAT_1:13;
hence thesis by A42,A99,A104,A103;
end;
X = rng f \/ rng <%x%> by A41,A79,AFINSQ_1:26
.= rng f \/ {x} by AFINSQ_1:33;
then
A105: rng f = X\{x} by A86,TARSKI:2;
ex m being Nat st X\{x} c= m by A37,XBOOLE_1:1;
then q9 = p by A36,A91,A67,A90,A98,A105;
hence thesis by A63,A64,A78,A68,AFINSQ_1:def 3;
end;
A106: S[{}];
A107: for p being XFinSequence holds S[p] from AFINSQ_1:sch 3(A106,A35);
ex k being Nat st X c= Segm k by Th2;
hence thesis by A31,A32,A33,A34,A107;
end;
end;
registration
let A be finite natural-membered set;
cluster Sgm0 A -> one-to-one;
coherence
proof
for x,y being object st x in dom(Sgm0 A) & y in dom(Sgm0 A) & (Sgm0(A)).x
= (Sgm0(A)).y & x<>y holds contradiction
proof
let x,y be object;
assume that
A1: x in dom(Sgm0 A) and
A2: y in dom(Sgm0 A) and
A3: (Sgm0(A)).x = (Sgm0(A)).y and
A4: x <> y;
reconsider i = x, j = y as Element of NAT by A1,A2;
per cases by A4,XXREAL_0:1;
suppose
A5: i < j;
j < len(Sgm0 A) by A2,AFINSQ_1:86;
hence contradiction by A3,A5,Def4;
end;
suppose
A6: j < i;
i < len(Sgm0 A) by A1,AFINSQ_1:86;
hence contradiction by A3,A6,Def4;
end;
end;
hence thesis;
end;
end;
theorem Th20: :: FINSEQ_3:44
for A being finite natural-membered set holds len(Sgm0 A) = card A
proof
let A be finite natural-membered set;
rng(Sgm0 A) = A by Def4;
then (len(Sgm0 A)),A are_equipotent by WELLORD2:def 4;
then card A = card((len(Sgm0 A))) by CARD_1:5;
hence thesis;
end;
theorem Th21:
for X,Y being finite natural-membered set st X c= Y & X <> {}
holds (Sgm0 Y).0 <= (Sgm0 X).0
proof
let X,Y be finite natural-membered set;
assume that
A1: X c= Y and
A2: X <> {};
reconsider X0=X as finite set;
0 <> card X0 by A2;
then 0 < len (Sgm0 X) by Th20;
then
A3: 0 in dom (Sgm0 X) by AFINSQ_1:86;
A4: rng (Sgm0 Y)=Y by Def4;
rng (Sgm0 X)=X by Def4;
then (Sgm0 X).0 in X by A3,FUNCT_1:def 3;
then consider x being object such that
A5: x in dom (Sgm0 Y) and
A6: (Sgm0 Y).x=(Sgm0 X).0 by A1,A4,FUNCT_1:def 3;
reconsider nx=x as Nat by A5;
A7: nx nx;
hence thesis by A6,A7,Def4;
end;
case
0=nx;
hence thesis by A6;
end;
end;
hence thesis;
end;
theorem Th22:
(Sgm0 {n}).0=n
proof
len (Sgm0 {n})=card {n} by Th20;
then 0 in dom (Sgm0 {n}) by AFINSQ_1:86;
then
A1: (Sgm0 {n}).0 in rng (Sgm0 {n}) by FUNCT_1:def 3;
rng (Sgm0 {n})={n} by Def4;
hence thesis by A1,TARSKI:def 1;
end;
definition
let B1,B2 be set;
pred B1 {};
then
A2: x in B1/\B2 by XBOOLE_0:def 4;
then
A3: nx in B2 by XBOOLE_0:def 4;
nx in B1 by A2,XBOOLE_0:def 4;
hence contradiction by A1,A3;
end;
hence thesis;
end;
theorem
for B1,B2 being finite natural-membered set st B1 {} & (ex x being set
st x in X & {x} {} and
A2: ex x being set st x in X & {x} card Y by A1;
then 0 < len (Sgm0 Y) by Th20;
then
A5: 0 in dom (Sgm0 Y) by AFINSQ_1:86;
rng (Sgm0 Y)=Y by Def4;
then
A6: (Sgm0 Y).0 in Y by A5,FUNCT_1:def 3;
reconsider x0=x as Element of NAT by A3,ORDINAL1:def 12;
set nx=x0;
nx in {x0} by TARSKI:def 1;
then
A7: nx<=(Sgm0 Y).0 by A4,A6;
{x0} c= X
by A3,TARSKI:def 1;
then
A8: (Sgm0 X).0 <= (Sgm0 {x0}).0 by Th21;
(Sgm0 {x0}).0=nx by Th22;
hence thesis by A8,A7,XXREAL_0:2;
end;
theorem Th27:
for X0,Y0 being finite natural-membered set st
X0 {} by A2,CARD_1:27,XBOOLE_1:15;
A18: now
assume that
A19: not Z c= X0 and
A20: not X0 c= Z;
consider v1 being object such that
A21: v1 in Z and
A22: not v1 in X0 by A19;
consider v10 being Element of X0 \/Y0 such that
A23: v1=v10 and
A24: ex k2 being Nat st v10=f.k2 & k2 in card X0 by A21;
A25: v10 in Y0 by A17,A22,A23,XBOOLE_0:def 3;
reconsider nv10 =v10 as Nat;
consider v2 being object such that
A26: v2 in X0 and
A27: not v2 in Z by A20;
X0 c= X0\/Y0 by XBOOLE_1:7;
then consider x2 being object such that
A28: x2 in dom f0 and
A29: v2=f0.x2 by A11,A26,FUNCT_1:def 3;
reconsider x20=x2 as Nat by A28;
reconsider nv2 =v2 as Nat by A29;
A30: x20 {} by A2,CARD_1:27,XBOOLE_1:15;
A12: now
assume that
A13: not Z c= X and
A14: not X c= Z;
consider v1 being object such that
A15: v1 in Z and
A16: not v1 in X by A13;
consider v10 being Element of X \/Y such that
A17: v1=v10 and
A18: ex k2 being Nat st v10=f.k2 & k2 in card X by A15;
A19: v10 in Y by A11,A16,A17,XBOOLE_0:def 3;
reconsider nv10 =v10 as Nat;
consider v2 being object such that
A20: v2 in X and
A21: not v2 in Z by A14;
X c= X\/Y by XBOOLE_1:7;
then consider x2 being object such that
A22: x2 in dom f0 and
A23: v2=f0.x2 by A3,A20,FUNCT_1:def 3;
reconsider x20=x2 as Nat by A22;
now
assume x20 < card X;
then
A24: x20 in Segm card X by NAT_1:44;
card X <= card (X \/Y) by NAT_1:43,XBOOLE_1:7;
then card X <= len f0 by Th20;
then f.x20=f0.x20 by A24,AFINSQ_1:53;
hence contradiction by A5,A10,A21,A23,A24,FUNCT_1:def 3;
end;
then
A25: len f <=x20 by A4,AFINSQ_1:54;
consider k20 being Nat such that
A26: v10=f.k20 and
A27: k20 in card X by A18;
A28: f.k20=f0.k20 by A4,A27,AFINSQ_1:53;
reconsider nv2 =v2 as Nat by A23;
k20 {} by A2,CARD_1:27,XBOOLE_1:15;
A22: now
assume that
A23: not Z c= Y0 and
A24: not Y0 c= Z;
consider v2 being object such that
A25: v2 in Y0 and
A26: not v2 in Z by A24;
Y0 c= X0\/Y0 by XBOOLE_1:7;
then consider x2 being object such that
A27: x2 in dom f0 and
A28: v2=f0.x2 by A6,A25,FUNCT_1:def 3;
consider v1 being object such that
A29: v1 in Z and
A30: not v1 in Y0 by A23;
consider v10 being Element of X0 \/Y0 such that
A31: v1=v10 and
A32: ex k2 being Nat st v10=f.k2 & k2 in Segm card Y0 by A29;
A33: v10 in X0 by A21,A30,A31,XBOOLE_0:def 3;
reconsider nv10 =v10 as Nat;
reconsider nv2 =v2 as Nat by A28;
consider k20 being Nat such that
A34: v10=f.k20 and
A35: k20 in Segm card Y0 by A32;
A36: k20+card X0= card X0;
then
A41: x20-'card X0=x20-card X0 by XREAL_1:233;
x20x20 by A39,XXREAL_0:2;
then nv10>nv2 by A34,A28,A36,A37,Def4;
hence contradiction by A1,A25,A33;
end;
A44: now
per cases by A22;
case
Z0 c= Y0;
hence Z0=Y0 by A19,CARD_2:102;
end;
case
Y0 c=Z0;
hence Z0=Y0 by A19,CARD_2:102;
end;
end;
i+card X0 < len f0 by A2,A9,A11,XREAL_1:20;
hence thesis by A15,A12,A44,Th8;
end;
theorem Th31:
for X,Y being finite natural-membered set st X {} & X {} and
A2: X 0 by A1;
then 0 {} & X {} and
A2: X 0 by A1;
then 0 n;
now
per cases;
suppose
A14: k in dom p;
set m1 = r.k;
set n1 = p.k;
now
per cases by A13,XXREAL_0:1;
suppose
A15: m < n;
then not m in Y by A1,A10;
then m in X by A12,XBOOLE_0:def 3;
then m in rng p by Def4;
then consider x being object such that
A16: x in dom p and
A17: p.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A16;
x < len p by A16,AFINSQ_1:86;
then
A18: x < k + 1 by A15,A17,Th33;
A19: k < k + 1 by XREAL_1:29;
k + 1 < len r by A9,A11,AFINSQ_1:86;
then
A20: n1 < m by A8,A14,A19,Def4;
k < len p by A14,AFINSQ_1:86;
then k < x by A17,A20,Th33;
hence contradiction by A18,NAT_1:13;
end;
suppose
A21: n < m;
n in X \/ Y by A10,XBOOLE_0:def 3;
then n in rng r by Def4;
then consider x being object such that
A22: x in dom r and
A23: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A22;
x < len r by A22,AFINSQ_1:86;
then
A24: x < k + 1 by A21,A23,Th33;
A25: k < k + 1 by XREAL_1:29;
k + 1 < len p by A9,AFINSQ_1:86;
then
A26: m1 < n by A8,A14,A25,Def4;
k < len r by A11,A14,AFINSQ_1:86;
then k < x by A23,A26,Th33;
hence contradiction by A24,NAT_1:13;
end;
end;
hence contradiction;
end;
suppose
A27: not k in dom p;
A28: k < k + 1 by XREAL_1:29;
len p <= k by A27,AFINSQ_1:86;
then len p < k + 1 by A28,XXREAL_0:2;
hence contradiction by A9,AFINSQ_1:86;
end;
end;
hence contradiction;
end;
end;
0{} by Th20,CARD_1:27;
then
A29: P[0] by A1,Th34;
A30: for k holds P[k] from NAT_1:sch 2(A29,A7);
defpred P[Nat] means $1 in dom q implies r.(len p + $1) = q.$1;
A31: now
let k;
assume
A32: P[k];
thus P[k+1]
proof
set n = q.(k + 1);
set a = len p + (k + 1);
set m = r.a;
assume
A33: k + 1 in dom q;
then q.(k + 1) in rng q by FUNCT_1:def 3;
then
A34: n in Y by Def4;
k + 1 q.(k + 1);
now
per cases;
suppose
A44: k in dom q;
set m1 = r.(len p + k);
set n1 = q.k;
A45: k < len q by A44,AFINSQ_1:86;
now
per cases by A43,XXREAL_0:1;
suppose
A46: m < n;
m in Y by A37,A38,XBOOLE_0:def 3;
then m in rng q by Def4;
then consider x being object such that
A47: x in dom q and
A48: q.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A47;
x < len q by A47,AFINSQ_1:86;
then
A49: x < k + 1 by A46,A48,Th33;
len p + k < len p + k + 1 by XREAL_1:29;
then
A50: n1 < m by A32,A35,A44,Def4;
k < len q by A44,AFINSQ_1:86;
then k < x by A48,A50,Th33;
hence contradiction by A49,NAT_1:13;
end;
suppose
A51: n < m;
n in X \/ Y by A34,XBOOLE_0:def 3;
then n in rng r by Def4;
then consider x being object such that
A52: x in dom r and
A53: r.x = n by FUNCT_1:def 3;
reconsider x as Element of NAT by A52;
x < len r by A52,AFINSQ_1:86;
then
A54: x < len p + k + 1 by A51,A53,Th33;
A55: k < k + 1 by XREAL_1:29;
k + 1 < len q by A33,AFINSQ_1:86;
then
A56: m1 < n by A32,A44,A55,Def4;
len p + k < len r by A6,A45,XREAL_1:6;
then len p + k < x by A53,A56,Th33;
hence contradiction by A54,NAT_1:13;
end;
end;
hence contradiction;
end;
suppose
A57: not k in dom q;
A58: k < k + 1 by XREAL_1:29;
len q <= k by A57,AFINSQ_1:86;
hence contradiction by A33,AFINSQ_1:86,A58,XXREAL_0:2;
end;
end;
hence contradiction;
end;
end;
len q>0 implies Y <>{} by Th20,CARD_1:27;
then
A59: P[0] by A1,Th32;
for k holds P[k] from NAT_1:sch 2(A59,A31);
hence thesis by A6,A30,AFINSQ_1:def 3;
end;
assume
A60: Sgm0(X \/ Y) = Sgm0(X) ^ Sgm0(Y);
let m,n be Nat;
assume that
A61: m in X and
A62: n in Y;
n in rng q by A62,Def4;
then consider y being object such that
A63: y in dom q and
A64: q.y = n by FUNCT_1:def 3;
reconsider y as Element of NAT by A63;
A65: n = r.(len p + y) by A60,A63,A64,AFINSQ_1:def 3;
y < len q by A63,AFINSQ_1:86;
then len p + y < len p + len q by XREAL_1:6;
then
A66: len p + y < len r by A60,AFINSQ_1:17;
A67: len p<=len p+y by NAT_1:12;
m in rng(Sgm0 X) by A61,Def4;
then consider x being object such that
A68: x in dom p and
A69: p.x = m by FUNCT_1:def 3;
reconsider x as Element of NAT by A68;
x < len p by A68,AFINSQ_1:86;
then
A70: x < len p + y by A67,XXREAL_0:2;
m = r.x by A60,A68,A69,AFINSQ_1:def 3;
hence thesis by A65,A70,A66,Def4;
end;
definition
let f be XFinSequence;
let B be set;
::Following is a subsequence selected from f by B.
func SubXFinS (f,B) -> XFinSequence equals
f*Sgm0(B /\ Segm len f);
coherence
proof
B/\ Segm len f c= dom f by XBOOLE_1:17;
then rng Sgm0(B/\ Segm len f) c= dom f by Def4;
hence thesis by AFINSQ_1:10;
end;
end;
theorem Th36:
for B being set holds len SubXFinS (p,B)=
card (B/\ Segm(len p)) &
for i st i < len SubXFinS (p,B) holds SubXFinS
(p,B).i=p.((Sgm0 (B/\ Segm(len p))).i)
proof
let B be set;
B/\ Segm len p c= dom p by XBOOLE_1:17;
then rng Sgm0(B/\ Segm len p) c= dom p by Def4;
then dom SubXFinS (p,B) = len Sgm0(B/\ Segm len p) by RELAT_1:27
.= card(B/\ Segm len p) by Th20;
hence len SubXFinS (p,B)=card (B/\ Segm len p);
let i;
assume i < len SubXFinS (p,B);
hence thesis by FUNCT_1:12,AFINSQ_1:86;
end;
registration
let D be set;
let f be XFinSequence of D, B be set;
cluster SubXFinS(f,B) -> D-valued;
coherence;
end;
registration
let p;
cluster SubXFinS (p,{}) -> empty;
coherence
proof
len (SubXFinS (p,{})) =card {} by Th36;
hence thesis;
end;
end;
registration
let B be set;
cluster SubXFinS ({},B) -> empty;
coherence;
end;
:: AFINSQ_2:48 => AFINSQ_2:83
reserve D for non empty set,
F,G for XFinSequence of D,
b for BinOp of D,
d,d1,d2 for Element of D;
scheme
Sch5{D()->set, P[set]}: for F be XFinSequence of D() holds P[F]
provided
A1: P[<%>D()] and
A2: for F be XFinSequence of D(),d be Element of D() st P[F] holds P[F^<%d%>]
proof
defpred R[set] means for F be XFinSequence of D() st len F = $1 holds P[F];
A3: for n st R[n] holds R[n+1]
proof
let n such that
A4: for F be XFinSequence of D() st len F=n holds P[F];
let F be XFinSequence of D();
assume
A5: len F = n + 1;
then F <>{};
then consider G be XFinSequence, d be object such that
A6: F = G^<%d%> by AFINSQ_1:40;
reconsider G,dd=<%d%> as XFinSequence of D() by A6,AFINSQ_1:31;
A7:rng dd c= D() & rng dd = {d} & d in {d}
by AFINSQ_1:33,TARSKI:def 1;
len dd = 1 by AFINSQ_1:34;
then len F = len G + 1 by A6,AFINSQ_1:17;
hence thesis by A2,A4,A5,A6,A7;
end;
let F be XFinSequence of D();
A8: len F=len F;
card X = {} implies X = {};
then
A9: R[0] by A1;
for n holds R[n] from NAT_1:sch 2(A9,A3);
hence thesis by A8;
end;
definition
let D;
let F be XFinSequence;
assume A1:F is D-valued;
let b;
assume A2: b is having_a_unity or len F >= 1;
func b "**" F -> Element of D means :Def8: :: STIRL2_1:def 3
it = the_unity_wrt b if b is having_a_unity & len F = 0
otherwise ex f be sequence of D st f.0 = F.0 &
(for n st n+1 < len F holds f.(n + 1) = b.(f.n,F.(n + 1))) &
it = f.(len F-1);
existence
proof
now
per cases;
suppose
len F = 0;
hence thesis by A2;
end;
suppose
A3: len F <> 0;
defpred P[Nat] means for F st len F = $1 & len F <> 0 ex d
be Element of D,f be sequence of D st f.0 = F.0 & (for n st n+1 < len F
holds f.(n + 1) = b.(f.n,F.(n + 1))) & d = f.(len F-1);
A4: for k st P[k] holds P[k + 1]
proof
let k such that
A5: P[k];
let F such that
A6: len F = k + 1 and
len F <> 0;
set G = F|k;
A7: k < k+1 by NAT_1:13;
then
A8: len G = k by A6,AFINSQ_1:11;
now
per cases;
suppose
A9: len G = 0;
then 0 in dom F by A6,A8,CARD_1:49,TARSKI:def 1;
then
A10: F.0 in rng F by FUNCT_1:def 3;
reconsider f = NAT --> F.0 as sequence of D by A10,
FUNCOP_1:45;
take d = f.0,f;
thus f.0 = F.0 by FUNCOP_1:7;
thus for n st n+1 < len F holds f.(n + 1) = b.(f.n,F.(n + 1)) by
A6,A8,A9,NAT_1:14;
k 0;
k < len F by A6,NAT_1:13;
then k in dom F by AFINSQ_1:86;
then
A12: F.k in rng F by FUNCT_1:def 3;
reconsider d1 = F.k as Element of D by A12;
A13: 0 in len G by A11,AFINSQ_1:86;
consider d be Element of D,f be sequence of D such that
A14: f.0 = G.0 and
A15: for n st n+1 K holds h.n = F(n) from
FUNCT_2:sch 6;
take a = h.k, h;
h.0=f.0 by A8,A11,A18;
hence h.0 =F.0 by A14,A13,FUNCT_1:47;
thus for n st n+1 < len F holds h.(n + 1) = b.(h.n,F.(n + 1))
proof
let n;
assume n+1 < len F;
then
A19: n+1 <= len G by A6,A8,NAT_1:13;
now
per cases by A19,XXREAL_0:1;
suppose
A20: n+1 = len G;
then
A21: n 0;
then 0< len F by A2;
then
A27: len F-1 is Element of NAT by NAT_1:20;
given f1 be sequence of D such that
A28: f1.0 = F.0 and
A29: for n st n+1 = d
proof
len<%d%> = 1 by AFINSQ_1:33;
then ex f be sequence of D st f.0=<%d%>.0& (for n st n+1 < len <%d%>
holds f.(n+1) = b.(f.n,<%d%>.(n+1)))& b "**" <%d%>=f.(1-1) by Def8;
hence thesis;
end;
reconsider zz=0 as Nat;
theorem Th38:
b "**" <%d1,d2%> = b.(d1,d2)
proof
len <%d1,d2%>=2 by AFINSQ_1:38;
then consider f be sequence of D such that
A1: f.0 = <%d1,d2%>.0 and
A2: for n st n+1 < 2 holds f.(n + 1) = b.(f.n,<%d1,d2%>.(n + 1)) and
A3: b "**" <%d1,d2%> = f.(2-1) by Def8;
f.(zz+1)=b.(f.zz,<%d1,d2%>.(zz+1)) by A2;
hence thesis by A1,A3;
end;
theorem Th39:
b "**" <%d,d1,d2%> = b.(b.(d,d1),d2)
proof
set F=<%d,d1,d2%>;
len F=3 by AFINSQ_1:39;
then consider f be sequence of D such that
A1: f.0 = F.0 and
A2: for n st n+1 < 3 holds f.(n + 1) = b.(f.n,F.(n + 1)) and
A3: b "**" F = f.(3-1) by Def8;
A4: f.(1+1)=b.(f.1,F.(1+1)) by A2;
f.(zz+1)=b.(f.zz,F.(zz+1)) by A2;
hence thesis by A1,A3,A4;
end;
theorem Th40: :: STIRL2_1:45
b is having_a_unity or len F > 0 implies b "**" (F ^ <% d %>) =
b.(b "**" F,d)
proof
assume
A1: b is having_a_unity or len F > 0;
now
per cases;
suppose
A2: len F)=d by Th37,A3;
len F=0 by A2,NAT_1:13;
then b "**" F = the_unity_wrt b by A1,Def8;
hence thesis by A1,A2,A4,NAT_1:13,SETWISEO:15;
end;
suppose
A5: len F>=1;
set G = F ^ <% d %>;
reconsider lenF1=len F-1 as Element of NAT by A5,NAT_1:21;
A6: G.(len F)=d by AFINSQ_1:36;
A7: len G=len F+len <%d%> by AFINSQ_1:17
.=len F+1 by AFINSQ_1:33;
then 1 <= len G by NAT_1:12;
then consider f1 be sequence of D such that
A8: f1.0 = G.0 and
A9: for n st n+1 < len G holds f1.(n+1)=b.(f1.n,G.(n+1)) and
A10: b "**" G = f1.(len G-1) by Def8;
consider f be sequence of D such that
A11: f.0 = F.0 and
A12: for n st n+1 < len F holds f.(n+1)=b.(f.n,F.(n+1)) and
A13: b "**" F = f.(len F-1) by A5,Def8;
defpred P[Nat] means $1+1 < len G implies f.$1 = f1.$1;
A14: P[n] implies P[n + 1]
proof
assume
A15: P[n];
set n1=n+1;
assume
A16: n1+1= 1 & len G >= 1)
implies b "**" (F ^ G) = b.(b "**" F,b "**" G)
proof
defpred P[XFinSequence of D] means for F,b st b is associative & (b is
having_a_unity or len F >= 1 & len $1 >= 1) holds b "**" (F^$1)=b.(b "**" F,b
"**" $1);
A1: for G,d st P[G] holds P[G ^ <%d%>]
proof
let G,d such that
A2: P[G];
let F,b such that
A3: b is associative and
A4: b is having_a_unity or len F >= 1 & len(G ^ <% d %>) >= 1;
now
per cases;
suppose
A5: len G<>0;
then
b is having_a_unity or len F>=1&len (F^G)=len F+len G & len F+len
G >len F+zz by A4,AFINSQ_1:17,XREAL_1:8;
then b.(b "**" (F ^ G),d)=b "**" ((F ^ G)^<%d%>) by Th40;
then
A6: b "**" (F ^ (G ^ <% d %>)) = b.(b "**" (F ^ G),d) by AFINSQ_1:27;
len G>=1 by A5,NAT_1:14;
then b "**" (F ^ (G ^ <% d %>))=b.(b.(b "**" F,b "**" G),d) by A2,A3,A4
,A6
.= b.(b "**" F,b.(b "**" G,d)) by A3
.= b.(b "**" F,b "**" (G ^ <% d %>)) by A5,Th40;
hence thesis;
end;
suppose
len G=0;
then
A7: G = {};
hence b "**" (F ^(G ^ <% d %>))
= b "**"(F^({}^<% d %>))
.= b "**"(F^<% d %>)
.= b.(b "**" F,d) by A4,Th40
.= b.(b "**" F,b "**" ({}^<%d%>)) by Th37
.= b.(b "**" F,b "**" (G ^ <% d %>)) by A7;
end;
end;
hence thesis;
end;
A8: P[<%>D]
proof
let F,b;
assume that
b is associative and
A9: b is having_a_unity or len F >= 1 & len <%>D >= 1;
thus b "**" (F ^ <%>D) = b "**" (F^{})
.= b.(b "**" F,the_unity_wrt b) by A9,SETWISEO:15
.= b.(b "**" F,b "**" <%>D) by A9,Def8,CARD_1:27;
end;
for G holds P[G] from Sch5(A8,A1);
hence thesis;
end;
theorem Th42: :: CARD_FIN:42
n in dom F & (b is having_a_unity or n <> 0 ) implies
b.(b "**" F|n, F.n) = b "**" F|(n+1)
proof
assume that
A1: n in dom F and
A2: b is having_a_unity or n <> 0;
len F>n by A1,AFINSQ_1:86;
then
A3: len (F|n)=n by AFINSQ_1:54;
defpred P[Nat] means $1 in dom F & (b is having_a_unity or len (F
|$1) >= 1) implies b.(b "**" F|$1, F.$1) = b "**" F|($1+1);
A4: for k st P[k] holds P[k+1]
proof
let k such that P[k];
set k1=k+1;
set Fk1=F|k1;
set Fk2=F|(k1+1);
assume that
A5: k1 in dom F and
A6: b is having_a_unity or len Fk1 >= 1;
0 < len F by A5;
then
A7: 0 in dom F by AFINSQ_1:86;
0 in Segm k1 by NAT_1:44;
then 0 in dom F/\k1 by A7,XBOOLE_0:def 4;
then 0 in dom Fk1 by RELAT_1:61;
then
A8: Fk1.0=F.0 by FUNCT_1:47;
A9: k= 1 by A6,A13,NAT_1:13;
then consider f2 be sequence of D such that
A18: f2.0 = Fk2.0 and
A19: for n st n+1 < len Fk2 holds f2.(n+1) = b.(f2.n,Fk2.(n+1)) and
A20: b "**" Fk2= f2.((k1+1)-1) by A17,Def8;
defpred R[Nat] means $1 < k1 implies f1.$1=f2.$1;
A21: for m st R[m] holds R[m+1]
proof
let m such that
A22: R[m];
set m1=m+1;
assume
A23: m1 < k1;
k1< len F by A5,AFINSQ_1:86;
then m1 < len F by A23,XXREAL_0:2;
then
A24: m1 in dom F by AFINSQ_1:86;
m1 = 1;
A32: F.0 in rng F by A30,FUNCT_1:def 3;
len F>0 by A30;
then
A33: len (F|1)=1 by AFINSQ_1:54,NAT_1:14;
then
A34: (F|1)=<%(F|1).0%> by AFINSQ_1:34;
0 in Segm 1 by NAT_1:44;
then
A35: F.0=(F|1).0 by A33,FUNCT_1:47;
len (F|(0 qua Ordinal))=0;
then b "**" F|(0 qua Ordinal)=the_unity_wrt b by A31,Def8;
then b.(b "**" F|(0 qua Ordinal), F.0)=F.0 by A31,A32,SETWISEO:15;
hence thesis by A32,A34,A35,Th37;
end;
for k holds P[k] from NAT_1:sch 2(A29,A4);
hence thesis by A1,A2,A3,NAT_1:14;
end;
theorem Th43: :: CARD_FIN:47
b is having_a_unity or len F >= 1 implies b "**" F = b "**" (XFS2FS F)
proof
assume
A1: b is having_a_unity or len F >= 1;
per cases by A1;
suppose
A2: len F >=1;
set FS=XFS2FS F;
len F=len FS by AFINSQ_1:def 9;
then consider f be sequence of D such that
A3: f.1 = FS.1 and
A4: for n be Nat st 0<>n & n= 1) &
G = F * P holds b "**" F = b "**" G
proof
let P be Permutation of dom F such that
A1: b is commutative associative and
A2: b is having_a_unity or len F >= 1 and
A3: G = F * P;
set xF=XFS2FS F;
A4: b is having_a_unity or len xF >= 1 by A2,AFINSQ_1:def 9;
set xG=XFS2FS G;
defpred p[object,object] means for n st $1=n holds $2=P.(n-1)+1;
dom F=len F;
then reconsider d=dom F as Element of NAT;
A6: for x being object st x in Seg d ex y being object st y in Seg d & p[x,y]
proof
let x be object such that
A7: x in Seg d;
reconsider x9=x as Element of NAT by A7;
1+zz<=x9 by A7,FINSEQ_1:1;
then reconsider x91=x9-1 as Element of NAT by NAT_1:21;
A8: x91+1<= d by A7,FINSEQ_1:1;
then x91 = 1) &
len F=len G & len F=len bFG &
(for n st n in dom bFG holds bFG.n=b.(F.n,G.n))
holds b "**" F^G = b "**" bFG
proof
let bFG be XFinSequence of D such that
A1: b is commutative associative and
A2: b is having_a_unity or len F >= 1 and
A3: len F=len G and
A4: len F=len bFG and
A5: for n st n in dom bFG holds bFG.n=b.(F.n,G.n);
set xG=XFS2FS G;
set xF=XFS2FS F;
A6: b "**" F=b "**" xF & b "**" G=b "**" xG by A2,A3,Th43;
set xb=XFS2FS bFG;
A7: len xb=len bFG by AFINSQ_1:def 9;
A8: for k be Nat st k in dom xb holds xb.k = b.(xF.k,xG.k)
proof
let k be Nat such that
A9: k in dom xb;
k in Seg len xb by A9,FINSEQ_1:def 3;
then k>=1 by FINSEQ_1:1;
then reconsider k1=k-1 as Element of NAT by NAT_1:21;
A10: k in Seg len xb by A9,FINSEQ_1:def 3;
then
A11: 1<=k by FINSEQ_1:1;
then
A12: k1=k-'1 by XREAL_1:233;
k in Seg len xb by A9,FINSEQ_1:def 3;
then k1= 1 &
D c= D1 /\ D2 &
for x,y st x in D & y in D holds b1.(x,y)=b2.(x,y) & b1.(x,y) in D
holds b1 "**" F = b2 "**" F
proof
let D1,D2 be non empty set;
let b1 be BinOp of D1,b2 be BinOp of D2 such that
A1: len F >= 1 and
A2: D c= D1 /\ D2 and
A3: for x,y st x in D & y in D holds b1.(x,y) = b2.(x,y) & b1.(x,y) in D;
D1/\D2 c= D1 & D1/\D2 c= D2 by XBOOLE_1:17;
then A4:D c= D1 & D c= D2 by A2;
rng F c= D1 & rng F c= D2 by A4;
then A5:F is D1-valued & F is D2-valued by RELAT_1:def 19;
then consider F1 be sequence of D1 such that
A6: F1.0 = F.0 and
A7: for n st n+1 < len F holds F1.(n + 1) = b1.(F1.n,F.(n + 1)) and
A8: b1 "**" F = F1.(len F-1) by A1,Def8;
consider F2 be sequence of D2 such that
A9: F2.0 = F.0 and
A10: for n st n+1 < len F holds F2.(n + 1) = b2.(F2.n,F.(n + 1)) and
A11: b2 "**" F = F2.(len F-1) by A1,Def8,A5;
defpred P[Nat] means $1 < len F implies F1.$1 = F2.$1 & F1.$1 in D;
0 in dom F by A1,AFINSQ_1:86;
then F.0 in rng F by FUNCT_1:def 3;
then
A12:P[0] by A6,A9;
A13: P[n] implies P[n+1]
proof
assume A14:P[n];
assume A15:n+1 < len F;
then n+1 in dom F & n < len F by NAT_1:13,AFINSQ_1:86;
then A16:F.(n+1) in rng F & n in dom F by FUNCT_1:def 3,AFINSQ_1:86;
A17:F1.(n + 1) = b1.(F1.n,F.(n + 1)) by A7,A15;
then F1.(n + 1)= b2.(F2.n,F.(n + 1)) by A3,A16,A14,AFINSQ_1:86
.=F2.(n+1) by A10,A15;
hence thesis by A16,A14,A17,A3,AFINSQ_1:86;
end;
reconsider l1=len F-1 as Element of NAT by A1,NAT_1:21;
A18:l1 < l1+1 by NAT_1:13;
P[n] from NAT_1:sch 2(A12,A13);
hence thesis by A8,A11,A18;
end;
reserve F for XFinSequence,
rF,rF1,rF2 for real-valued XFinSequence,
r for Real,
cF,cF1,cF2 for complex-valued XFinSequence,
c,c1,c2 for Complex;
Lm2:cF is COMPLEX -valued
proof
rng cF c= COMPLEX by VALUED_0:def 1;
hence thesis by RELAT_1:def 19;
end;
Lm3:rF is REAL -valued
proof
rng rF c= REAL by VALUED_0:def 3;
hence thesis by RELAT_1:def 19;
end;
definition
let F;
func Sum F ->Element of COMPLEX equals
addcomplex "**" F;
coherence;
end;
registration
let f be empty complex-valued XFinSequence;
cluster Sum f -> zero;
coherence
proof
f is COMPLEX-valued & len f = 0 by Lm2;
hence thesis by Def8,BINOP_2:1;
end;
end;
theorem Th47:
F is real-valued implies Sum F = addreal "**" F
proof
assume A1:F is real-valued;
then rng F c= REAL by VALUED_0:def 3;
then A2:F is REAL-valued by RELAT_1:def 19;
rng F c= COMPLEX by A1,MEMBERED:1;
then A3:F is COMPLEX-valued by RELAT_1:def 19;
per cases by NAT_1:14;
suppose A4:len F=0;
hence addreal "**" F = 0 by Def8,A2,BINOP_2:2
.= Sum F by Def8,A3,A4,BINOP_2:1;
end;
suppose A5:len F>=1;
A6: REAL = REAL /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
now let x,y;assume x in REAL & y in REAL;
then reconsider X=x,Y=y as Element of REAL;
addreal.(x,y) = X+Y by BINOP_2:def 9;
hence addreal.(x,y) =addcomplex.(x,y) & addreal.(x,y) in REAL
by BINOP_2:def 3,XREAL_0:def 1;
end;
hence thesis by Th46,A5,A6,A2;
end;
end;
theorem Th48:
F is RAT-valued implies Sum F = addrat "**" F
proof
assume A1:F is RAT-valued;
rng F c= COMPLEX by A1,MEMBERED:1;
then A2:F is COMPLEX-valued by RELAT_1:def 19;
per cases by NAT_1:14;
suppose A3:len F=0;
hence addrat "**" F = 0 by Def8,A1,BINOP_2:3
.= Sum F by Def8,A2,A3,BINOP_2:1;
end;
suppose A4:len F>=1;
A5: RAT = RAT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
now let x,y;assume x in RAT & y in RAT;
then reconsider X=x,Y=y as Element of RAT;
addrat.(x,y) = X+Y by BINOP_2:def 15;
hence addrat.(x,y) =addcomplex.(x,y) & addrat.(x,y) in RAT
by BINOP_2:def 3,RAT_1:def 2;
end;
hence thesis by Th46,A4,A5,A1;
end;
end;
theorem Th49:
F is INT-valued implies Sum F = addint "**" F
proof
assume A1:F is INT-valued;
rng F c= COMPLEX by A1,MEMBERED:1;
then A2:F is COMPLEX-valued by RELAT_1:def 19;
per cases by NAT_1:14;
suppose A3:len F=0;
hence addint "**" F = 0 by Def8,A1,BINOP_2:4
.= Sum F by Def8,A2,A3,BINOP_2:1;
end;
suppose A4:len F>=1;
A5: INT = INT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
now let x,y;assume x in INT & y in INT;
then reconsider X=x,Y=y as Element of INT;
addint.(x,y) = X+Y by BINOP_2:def 20;
hence addint.(x,y) =addcomplex.(x,y) & addint.(x,y) in INT
by BINOP_2:def 3, INT_1:def 2;
end;
hence thesis by Th46,A4,A5,A1;
end;
end;
theorem Th50:
F is natural-valued implies Sum F = addnat "**" F
proof
assume A1:F is natural-valued;
then rng F c= NAT by VALUED_0:def 6;
then A2:F is NAT-valued by RELAT_1:def 19;
rng F c= COMPLEX by A1,MEMBERED:1;
then A3:F is COMPLEX-valued by RELAT_1:def 19;
per cases by NAT_1:14;
suppose A4:len F=0;
hence addnat "**" F = 0 by Def8,A2,BINOP_2:5
.= Sum F by Def8,A3,A4,BINOP_2:1;
end;
suppose A5:len F>=1;
A6: NAT = NAT /\ COMPLEX by MEMBERED:1,XBOOLE_1:28;
now let x,y;assume x in NAT & y in NAT;
then reconsider X=x,Y=y as Element of NAT;
addnat.(x,y) = X+Y by BINOP_2:def 23;
hence addnat.(x,y) =addcomplex.(x,y) & addnat.(x,y) in NAT
by BINOP_2:def 3;
end;
hence thesis by Th46,A5,A6,A2;
end;
end;
registration
let F be real-valued XFinSequence;
cluster Sum F -> real;
coherence
proof
Sum F = addreal "**" F by Th47;
hence thesis;
end;
end;
registration
let F be RAT-valued XFinSequence;
cluster Sum F -> rational;
coherence
proof
Sum F = addrat "**" F by Th48;
hence thesis;
end;
end;
registration
let F be INT-valued XFinSequence;
cluster Sum F -> integer;
coherence
proof
Sum F = addint "**" F by Th49;
hence thesis;
end;
end;
registration
let F be natural-valued XFinSequence;
cluster Sum F -> natural;
coherence
proof
Sum F = addnat "**" F by Th50;
hence thesis;
end;
end;
registration
cluster natural-valued -> nonnegative-yielding for Relation;
coherence
proof
let R be Relation;
assume R is natural-valued;
then for r be Real st r in rng R holds r >=0;
hence thesis by PARTFUN3:def 4;
end;
end;
theorem
cF = {} implies Sum cF = 0;
theorem
Sum <%c%> = c
proof
c in COMPLEX by XCMPLX_0:def 2;
hence thesis by Th37;
end;
theorem
Sum <%c1,c2%> = c1 + c2
proof
c1 in COMPLEX & c2 in COMPLEX by XCMPLX_0:def 2;
then addcomplex "**" <%c1,c2%> = addcomplex.(c1,c2) by Th38
.= c1+c2 by BINOP_2:def 3;
hence thesis;
end;
theorem Th54: :: RLVECT_1:58 NUMERAL1:1
Sum(cF1^cF2)=Sum(cF1)+Sum(cF2)
proof
A1: cF1 is COMPLEX -valued & cF2 is COMPLEX -valued by Lm2;
thus Sum(cF1^cF2)=addcomplex.(Sum(cF1),Sum(cF2)) by Th41,A1
.= Sum(cF1)+Sum(cF2) by BINOP_2:def 3;
end;
theorem :: NUMERAL1:2
for S being Real_Sequence st rF=S|(n+1) holds Sum rF = Partial_Sums(S).n
proof
let S be Real_Sequence;
A1:rF is REAL -valued by Lm3;
n+1 c= NAT;
then
A2: n+1 c= dom S by FUNCT_2:def 1;
assume
A3: rF=S|(n+1);
then dom rF = dom S /\ (n+1) by RELAT_1:61;
then
A4: dom rF = n+1 by A2,XBOOLE_1:28;
then consider f be sequence of REAL such that
A5: f.0 = rF.0 and
A6: for m be Nat st m+1 < len rF holds f.(m + 1) = addreal.(f.m,rF.(m + 1)) and
A7: addreal "**" rF = f.(len rF-1) by Def8,A1;
defpred P[Nat] means $1 in dom rF implies f.$1=Partial_Sums(S).$1;
A8: now
let k;
assume
A9: P[k];
thus P[k+1]
proof
assume
A10: k+1 in dom rF;
then
A11: k+1 < len rF by AFINSQ_1:86;
then
A12: k=1;
consider f being sequence of REAL such that
A5: f.0 = d.0 and
A6: for n st n+1 < len d holds f.(n + 1) = addreal.
(f.n,d.(n + 1)) and
A7: Sum d = f.(len d-1) by A4,Def8,A3;
consider g being sequence of REAL such that
A8: g.0 = e.0 and
A9: for n st n+1 < len e holds g.(n + 1) = addreal.
(g.n,e.(n + 1)) and
A10: Sum e = g.(len e-1) by A4,A1,Def8,A3;
defpred P[Nat] means $1 in dom d implies f.$1 <= g.$1;
A11: now
let i;
assume
A12: P[i];
thus P[i+1]
proof
assume
A13: i+1 in dom d;
then
A14: i+1 < len d by AFINSQ_1:86;
then
A15: i < len d by NAT_1:13;
A16: d.(i+1) <= e.(i+1) by A2,A13;
A17: f.(i+1) = addreal.(f.i,d.(i + 1)) by A6,A14
.= f.i + d.(i+1) by BINOP_2:def 9;
g.(i+1) = addreal.(g.i,e.(i + 1)) by A1,A9,A14
.= g.i + e.(i+1) by BINOP_2:def 9;
hence thesis by A12,A15,A17,A16,AFINSQ_1:86,XREAL_1:7;
end;
end;
reconsider ld=len d-1 as Element of NAT by A4,NAT_1:21;
len d-1 < len d - 0 by XREAL_1:10;
then
A18: ld in len d by AFINSQ_1:86;
A19: P[0] by A2,A5,A8;
for i holds P[i] from NAT_1:sch 2(A19,A11);
hence thesis by A1,A7,A10,A18;
end;
suppose len d=0;
then Sum d = the_unity_wrt addreal & Sum e = the_unity_wrt addreal
by Def8,A3,A1;
hence thesis;
end;
end;
theorem Th57:
Sum (n-->c) = n*c
proof
set Fn= n-->c;
reconsider Fn as XFinSequence of COMPLEX by Lm2;
A1:dom Fn = n by FUNCOP_1:13;
now
per cases;
suppose
dom Fn=0;
hence thesis by A1;
end;
suppose
A2: dom Fn>0;
then consider f be sequence of COMPLEX such that
A3: f.0 = Fn.0 and
A4: for k st k+1 < len Fn holds
f.(k + 1) = addcomplex.(f.k,Fn.(k + 1)) and
A5: Sum Fn= f.(len Fn-1) by Def8;
defpred P[Nat] means $1 < len Fn implies f.$1 =($1+1)*c;
A6: for m st P[m] holds P[m+1]
proof
let m such that
A7: P[m];
assume
A8: m + 1 < len Fn;
then f.(m+1)=addcomplex.(f.m,Fn.(m+1)) by A4;
then
A9: f.(m + 1) = f.m + Fn.(m+1) by BINOP_2:def 3;
Fn.(m+1) = c by A1,FUNCOP_1:7,A8,AFINSQ_1:86;
hence thesis by A7,A8,A9,NAT_1:13;
end;
reconsider lenFn1=len Fn -1 as Element of NAT by A2,NAT_1:20;
A10: lenFn1r;
assume A1:n in dom rF implies rF.n <= r;
A2:len L=len rF by FUNCOP_1:13;
now let n;assume n in dom rF;
then rF.n <= r & L.n = r by A1,FUNCOP_1:7;
hence rF.n <= L.n;
end;
then Sum rF <= Sum L by Th56,A2;
hence thesis by Th57;
end;
theorem :: STIRL2_1:51
(for n st n in dom rF holds rF.n >= r) implies
Sum rF >= len rF *r
proof
set L=len rF-->r;
assume A1:n in dom rF implies rF.n >= r;
A2:len L=len rF by FUNCOP_1:13;
now let n;assume n in dom rF;
then rF.n >= r & L.n = r by A1,FUNCOP_1:7;
hence rF.n >= L.n;
end;
then Sum rF >= Sum L by Th56,A2;
hence thesis by Th57;
end;
theorem Th60: :: STIRL2_1:52
rF is nonnegative-yielding & len rF > 0 &
(ex x st x in dom rF & rF.x = r) implies Sum rF >= r
proof
assume that
A1:rF is nonnegative-yielding and
A2: len rF > 0 and
A3: ex x st x in dom rF & rF.x = r;
consider x such that
A4: x in dom rF and
A5: rF.x = r by A3;
reconsider lenrF1=len rF-1 as Element of NAT by A2,NAT_1:20;
A6: dom rF=lenrF1+1;
reconsider x as Element of NAT by A4;
A7: lenrF1 < lenrF1+1 by NAT_1:13;
A8: x < len rF by A4,AFINSQ_1:86;
then
A9: x<=lenrF1 by A6,NAT_1:13;
rF is REAL-valued by Lm3;then
consider f be sequence of REAL such that
A10: f.0 = rF.0 and
A11: for n st n+1 < len rF holds f.(n + 1) = addreal.(f.n,rF.(n + 1)) and
A12: addreal "**" rF= f.(len rF-1) by Def8,A2;
defpred P[Nat] means $1 < x implies f.$1 >= 0;
0 in len rF by A2,AFINSQ_1:86;
then rF.0 in rng rF by FUNCT_1:def 3;
then
A13:P[0] by A1,A10,PARTFUN3:def 4;
A14:P[n] implies P[n+1]
proof
assume A15:P[n];
assume A16:n+1 < x;
then n < x & n+1 < len rF by A8,NAT_1:13,XXREAL_0:2;
then A17:f.(n + 1) = addreal.(f.n,rF.(n + 1)) & f.n >=0 & n+1 in dom rF
by A11,A15,AFINSQ_1:86;
then rF.(n+1) in rng rF by FUNCT_1:def 3;
then rF.(n+1) >=0 by A1,PARTFUN3:def 4;
then f.n+rF.(n + 1) >=zz+zz by A16,A15,NAT_1:13;
hence thesis by A17,BINOP_2:def 9;
end;
A18:P[n] from NAT_1:sch 2(A13,A14);
defpred P[Nat] means x <= $1 & $1 < len rF implies f.$1 >= r;
now
per cases;
suppose
A19: x=0;
assume that
x <= x and
x < len rF;
thus f.x>=r by A5,A10,A19;
end;
suppose
x>0;
then reconsider x1=x-1 as Element of NAT by NAT_1:20;
assume that
x <= x and
A20: x < len rF;
A21: x1 =0
by A21,A18,BINOP_2:def 9;
then f.x>=r+(0 qua Real) by A5,XREAL_1:7;
hence f.x>=r;
end;
end;
then
A22: P[x];
A23: for m be Nat st m>=x & P[m] holds P[m+1]
proof
let m be Nat such that
A24: m>=x and
A25: P[m];
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
assume that
x <= m+1 and
A26: m+1 < len rF;
m+1 in dom rF by A26,AFINSQ_1:86;
then A27:rF.(m+1) in rng rF by FUNCT_1:def 3;
f.(m1 + 1) = addreal.(f.m1,rF.(m1 + 1)) by A11,A26;
then f.(m1+1)=f.m1+rF.(m1+1) & rF.(m1+1) >=0
by A27,A1,BINOP_2:def 9,PARTFUN3:def 4;
then f.(m+1) >= r+(0 qua Real) by A24,A25,A26,NAT_1:13,XREAL_1:7;
hence thesis;
end;
for m be Nat st m>=x holds P[m] from NAT_1:sch 8(A22,A23);
then addreal "**" rF >= r by A12,A9,A7;
hence thesis by Th47;
end;
theorem Th61: :: STIRL2_1:53
rF is nonnegative-yielding implies
(Sum rF=0 iff (len rF=0 or rF = len rF --> 0))
proof
assume A1:
rF is nonnegative-yielding;
hereby
assume
A2: Sum rF=0;
assume
A3: len rF <>0;
set L=len rF -->0;
assume rF <> len rF -->0;
then consider k such that
A4: k in dom L & L.k <> rF.k by AFINSQ_1:8,FUNCOP_1:13;
rF.k in rng rF by A4,FUNCT_1:def 3;
then L.k = 0 & rF.k >=0 by A4,A1,FUNCOP_1:7,PARTFUN3:def 4;
hence contradiction by A2,Th60,A1,A4,A3;
end;
A5:rF is COMPLEX-valued by Lm2;
assume len rF=0 or rF= len rF -->0 ;
then Sum rF = 0 or Sum rF = len rF *0 by A5,Th57,Def8,BINOP_2:1;
hence thesis;
end;
theorem Th62:
c(#)cF|n = (c(#)cF)|n
proof
set ccF=c(#)cF;
set cFn = cF|n;
A1:len ccF = len cF & len (c(#)cFn) = len cFn by VALUED_1:def 5;
per cases;
suppose A2:n <= len cF;
then A3:len(cFn) = n & len (ccF|n)=n by A1,AFINSQ_1:54;
now let i;
assume i < len (c(#)cFn);
then A4: i in dom (c(#)cFn) by AFINSQ_1:86;
thus (c(#)cFn).i = c* (cFn.i) by VALUED_1:6
.= c* (cF.i) by A4,A2,AFINSQ_1:53
.=ccF.i by VALUED_1:6
.=(ccF|n).i by A4,A1,A2,AFINSQ_1:53;
end;
hence thesis by A1,A3,AFINSQ_1:9;
end;
suppose n > len cF;
then cF|n= cF & ccF|n=ccF by A1,AFINSQ_1:52;
hence thesis;
end;
end;
theorem
c * Sum cF = Sum (c(#)cF)
proof
defpred P[Nat] means for cF st len cF=$1 holds
c * Sum cF = Sum (c(#)cF);
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
A3: kx holds (f|(dom f\{y}))"{x}=f"{x}
proof let x,y be object;
let f be Function;
set d=dom f\{y};
assume
A1: f.y<>x;
A2: f"{x} c= (f|d)"{x}
proof
A3: dom (f|d)=dom f/\d by RELAT_1:61;
let x1 be object such that
A4: x1 in f"{x};
A5: f.x1 in {x} by A4,FUNCT_1:def 7;
f.x1 in {x} by A4,FUNCT_1:def 7;
then f.x1=x by TARSKI:def 1;
then
A6: not x1 in {y} by A1,TARSKI:def 1;
x1 in dom f by A4,FUNCT_1:def 7;
then x1 in d by A6,XBOOLE_0:def 5;
then
A7: x1 in dom (f|d) by A3,XBOOLE_0:def 4;
then f.x1=(f|d).x1 by FUNCT_1:47;
hence thesis by A7,A5,FUNCT_1:def 7;
end;
(f|d)"{x} c= f"{x}
proof
let x1 be object such that
A8: x1 in (f|d)"{x};
A9: (f|d).x1 in {x} by A8,FUNCT_1:def 7;
A10: x1 in dom (f|d) by A8,FUNCT_1:def 7;
then dom (f|d)=dom f/\d & f.x1=(f|d).x1 by FUNCT_1:47,RELAT_1:61;
hence thesis by A10,A9,FUNCT_1:def 7;
end;
hence thesis by A2;
end;
theorem :: CATALAN2:45
rng cF c= {0,c} implies Sum cF = c * card (cF"{c})
proof
defpred P[Nat] means for cF,c st len cF=$1 &
rng cF c= {0,c} holds Sum cF = c* card (cF"{c});
assume
A1: rng cF c= {0,c};
A2: for k st P[k] holds P[k+1]
proof
let k such that
A3: P[k];
let F be complex-valued XFinSequence,
c be Complex such that
A4: len F=k+1 and
A5: rng F c= {0,c};
per cases;
suppose
A6: c <>0;
( not k in k)& Segm k \/ {k}= Segm(k+1) by AFINSQ_1:2;
then
A7: dom F\{k}=k by A4,ZFMISC_1:117;
k 0 by FUNCOP_1:11;
then Sum F = len F*0 by Th61;
hence thesis by A20;
end;
end;
A21: P[0]
proof
let F be complex-valued XFinSequence,
c be Complex such that
A22: len F=0 and
rng F c= {0,c};
F"{c} c= 0 & F={} by A22,RELAT_1:132;
then card (F"{c})=0 & Sum F =0;
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2(A21,A2);
then P[len cF];
hence thesis by A1;
end;
theorem :: CATALAN2:48
Sum cF = Sum Rev cF
proof
cF is COMPLEX-valued by Lm2;then
reconsider Fr2 = cF,Fr1 = Rev cF as XFinSequence of COMPLEX;
A1: len Fr1=len Fr2 by Def1;
defpred P[object,object] means for i st i=$1 holds $2=len Fr1-(1+i);
A2: card len Fr1 =card len Fr1;
A3: for x being object st x in len Fr1
ex y being object st y in len Fr1 & P[x,y]
proof
let x be object such that
A4: x in len Fr1;
reconsider k=x as Element of NAT by Th1,A4;
k+1 <= len Fr1 by NAT_1:13,A4,AFINSQ_1:86;
then
A5: len Fr1-'(1+k)=len Fr1-(1+k) by XREAL_1:233;
take len Fr1-'(1+k);
len Fr1 +zz< len Fr1 +(1+k) by XREAL_1:8;
then len Fr1-(1+k) < len Fr1+(1+k)-(1+k) by XREAL_1:9;
hence thesis by A5,AFINSQ_1:86;
end;
consider P be Function of len Fr1,len Fr1 such that
A6: for x being object st x in len Fr1 holds P[x,P.x] from FUNCT_2:sch 1(A3);
for x1,x2 be object
st x1 in len Fr1 & x2 in len Fr1 & P.x1 = P.x2 holds x1 = x2
proof
let x1,x2 be object such that
A7: x1 in len Fr1 and
A8: x2 in len Fr1 and
A9: P.x1 = P.x2;
reconsider i=x1,j=x2 as Element of NAT by A7,A8,Th1;
A10: P.x2=len Fr1-(1+j) by A6,A8;
P.x1=len Fr1-(1+i) by A6,A7;
hence thesis by A9,A10;
end;
then
A11: P is one-to-one by FUNCT_2:56;
then P is onto by A2,Lm1;
then reconsider P as Permutation of dom Fr1 by A11;
A12: now
let x be object such that
A13: x in dom Fr1;
reconsider k=x as Element of NAT by A13;
P.k=len Fr1-(1+k) by A6,A13;
hence Fr1.x=Fr2.(P.x) by A1,Def1,A13;
end;
A14: now
let x be object such that
A15: x in dom Fr1;
x in dom P by A15,FUNCT_2:52;
then P.x in rng P by FUNCT_1:3;
hence x in dom P & P.x in dom Fr2 by A1,A15,FUNCT_2:52;
end;
for x being object st x in dom P & P.x in dom Fr2 holds x in dom Fr1;
then Fr1 = Fr2 * P by A14,A12,FUNCT_1:10;
hence thesis by A1,Th44;
end;
theorem Th69:
for f be Function,p,q,fp,fq be XFinSequence st
rng p c= dom f & rng q c= dom f & fp = f*p & fq = f*q
holds fp ^ fq = f*(p^q)
proof
let f be Function,p,q,fp,fq be XFinSequence such that
A1: rng p c= dom f & rng q c= dom f & fp = f*p & fq = f*q;
set pq=p^q;
A2:rng pq = rng p \/rng q by AFINSQ_1:26;
then A3:dom (f*pq)=dom pq by A1,RELAT_1:27,XBOOLE_1:8;
reconsider fpq = f*pq as XFinSequence by A2,A1,AFINSQ_1:10,XBOOLE_1:8;
A4:dom fp=dom p & dom fq = dom q by A1,RELAT_1:27;
A5:dom pq=len p+len q & dom (fp^fq) = len fp+len fq by AFINSQ_1:def 3;
A6:len fpq = len (fp^fq) by A2,A1,A4,A5,RELAT_1:27,XBOOLE_1:8;
k < len fpq implies (fp^fq).k = fpq.k
proof
assume A7:k< len fpq;
then A8:k in dom fpq by AFINSQ_1:86;
per cases;
suppose k < len p;
then k in dom p by AFINSQ_1:86;
then pq.k = p.k & fp.k = f.(p.k) & (fp^fq).k =fp.k
by A1,A4,AFINSQ_1:def 3,FUNCT_1:13;
hence thesis by A8,FUNCT_1:12;
end;
suppose A9:k >= len p;
then reconsider kp=k-len p as Element of NAT by NAT_1:21;
len p + kp < len p+len q by A5,A2,A1,A7,RELAT_1:27,XBOOLE_1:8;
then
kp < len q by XREAL_1:7;
then pq.k = q.kp & (fp^fq).k = fq.kp & fq.kp = f.(q.kp)
by A7,A1,A3,A4,A5,A9,AFINSQ_1:18,FUNCT_1:13,AFINSQ_1:86;
hence thesis by A8,FUNCT_1:12;
end;
end;
hence thesis by A6,AFINSQ_1:9;
end;
theorem
for B1,B2 being finite natural-membered set st
B1 D = the_unity_wrt b
proof
A1: len <%>D = 0;
assume b is having_a_unity;
hence thesis by A1,Def8;
end;
definition
let D be set, F be XFinSequence of D^omega;
func FlattenSeq F -> Element of D^omega means
:Def10:
ex g being BinOp of D^omega st
(for p, q being Element of D^omega holds g.(p,q) = p^q) & it = g "**" F;
existence
proof
deffunc F(Element of D^omega,Element of D^omega) = $1^$2;
consider g being BinOp of D^omega such that
A1: for a, b being Element of D^omega holds g.(a,b) = F(a,b)
from BINOP_1:sch 4;
take g "**" F, g;
thus thesis by A1;
end;
uniqueness
proof
let it1, it2 be Element of D^omega;
given g1 being BinOp of D^omega such that
A2: for p, q being Element of D^omega holds g1.(p,q) = p^q and
A3: it1 = g1 "**" F;
given g2 being BinOp of D^omega such that
A4: for p, q being Element of D^omega holds g2.(p,q) = p^q and
A5: it2 = g2 "**" F;
now
let a, b be Element of D^omega;
thus g1.(a,b) = a^b by A2
.= g2.(a,b) by A4;
end;
hence thesis by A3,A5,BINOP_1:2;
end;
end;
theorem
for D being set, d be Element of D^omega holds FlattenSeq <%d%> = d
proof
let D be set, d be Element of D^omega;
ex g being BinOp of D^omega st
(for p, q being Element of D^omega holds g.(p,q) = p^q) &
FlattenSeq <%d%> = g "**" <% d %> by Def10;
hence thesis by Th37;
end;
theorem
for D being set holds FlattenSeq <%>(D^omega) = <%>D
proof
let D be set;
consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <%>(D^omega) = g "**" <%>(D^omega) by Def10;
A3: {} is Element of D^omega by AFINSQ_1:43;
reconsider p = {} as Element of D^omega by AFINSQ_1:43;
now
let a be Element of D^omega;
thus g.({},a) = {} ^ a by A1,A3
.= a;
thus g.(a,{}) = a ^ {} by A1,A3
.= a;
end;
then
A4: p is_a_unity_wrt g by BINOP_1:3;
then g "**" <%>(D^omega) = the_unity_wrt g by Th71,SETWISEO:def 2;
hence thesis by A2,A4,BINOP_1:def 8;
end;
theorem Th74:
for D being set, F,G be XFinSequence of D^omega holds
FlattenSeq (F ^ G) = FlattenSeq F ^ FlattenSeq G
proof
let D be set, F,G be XFinSequence of D^omega;
consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq (F ^ G) = g "**" F ^ G by Def10;
now
let a,b,c be Element of D^omega;
thus g.(a,g.(b,c)) = a ^ g.(b,c) by A1
.= a ^ (b ^ c) by A1
.= a ^ b ^ c by AFINSQ_1:27
.= g.(a,b) ^ c by A1
.= g.(g.(a,b),c) by A1;
end;
then
A3: g is associative;
A4: {} is Element of D^omega by AFINSQ_1:43;
reconsider p = {} as Element of D^omega by AFINSQ_1:43;
now
let a be Element of D^omega;
thus g.({},a) = {} ^ a by A1,A4
.= a;
thus g.(a,{}) = a ^ {} by A1,A4
.= a;
end;
then p is_a_unity_wrt g by BINOP_1:3;
then g is having_a_unity or len F >= 1 & len G >= 1 by SETWISEO:def 2;
hence FlattenSeq (F ^ G) = g.(g "**" F,g "**" G) by A2,A3,Th41
.= (g "**" F) ^ (g "**" G) by A1
.= FlattenSeq F ^ (g "**" G) by A1,Def10
.= FlattenSeq F ^ FlattenSeq G by A1,Def10;
end;
theorem
for D being set, p,q be Element of D^omega holds FlattenSeq <% p,q %> = p ^ q
proof
let D be set, p,q be Element of D^omega;
consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <% p,q %> = g "**" <% p,q %> by Def10;
thus FlattenSeq <% p,q %> = g.(p,q) by A2,Th38
.= p ^ q by A1;
end;
theorem
for D being set, p,q,r be Element of D^omega holds
FlattenSeq <% p,q,r %> = p ^ q ^ r
proof
let D be set, p,q,r be Element of D^omega;
consider g being BinOp of D^omega such that
A1: for d1,d2 being Element of D^omega holds g.(d1,d2) = d1^d2 and
A2: FlattenSeq <% p,q,r %> = g "**" <% p,q,r %> by Def10;
thus FlattenSeq <% p,q,r %> = g.(g.(p,q),r) by A2,Th39
.= g.(p,q) ^ r by A1
.= p ^ q ^ r by A1;
end;
theorem Th77:
p c= q implies p ^ (q /^ len p) = q
proof assume
A1: p c= q;
A2: len p + len (q /^ len p)
= len p + (len q -' len p) by Def2
.= len q + len p -' len p by A1,NAT_1:43,NAT_D:38
.= dom q by NAT_D:34;
A3: for k st k in dom p holds q.k=p.k by A1,GRFUNC_1:2;
for k st k in dom(q /^ len p) holds q.(len p + k) = (q /^ len p).k
by Def2;
hence p ^ (q /^ len p) = q by A2,A3,AFINSQ_1:def 3;
end;
reserve r,s for XFinSequence;
theorem Th78:
p c= q implies ex r st p^r = q
proof
assume
A1: p c= q;
take r = q /^ len p;
thus p^r = q by A1,Th77;
end;
theorem Th79:
for p,q being XFinSequence of D st p c= q
ex r being XFinSequence of D st p^r = q
proof
let p,q being XFinSequence of D;
assume p c= q;
then consider r such that
A1: p^r = q by Th78;
reconsider r as XFinSequence of D by A1,AFINSQ_1:31;
take r;
thus thesis by A1;
end;
theorem
q c= r implies p^q c= p^r
proof
assume q c= r;
then consider s such that
A1: q^s = r by Th78;
p^q c= p^q^s by AFINSQ_1:74;
hence thesis by A1,AFINSQ_1:27;
end;
theorem
for D being set, F,G be XFinSequence of D^omega holds
F c= G implies FlattenSeq F c= FlattenSeq G
proof
let D be set, F,G be XFinSequence of D^omega;
assume F c= G;
then consider F9 being XFinSequence of D^omega such that
A1: F ^ F9 = G by Th79;
FlattenSeq F ^ FlattenSeq F9 = FlattenSeq G by A1,Th74;
hence thesis by AFINSQ_1:74;
end;
registration let p; let q be non empty XFinSequence;
cluster p^q -> non empty;
coherence by AFINSQ_1:30;
cluster q^p -> non empty;
coherence by AFINSQ_1:30;
end;
theorem
CutLastLoc(p^<%x%>) = p
proof set q = CutLastLoc(p^<%x%>);
A1: len(p^<%x%>) -' 1 = len p + 1 -' 1 by AFINSQ_1:75
.= len p by NAT_D:34;
A2: dom(p^<%x%>) = len(p^<%x%>)
.= Segm(len p + 1) by AFINSQ_1:75
.= Segm len p \/ {len p} by AFINSQ_1:2;
A3: not len p in dom p;
LastLoc(p^<%x%>) = len(p^<%x%>) -' 1 by AFINSQ_1:70;
hence
A4: dom q = dom(p^<%x%>) \ {len p} by A1,VALUED_1:36
.= dom p by A2,A3,ZFMISC_1:117;
let y be object;
assume
A5: y in dom q;
A6: p c= p^<%x%> by AFINSQ_1:74;
thus q.y = (p^<%x%>).y by A5,GRFUNC_1:2
.= p.y by A5,A4,A6,GRFUNC_1:2;
end;
:: generalizes BALLOT_1:1 to empty D
theorem Th17:
for D being set, p being XFinSequence of D, n being Nat
holds XFS2FS(p|n) = (XFS2FS p)|n & XFS2FS(p/^n) = (XFS2FS p)/^n
proof
let D be set, p be XFinSequence of D, n be Nat;
:: first part
thus XFS2FS(p|n) = (XFS2FS p)|n
proof
A1: now
let x be object;
hereby
assume A2: x in dom XFS2FS(p|n);
then reconsider m1 = x as Nat;
A3: 1 <= m1 & m1 <= len XFS2FS(p|n) by A2, FINSEQ_3:25;
then reconsider m = m1 - 1 as Nat by INT_1:74;
m+1 in dom XFS2FS(p|n) by A2;
then m in dom(p|n) by AFINSQ_1:95;
then A4: m in dom p & m in n by RELAT_1:57;
then A5: m+1 in dom XFS2FS p by AFINSQ_1:95;
m in Segm n by A4;
then m < n by NAT_1:44;
then m+1 <= n by NAT_1:13;
then x in dom((XFS2FS p)|Seg n) by A3, A5, FINSEQ_1:1, RELAT_1:57;
hence x in dom((XFS2FS p)|n) by FINSEQ_1:def 15;
end;
assume x in dom((XFS2FS p)|n);
then x in dom((XFS2FS p)|Seg n) by FINSEQ_1:def 15;
then A6: x in dom XFS2FS p & x in Seg n by RELAT_1:57;
then reconsider m1 = x as Nat;
A7: 1 <= m1 & m1 <= n by A6, FINSEQ_1:1;
then reconsider m = m1-1 as Nat by INT_1:74;
m+1 in dom XFS2FS p by A6;
then A8: m in dom p by AFINSQ_1:95;
m+1 <= n by A7;
then m < n by NAT_1:13;
then m in Segm n by NAT_1:44;
then m in dom(p|n) by A8, RELAT_1:57;
then m+1 in dom XFS2FS(p|n) by AFINSQ_1:95;
hence x in dom XFS2FS(p|n);
end;
for k being Nat st k in dom XFS2FS(p|n)
holds (XFS2FS(p|n)).k = ((XFS2FS p)|n).k
proof
let k be Nat;
assume A9: k in dom XFS2FS(p|n);
then A10: 1 <= k & k <= len XFS2FS(p|n) by FINSEQ_3:25;
then reconsider m = k-1 as Nat by INT_1:74;
m+1 in dom XFS2FS(p|n) by A9;
then A11: m in dom(p|n) by AFINSQ_1:95;
then m in Segm len(p|n);
then m < len(p|n) by NAT_1:44;
then A12: m+1 <= len(p|n) by NAT_1:13;
Segm len(p|n) c= Segm len p by RELAT_1:60;
then len(p|n) <= len p by NAT_1:39;
then A13: k <= len p by A12, XXREAL_0:2;
m in Segm n by A11;
then m < n by NAT_1:44;
then m+1 <= n by NAT_1:13;
then A14: k in Seg n by A10, FINSEQ_1:1;
thus (XFS2FS(p|n)).k = (p|n).(m+1-'1) by A10, A12, AFINSQ_1:def 9
.= (p|n).m by NAT_D:34
.= p.m by A11, FUNCT_1:47
.= p.(m+1-'1) by NAT_D:34
.= (XFS2FS p).k by A10, A13, AFINSQ_1:def 9
.= ((XFS2FS p)|Seg n).k by A14, FUNCT_1:49
.= ((XFS2FS p)|n).k by FINSEQ_1:def 15;
end;
hence XFS2FS(p|n) = (XFS2FS p)|n by A1, TARSKI:2;
end;
:: second part
per cases;
suppose A15: len p <= n;
then p/^n = {} by Th6;
then A16: XFS2FS(p/^n) = {};
len((XFS2FS p)/^n) = 0
proof
per cases by A15, XXREAL_0:1;
suppose len p < n;
then A17: len p - n < n-n by XREAL_1:14;
thus len((XFS2FS p)/^n) = len XFS2FS p -' n by RFINSEQ:29
.= len p -' n by AFINSQ_1:def 9
.= 0 by A17, XREAL_0:def 2;
end;
suppose A18: len p = n;
thus len((XFS2FS p)/^n) = len XFS2FS p -' n by RFINSEQ:29
.= 0 + len p -' n by AFINSQ_1:def 9
.= 0 by A18, NAT_D:34;
end;
end;
hence thesis by A16;
end;
suppose A19: n < len p;
then A20: n <= len XFS2FS p by AFINSQ_1:def 9;
A21: len XFS2FS(p/^n) = len(p/^n) by AFINSQ_1:def 9
.= len p -' n by Def2
.= len XFS2FS p -' n by AFINSQ_1:def 9
.= len((XFS2FS p)/^n) by RFINSEQ:29;
now
let k be Nat;
assume A22: 1 <= k & k <= len XFS2FS(p/^n);
then A23: 1 <= k & k <= len(p/^n) by AFINSQ_1:def 9;
then reconsider m = k-1 as Nat by INT_1:74;
m+1 <= len(p/^n) by A23;
then m < len(p/^n) by NAT_1:13;
then m in Segm len(p/^n) by NAT_1:44;
then A24: m in dom(p/^n);
A25: k in dom((XFS2FS p)/^n) by A21, A22, FINSEQ_3:25;
A26: 1+0 <= k+n by A23, XREAL_1:7;
k <= len p - n by A19, A23, Th7;
then A27: k+n <= len p - n + n by XREAL_1:6;
thus (XFS2FS(p/^n)).k = (p/^n).(m+1-'1) by A23, AFINSQ_1:def 9
.= (p/^n).m by NAT_D:34
.= p.(m+n) by A24, Def2
.= p.(n+m+1-'1) by NAT_D:34
.= (XFS2FS p).(k+n) by A26, A27, AFINSQ_1:def 9
.= ((XFS2FS p)/^n).k by A20, A25, RFINSEQ:def 1;
end;
hence thesis by A21;
end;
end;
theorem Th5: :: from BALLOT_1:5
for D being set
for d be FinSequence of D holds XFS2FS (FS2XFS d) = d
proof
let D be set;
let d be FinSequence of D;
set Xd=FS2XFS d;
A1: len d = len Xd by AFINSQ_1:def 8;
A2: len Xd = len XFS2FS Xd by AFINSQ_1:def 9;
now let i such that
A3: 1 <= i and
A4: i <= len d;
reconsider i1=i-1 as Nat by A3,NAT_1:21;
A5: i1+1 = i;
A6: i-'1 = i1 by XREAL_0:def 2;
thus d.i = Xd.i1 by A4,A5,NAT_1:13,AFINSQ_1:def 8
.= (XFS2FS Xd).i by A3,A4,A6,A1,AFINSQ_1:def 9;
end;
hence thesis by A1,A2;
end;
registration
let D be set, f be FinSequence of D;
reduce XFS2FS (FS2XFS f) to f;
reducibility by Th5;
end;
theorem
for D being set, p being FinSequence of D, n being Nat
holds (FS2XFS p)|n = FS2XFS(p|n) & (FS2XFS p)/^n = FS2XFS(p/^n)
proof
let D be set, p be FinSequence of D, n be Nat;
thus (FS2XFS p)|n = FS2XFS XFS2FS((FS2XFS p)|n)
.= FS2XFS((XFS2FS FS2XFS p)|n) by Th17
.= FS2XFS(p|n);
thus (FS2XFS p)/^n = FS2XFS XFS2FS((FS2XFS p)/^n)
.= FS2XFS((XFS2FS FS2XFS p)/^n) by Th17
.= FS2XFS(p/^n);
end;
:: analogous theorem of FINSEQ_5:34
theorem
for D being set, p being one-to-one XFinSequence of D, n being Nat
holds rng(p|n) misses rng(p/^n)
proof
let D be set, p be one-to-one XFinSequence of D, n be Nat;
rng((XFS2FS p)|n) misses rng((XFS2FS p)/^n) by FINSEQ_5:34;
then rng((XFS2FS p)|n) misses rng(XFS2FS(p/^n)) by Th17;
then rng(XFS2FS(p|n)) misses rng(XFS2FS(p/^n)) by Th17;
then rng(XFS2FS(p|n)) misses rng(p/^n) by AFINSQ_1:97;
hence rng(p|n) misses rng(p/^n) by AFINSQ_1:97;
end;
registration
cluster finite for Ordinal-Sequence;
existence
proof
reconsider f = 0 --> omega as Ordinal-Sequence;
take f;
thus thesis;
end;
end;
registration
let A be finite Ordinal-Sequence, n be Nat;
cluster A /^ n -> Ordinal-yielding;
coherence
proof
consider a being Ordinal such that
A1: rng A c= a by ORDINAL2:def 4;
rng(A /^ n) c= rng A by Th9;
hence thesis by A1, XBOOLE_1:1, ORDINAL2:def 4;
end;
end;