:: 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 Association of Mizar Users
environ
vocabularies FUNCT_1, BOOLE, FINSEQ_1, FINSET_1, RELAT_1, CARD_1, TARSKI,
ALGSEQ_1, ARYTM_1, AFINSQ_1, ARYTM, FINSEQ_5, RFINSEQ, SQUARE_1,
ORDINAL2, AFINSQ_2, RLVECT_1, JORDAN3, MEMBERED, XREAL_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, NUMBERS, RELAT_1,
STRUCT_0, FUNCT_1, XCMPLX_0, REAL_1, NAT_1, PARTFUN1, FUNCT_2, FINSET_1,
ORDINAL1, ORDINAL4, FINSEQ_1, FUNCOP_1, FUNCT_4, XREAL_0, XXREAL_0,
BINARITH, AFINSQ_1, MATRIX_7, CARD_FIN, RECDEF_1, SEQ_1, MEMBERED,
VALUED_1, PRE_CIRC;
constructors WELLORD2, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, ORDINAL4, FUNCT_7,
FUNCOP_1, RLVECT_1, ORDINAL3, VALUED_1, PARTFUN1, SEQ_1, AFINSQ_1,
BINARITH, MATRIX_7, NUMBERS, XCMPLX_0, REAL_1, CARD_FIN, RECDEF_1,
MEMBERED, VALUED_0, PRE_CIRC;
registrations XBOOLE_0, SUBSET_1, RELAT_1, STRUCT_0, FUNCT_1, ORDINAL1,
FUNCOP_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, ORDINAL2, ORDINAL3, VALUED_0,
VALUED_1, FUNCT_2, AFINSQ_1, RELSET_1, NUMBERS, REAL_1, FINSET_1,
MEMBERED, PARTFUN1, PRE_CIRC;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, SUBSET_1, AFINSQ_1, FUNCT_1;
theorems TARSKI, FUNCT_1, REAL_1, NAT_1, ZFMISC_1, RELAT_1, CARD_2, XBOOLE_0,
XBOOLE_1, FINSET_1, ORDINAL1, CARD_1, XREAL_1, AFINSQ_1, BINARITH,
XXREAL_0, NAT_2, FINSEQ_2, WELLORD2, CARD_FIN, MEMBERED, VALUED_0,
VALUED_1;
schemes NAT_1, AFINSQ_1;
begin :: Preparation
reserve k,n for Element of NAT,
x,y,z,y1,y2,X,Y,D for set,
f,g for Function;
theorem AB470: for x being set, i being Nat st
x in i holds x is Element of NAT
proof let x be set, i be Nat;
assume A1: x in i;
reconsider i0=i as Element of NAT by ORDINAL1:def 13;
i0 c= NAT by MEMBERED:6;
hence x is Element of NAT by A1;
end;
registration
cluster -> natural-membered Nat;
coherence
proof
let n be Nat;
for x st x in n holds x is natural by AB470;
hence thesis by MEMBERED:def 6;
end;
end;
begin :: Additional Properties of Zero Based Finite Sequence
theorem AE221f: for X0 being finite natural-membered set holds
ex m being Nat st X0 c= m
proof let X0 be finite natural-membered set;
A1: X0 c= NAT by MEMBERED:6;
consider p being Function such that
A2: rng p = X0 & 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:7;
reconsider p as XFinSequence of NAT by ORDINAL1:def 8,A1,A2;
defpred P[Nat] means ex n being Nat st for i being Nat st i in $1 &
$1-'1 in dom p holds p.i in n;
for i being Nat st i in 0 & 0-'1 in dom p holds p.i in 0;then
A4: P[0];
A6: for k being Element of NAT st P[k] holds P[k+1]
proof let k be Element of NAT;assume P[k];then
consider n being Nat such that
B1: for i being Nat st i in k & k-'1 in dom p holds p.i in n;
per cases;
suppose C0: k+1-1 =k;
i<=k by D2,NAT_1:13;then
E2: p.i=m by E0,XXREAL_0:1;
m=len p;
E30: k+1-'1=k by BINARITH:39;
not k in len p by E20,NAT_1:45;
then not k in dom p by E20,NAT_1:45,E30,AFINSQ_1:def 1;
then for i being Nat st i in (k+1) &
(k+1)-'1 in dom p holds p.i in 2 by E20,NAT_1:45,E30,AFINSQ_1:def 1;
hence P[k+1];
end;
end;
for k being Element of NAT holds P[k] from NAT_1:sch 1(A4,A6);then
consider n being Nat such that
A5: for i being Nat st i in len p & len p -'1 in dom p holds
p.i in n;
rng p c= n
proof let y be set;assume y in rng p;then
consider x being set such that
B2: x in dom p & y=p.x by FUNCT_1:def 5;
reconsider nn=dom p as Nat;
reconsider nx=x as Nat by B2,ORDINAL1:def 13;
B6: len p -1 < len p by XREAL_1:46;
B7:nx in len p by B2,AFINSQ_1:def 1;
then len p<>0;
then len p>0;
then (0 qua Element of NAT )+1 <= len p by NAT_1:13,B2;then
B8:len p-'1=len p-1 by BINARITH:50;then
len p-'1 in len p by B6,NAT_1:45;then
nx in len p & len p -'1 in dom p by B2,B6,B7,B8,NAT_1:45,AFINSQ_1:def 1;
hence y in n by B2,A5;
end;
hence ex m being Nat st X0 c= m by A2;
end;
theorem Th11: :: from FINSEQ_2:11
for p being XFinSequence, b being set holds
b in rng p implies ex i being Element of NAT st i in dom p & p.i = b
proof let p be XFinSequence, b be set;
assume b in rng p;
then ex a being set st
a in dom p & b = p.a by FUNCT_1:def 5;
hence thesis;
end;
theorem Th14: ::from FINSEQ_2:14
for D being set,p being XFinSequence holds
(for i being Nat st i in dom p holds p.i in D) implies
p is XFinSequence of D
proof
let D be set,p be XFinSequence;
assume
A1: for i being Nat st i in dom p holds p.i in D;
rng p c= D
proof
let b be set;
assume b in rng p;then
consider i being Element of NAT such that
B1: i in dom p & p.i = b by Th11;
thus b in D by B1,A1;
end;
hence thesis by ORDINAL1:def 8;
end;
scheme XSeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}:
ex z being XFinSequence of D() st len z = i() &
for j being Nat st j in i() holds z.j = F(j)
proof
consider z being XFinSequence such that
A1: len z = i() and
A2: for i being Element of NAT st i in i() holds z.i = F(i)
from AFINSQ_1:sch 2;
A3:dom z =i() by A1,AFINSQ_1:def 1;
for j be Nat st j in i() holds z.j in D()
proof
let j be Nat;
assume B2: j in i();
reconsider j0=j as Element of NAT by ORDINAL1:def 13;
z.j0 = F(j0) by A2,B2;
hence z.j in D();
end;
then reconsider z as XFinSequence of D() by A1,A3,Th14,AFINSQ_1:def 1;
take z;
thus len z = i() by A1;
let j be Nat;
assume B3: j in i();
reconsider j0=j as Element of NAT by ORDINAL1:def 13;
j0 in i() by B3;
hence thesis by A2;
end;
theorem Th10: ::from FINSEQ_2:10
for p,q being XFinSequence
holds len p = len q & (for j being Nat st j in dom p holds p.j = q.j)
implies p = q
proof let p,q be XFinSequence;
assume that
A1: len p = len q and
A2: for j being Nat st j in dom p holds p.j = q.j;
for k being Element of NAT st k XFinSequence of REAL;
coherence
proof
dom (f+a) = len f by VALUED_1:def 2,AFINSQ_1:def 1;then
B5: f+a is XFinSequence by AFINSQ_1:7;
rng (f+a) c= REAL by VALUED_0:def 3;
hence thesis by B5,ORDINAL1:def 8;
end;
end;
theorem AC500: for f being XFinSequence of REAL, a being Element of REAL
holds len(f+a) = len f &
for i being Nat st i XFinSequence means :Def3:
len it = len f & for i being Element of NAT st i in dom it
holds it.i = f.(len f - (i + 1));
existence
proof
deffunc F(Element of NAT) = f.(len f - ($1 + 1));
consider p being XFinSequence such that
A1:len p = len f &
for k being Element of NAT st k in len f holds p.k = F(k)
from AFINSQ_1:sch 2;
len f=dom p by A1,AFINSQ_1:def 1;
hence thesis by A1,AFINSQ_1:def 1;
end;
uniqueness
proof let f1,f2 be XFinSequence such that
A1: len f1 = len f and
A2: for i being Element of NAT st
i in dom f1 holds f1.i = f.(len f - (i + 1)) and
A3: len f2 = len f and
A4: for i being Element of NAT st i in dom f2 holds f2.i = f.(len f - (i + 1));
A5:dom f = len f & len f1=dom f1 & len f2=dom f2 by A1,A3,AFINSQ_1:def 1;
now let i be Element of NAT;
assume i in dom f1;
then f1.i = f.(len f - (i + 1)) & f2.i = f.(len f - (i + 1))
by A1,A2,A3,A4,A5;
hence f1.i = f2.i;
end;
hence thesis by A1,A3,A5,AFINSQ_1:10;
end;
end;
theorem Th60: ::from FINSEQ_5:60
for f being XFinSequence holds dom f = dom Rev f & rng f = rng Rev f
proof let f be XFinSequence;
thus
A1: dom f = len f by AFINSQ_1:def 1
.= len (Rev f) by Def3
.= dom(Rev f) by AFINSQ_1:def 1;
A2: len f = len(Rev f) by Def3;
hereby let x be set;
assume x in rng f;
then consider z being set such that
A3: z in dom f and
A4: f.z = x by FUNCT_1:def 5;
reconsider i=z as Element of NAT by A3;
i in len f by A3,AFINSQ_1:def 1;then
i < len f by A3,NAT_1:45;then
i+1<=len f by NAT_1:13;then
len f -'(i+1)=len f -(i+1) by BINARITH:50;
then reconsider j = len f - (i + 1) as Element of NAT;
len f -(i+1) XFinSequence of D;
coherence
proof
rng f=rng (Rev f) by Th60;
hence thesis by ORDINAL1:def 8;
end;
end;
theorem ::from FINSEQ_1:63
for p being XFinSequence holds
p <> {} implies ex q being XFinSequence,x being set st p=q^<%x%>
proof let p be XFinSequence;
assume p <> {};
then len p<>0 by CARD_2:59;
then consider n be Nat such that
A1: len p = n + 1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 13;
set q=p|n;
take q;
take p.(len p-1);
A2: dom q = n
proof
dom p=len p by AFINSQ_1:def 1;then
A3: dom q = len p /\ n by RELAT_1:90;
n )=p
proof
A4: dom(q^(<%p.((len p)-1)%>)) = len (q^(<%p.(len p-1)%>)) by AFINSQ_1:def 1
.= (len q + len <%p.(len p-1)%>) by AFINSQ_1:20
.= len p by A1,A2,AFINSQ_1:38,def 1
.= dom p by A1,A2,AFINSQ_1:38,def 1;
for x being set st x in dom p holds p.x = (q^(<%p.(len p-1)%>)).x
proof
let x be set;
assume
A5: x in dom p;
then reconsider k = x as Element of NAT;
A6: k in n \/ {n} by A1,A5,AFINSQ_1:4;
A7: now
assume
A8: k in n;
hence p.k=q.k by A2,FUNCT_1:70
.=(q^<%p.(len p-1)%>).k by A2,A8,AFINSQ_1:def 4;
end;
now
assume
A9: k in {n};
A10: 0 in dom <%p.(len p-1)%> by NAT_1:45;
thus (q^<%p.(len p-1)%>).k =
(q^<%p.(len p-1)%>).(len q +(0 qua Element of NAT))
by A2,A9,TARSKI:def 1
.=<%p.(len p-1)%>.(0 qua Element of NAT) by A10,AFINSQ_1:def 4
.=p.(n) by A1,AFINSQ_1:def 5
.=p.k by A9,TARSKI:def 1;
end;
hence thesis by A6,A7,XBOOLE_0:def 2;
end;
hence q^(<%p.(len p-1)%>)=p by A4,FUNCT_1:9;
end;
end;
theorem Lm4:
for n be Nat
for f being XFinSequence st len f<=n holds (f|n) = f
proof
let n be Nat;
let f be XFinSequence;
assume len f<=n;then
(len f) /\ n=len f by NAT_1:47;
hence (f|n) = f by RELAT_1:97,XBOOLE_1:18;
end;
theorem Th19: ::from RFINSEQ:19
for f be XFinSequence, n,m be Nat holds
n <=len f & m in n implies (f|n).m = f.m & m in dom f
proof
let f be XFinSequence, n,m be Nat;
assume
A1: n <=len f & m in n;then
n c= len f by NAT_1:40;then
A3: n c= dom f by NAT_1:40,AFINSQ_1:def 1;
then n = dom f /\ n by XBOOLE_1:28
.= dom(f|n) by FUNCT_1:68;
hence (f|n).m = f.m & m in dom f by A1,A3,FUNCT_1:68;
end;
theorem TH80: for i being Element of NAT,q being XFinSequence st
i <= len q holds len(q|i) = i
proof let i be Element of NAT,q be XFinSequence;
assume A0: i <= len q;
i c= (len q) by NAT_1:40,A0;
then i c= dom q by AFINSQ_1:def 1;
then dom (q|i)=i by RELAT_1:91;
hence i = len(q|i) by AFINSQ_1:def 1;
end;
theorem TH80f: for i being Element of NAT,q being XFinSequence
holds len(q|i) <= i
proof let i be Element of NAT,q be XFinSequence;
dom (q|i) c= i by RELAT_1:87;
then len(q|i) c= i by AFINSQ_1:def 1;
hence len (q|i) <= i by NAT_1:40;
end;
theorem
for f be XFinSequence, n be Element of NAT st
len f = n+1 holds f = (f|n) ^ <% f.n %>
proof
let f be XFinSequence, n be Element of NAT;
assume
A1: len f = n+1;
set fn = f|n;
set x=f.n;
A2b: n < len f by A1,NAT_1:13;
A3: len fn = n by A1,TH80,NAT_1:11;
then
A4: len (fn^<%x%>) = n + len <%x%> by AFINSQ_1:20
.= len f by A1,AFINSQ_1:38;
now
let m be Nat;
assume m in len f;
then
m).m by A3,AFINSQ_1:40;
end;
case m <> len fn;
then m< len fn by A11,REAL_1:def 5;
then m in len fn by NAT_1:45;
then
A7: m in dom fn by NAT_1:45,AFINSQ_1:def 1;
hence (fn^<%x%>).m = fn.m by AFINSQ_1:def 4
.= f.m by A2b,A3,A7,A11,Th19;
:: theorem Th19: ::from RFINSEQ:19
:: for f be XFinSequence, n,m be Nat holds
:: n <=len f & m in n implies (f|n).m = f.m & m in dom f
end;
end;
hence f.m = (fn^<%x%>).m;
end;
hence thesis by A4,Th10;
end;
definition
let f be XFinSequence, n be Nat;
func f /^ n -> XFinSequence means
:Def2:
len it = len f -' n & for m be Nat st
m in dom it holds it.m = f.(m+n);
existence
proof
thus ex p1 be XFinSequence st
len p1 = len f -' n & for m be Nat st m in dom p1 holds p1.m = f.(m+n)
proof
set k = len f -' n;
deffunc F(Nat)=f.($1+n);
consider p be XFinSequence such that
A1: len p = k &
for m2 be Element of NAT st m2 in k holds
p.m2 = F(m2) from AFINSQ_1:sch 2;
take p;
k=dom p by A1,AFINSQ_1:def 1;
hence thesis by A1;
end;
end;
uniqueness
proof
let p1,p2 be XFinSequence;
thus
(len p1 = len f -' n & for m be Nat st m in dom p1 holds p1.m = f.(m+n)) &
(len p2 = len f -' n & for m be Nat st m in dom p2 holds p2.m = f.(m+n))
implies p1 = p2
proof
assume that
A2: len p1 = len f -' n & for m be Nat st m in dom p1 holds
p1.m = f.(m+n) and
A3: len p2 = len f -' n & for m be Nat st m in dom p2 holds p2.m = f.(m+n);
A4: dom p1 = len p1 & dom p2 = len p2 by AFINSQ_1:def 1;
now
let m be Nat;
assume m in len p1;
then p1.m = f.(m+n) & p2.m = f.(m+n) by A2,A3,A4;
hence p1.m = p2.m;
end;
hence p1 = p2 by A2,A3,A4,Th10;
end;
end;
end;
theorem TH80e: for f being XFinSequence, n being Nat st
n>=len f holds f/^n={}
proof let f be XFinSequence, n be Nat;
assume n>=len f;then len f-'n=0 by NAT_2:10;then
len (f/^n)=0 by Def2;
hence f/^n={} by AFINSQ_1:def 1,CARD_2:59;
end;
theorem TH80b: for f being XFinSequence,n being Nat st
n < len f holds len (f/^n) = len f -n
proof let f be XFinSequence,n be Nat;
assume n < len f;then len f-n>=0 by XREAL_1:50;then
len f-'n=len f-n by BINARITH:def 3;
hence len (f/^n) = len f -n by Def2;
end;
theorem Th19b:
for f being XFinSequence, n,m being Nat st
m+n one-to-one;
coherence
proof
let x,y be set;
assume B1: x in dom (f/^n) & y in dom (f/^n) & (f/^n).x=(f/^n).y;
B2: dom (f/^n)=len (f/^n) by AFINSQ_1:def 1;
dom (f/^n) is Subset of NAT;
then x in NAT by B1;
then reconsider nx=x,ny=y as Nat by B1,ORDINAL1:def 13;
B3: nxlen f;then f/^n={} by TH80e;
then len (f/^n)={} by CARD_1:47;
then dom (f/^n)={} by AFINSQ_1:def 1;
hence x=y by B1;
end;
end;
end;
theorem AG170: for f being XFinSequence,n being Nat holds
rng (f/^n) c= rng f
proof let f be XFinSequence,n be Nat;
thus rng (f/^n) c= rng f
proof let z be set;assume z in rng (f/^n);then
consider x being set such that
B1: x in dom (f/^n) & z=(f/^n).x by FUNCT_1:def 5;
reconsider nx=x as Element of NAT by B1;
nx in len (f/^n) by B1,AFINSQ_1:def 1;then
nx=len f;then
(f/^n)={} by TH80e;then
len(f/^n)=0 by CARD_1:47;then
dom (f/^n)={} by AFINSQ_1:def 1;
hence z in rng f by B1;
end;
end;
end;
theorem Th31: ::from FINSEQ_5:31
for f being XFinSequence holds f/^0 = f
proof let f be XFinSequence;
per cases;
suppose 0 =len f;then
f/^0 ={} & card f = 0 by TH80e,CARD_2:59;
hence thesis by B0,CARD_2:59;
end;
end;
theorem Th39: ::from FINSEQ_5:39
for i being Nat,f,g being XFinSequence holds
(f^g)/^(len f + i) = g/^i
proof let
i be Nat,f,g be XFinSequence;
A1: len(f^g) = len f + len g by AFINSQ_1:20;
per cases;
suppose
A2: i < len g;
then len f + i < len f + len g by XREAL_1:8;then
len f +i= len g;
then len f + i >= len(f^g) by A1,XREAL_1:8;
hence (f^g)/^(len f+i) = {} by TH80e
.= g/^i by A7,TH80e;
end;
end;
theorem Th40: ::from FINSEQ_5:40
for f,g being XFinSequence holds (f^g)/^(len f) = g
proof let f,g be XFinSequence;
thus (f^g)/^(len f) = (f^g)/^(len f + (0 qua Element of NAT))
.= g/^0 by Th39
.= g by Th31;
end;
theorem ::from RFINSEQ:21
for f be XFinSequence, n be Element of NAT
holds (f|n)^(f/^n) = f
proof
let f be XFinSequence,n be Element of NAT;
set fn = f/^n;
now per cases;
case
A1: len f<=n;
then
A2: f/^n = {} by TH80e;
f|n = f by A1,Lm4;
hence (f|n) ^ (f/^n) = f by A2,AFINSQ_1:32;
end;
case
A3: n XFinSequence of D;
coherence
proof A0: rng f c= D by ORDINAL1:def 8;
set p = f /^ n;
deffunc F(Element of NAT)=f.($1+n);
per cases;
suppose
A1: nD by TH80e;
hence thesis;
end;
end;
end;
definition
let f be XFinSequence,k1,k2 be Nat;
func mid(f,k1,k2) -> XFinSequence means
:AB540b: for k11,k21 being Element of NAT st
k11=k1 & k21=k2 holds it=(f|k21)/^(k11-'1);
existence
proof
reconsider k12=k1,k22=k2 as Element of NAT by ORDINAL1:def 13;
for k11,k21 being Element of NAT st
k11=k1 & k21=k2 holds (f|k22)/^(k12-'1)=(f|k21)/^(k11-'1);
hence thesis;
end;
uniqueness
proof let p,q being XFinSequence;
assume B1: (for k11,k21 being Element of NAT st
k11=k1 & k21=k2 holds p=(f|k21)/^(k11-'1))&
(for k11,k21 being Element of NAT st
k11=k1 & k21=k2 holds q=(f|k21)/^(k11-'1));
reconsider k12=k1,k22=k2 as Element of NAT by ORDINAL1:def 13;
p=(f|k22)/^(k12-'1) by B1;
hence p=q by B1;
end;
end;
theorem AB540f: for f being XFinSequence,k1,k2 being Nat st
k1>k2 holds mid(f,k1,k2) = {}
proof let f be XFinSequence,k1,k2 be Nat;
assume A6: k1>k2;
reconsider k11=k1,k21=k2 as Element of NAT by ORDINAL1:def 13;
A2: mid(f,k1,k2) = (f|k21)/^(k11-'1) by AB540b;
k1>= (0 qua Nat) +1 by A6,NAT_1:13;then
A17: k1-'1=k1-1 by BINARITH:50;
k1>=k2+1 by A6,NAT_1:13;then
A18: k1-1>=k2+1-1 by XREAL_1:11;
len (f|k21)<=k21 by TH80f;
hence mid(f,k1,k2) = {} by A2,TH80e,A17,A18,XXREAL_0:2;
end;
theorem for f being XFinSequence,k1,k2 being Nat st 1<=k1 & k2<=len f
holds
mid(f,k1,k2) = (f/^(k1-'1))|(k2+1-'k1)
proof let f be XFinSequence,k1,k2 be Nat;
assume A5: 1<=k1 & k2<=len f;
reconsider k11=k1,k21=k2 as Element of NAT by ORDINAL1:def 13;
A2: mid(f,k1,k2) = (f|k21)/^(k11-'1) by AB540b;
B2: len (f|k21)=k21 by TH80,A5;
k1k2;then
D3: mid(f,k1,k2)={} by AB540f;
k2+1<=k1 by A6,NAT_1:13;then
k2+1-'k1=0 by NAT_2:10;
hence (mid(f,k1,k2))=((f/^(k1-'1))|(k2+1-'k1)) by D3,RELAT_1:110;
end;
end;
theorem Th5: ::from FINSEQ_8:5
for f being XFinSequence,k2 being Nat holds mid(f,1,k2)=f|k2
proof
let f be XFinSequence,k2 be Nat;
reconsider k21=k2 as Element of NAT by ORDINAL1:def 13;
A2: mid(f,1,k2) = (f|k21)/^(1-'1) by AB540b;
1-'1=0 by BINARITH:51;
hence mid(f,1,k2)=f|k2 by A2,Th31;
end;
theorem ::from FINSEQ_8:6
for f being XFinSequence of D,k2 being Nat st len f<=k2 holds
mid(f,1,k2)=f
proof
let f be XFinSequence of D,k2 be Nat;
assume
A1: len f<=k2;
thus mid(f,1,k2)=f|k2 by Th5
.=f by A1,Lm4;
end;
theorem ::from FINSEQ_8:8
for f being XFinSequence,k2 being Element of NAT holds
mid(f,0,k2)=mid(f,1,k2)
proof
let f be XFinSequence,k2 be Element of NAT;
reconsider k21=k2 as Element of NAT;
A2: mid(f,1,k2) = (f|k21) by Th5;
A4: mid(f,0,k2) = (f|k21)/^(0-'1) by AB540b;
0-'1=0 by NAT_2:10;
hence mid(f,0,k2) = mid(f,1,k2) by Th31,A4,A2;
end;
theorem ::from FINSEQ_8:9
for f,g being XFinSequence holds
mid(f^g,len f+1,len f+len g)=g
proof
let f,g be XFinSequence;
A2: mid(f^g,len f +1,len f+len g)
= ((f^g)|(len f+len g))/^((len f +1)-'1) by AB540b;
A3: (len f +1)-'1=len f by BINARITH:39;
len (f^g)=len f + len g by AFINSQ_1:20;then
(f^g)|(len f+len g)= f^g by Lm4;
hence mid(f^g,len f+1,len f+len g)=g by Th40,A2,A3;
end;
definition
let D be set, f be XFinSequence of D, k1,k2 be Nat;
redefine func mid(f,k1,k2) -> XFinSequence of D;
coherence
proof
reconsider k11=k1,k21=k2 as Element of NAT by ORDINAL1:def 13;
mid(f,k1,k2) = (f|k21)/^(k11-'1) by AB540b;
hence mid(f,k1,k2) is XFinSequence of D;
end;
end;
definition let f be XFinSequence of REAL;
func Sum f -> Element of REAL means
:AC300: ex g being XFinSequence of REAL st
len f=len g & f.0=g.0 & (for i being Nat st i+1 0;
then
A3: (0 qua Element of NAT)+1<=len f by NAT_1:13;
defpred P[Nat] means ex g being XFinSequence of REAL st
len g=$1+1 & f.0=g.0 &
(len g<=len f implies (for i being Nat st i+1<$1+1 holds
g.(i+1)=(g.i)+(f.(i+1))));
A2: len (<% f.0 %>)=(0 qua Element of NAT)+1 by AFINSQ_1:38;
A34: f.0=(<% f.0 %>).0 by AFINSQ_1:38;
set d=f.0;
set g2=(<% d %>);
for i being Nat st i+1< (0 qua Element of NAT)+1 holds
g2.(i+1)=(g2.i)+(f.(i+1)) by XREAL_1:8;then
A31: P[0] by A2,A34;
A32: for k being Element of NAT st P[k] holds P[k + 1]
proof let k be Element of NAT;
assume P[k];then
consider g3 being XFinSequence of REAL such that
B2: len g3=k+1 & f.0=g3.0 &
(len g3<=len f implies (for i being Nat st i+1;
set g4=g3^r;
C2: len g4=len g3 + len (<% O %>) by AFINSQ_1:20
.=len g3 +1 by AFINSQ_1:38;
0= len f;
reconsider O=0 as Element of REAL;
set r=<% O %>;
set g4=g3^r;
C2: len g4=len g3 + len (<% 0 %>) by AFINSQ_1:20
.=len g3 +1 by AFINSQ_1:38;then
C3: len g4>len f by C1,NAT_1:13,AFINSQ_1:def 1;
len g3 =dom g3 by C1,NAT_1:13,AFINSQ_1:def 1;then
C4: 0 in dom g3 by NAT_1:45,B1,C1;
g4.0=g3.0 by C4,AFINSQ_1:def 4;
hence P[k + 1] by B2,C3,C2;
end;
end;
for k being Element of NAT holds P[k] from NAT_1:sch 1(A31,A32);then
consider g being XFinSequence of REAL such that
A33: len g=len f-'1+1 & f.0=g.0 &
(len g<=len f implies (for i being Nat st i+10;
take 0, g=<%>REAL;
len f = 0 by A1;
hence len f=len g & f.0=g.0 by AFINSQ_1:18;
thus for i be Nat st i+1=len g1;
hence P[k+1];
end;
end;
for k being Element of NAT holds P[k] from NAT_1:sch 1(A31,A32);
hence a=b by C3,C2,AFINSQ_1:11;
end;
hence thesis;
end;
end;
registration
let f be empty XFinSequence of REAL;
cluster Sum f -> zero;
coherence
proof
ex g being XFinSequence of REAL st
len f=len g & f.0=g.0 &
(for i being Nat st i+10;
per cases;
suppose A71: len h1>0;
consider g1 being XFinSequence of REAL such that
A1: len (h1)=len g1 & (h1).0=g1.0 &
(for i being Nat st i+10;
consider g2 being XFinSequence of REAL such that
A2: len (h2)=len g2 & (h2).0=g2.0 &
(for i being Nat st i+1=len g1;
per cases by H0,REAL_1:def 5;
suppose J0: i+1>len g1;then
i>=len g1 by NAT_1:13;then
i-'len g1=i-len g1 by BINARITH:50;then
reconsider i1=i-len g1 as Element of NAT;
i+1-len g1= (0 qua Element of NAT)+1 by A0,NAT_1:13;then
R50: len g1+len g2b>=1 by A1,A2,E4b,AFINSQ_1:20;
R4n: len g2b>=(0 qua Element of NAT)+1 by A2,E4b,A72,NAT_1:13;then
R4: len g2b-'1=len g2b-1 by BINARITH:50;
R2: len g1 + len g2b -'1=len g1 + len g2b -1 by R50,BINARITH:50
.= len g1 +(len g2b-1)
.= len g1 +(len g2b-'1) by BINARITH:50,R4n;
R7n: len g2b-1 XFinSequence of NAT means
:AC113:
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
consider k being Nat such that
A6: X c= k by AE221f;
defpred P[Nat] means for X being set st
X c= $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;
A2: P[0]
proof
let X be set;
assume
A3: X c= 0;
take <%>(NAT);
thus rng <%>(NAT) = X by A3,XBOOLE_1:3;
thus for l,m,k1,k2 be Nat st ( l < m & m < len <%>(NAT) &
k1=<%>(NAT).l & k2=<%>(NAT).m) holds k1 < k2;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: for X being set st X c= k holds 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
A6: X c= (k+1);
now
assume not X c= k;
then consider x such that
A7: x in X & not x in k by TARSKI:def 3;
reconsider n=x as Element of NAT by AB470,A6,A7;
nk by A12n,A6,TARSKI:def 1,NAT_1:45;then
m<=k & m<>k by NAT_1:13;
then m ;
A15: {k} c= X by A7,A8,ZFMISC_1:37;
A16: rng q = rng p \/ rng <% k %> by A14,AFINSQ_1:29
.= Y \/ {k} by A13,AFINSQ_1:36
.= X \/ {k} by XBOOLE_1:39
.= X by A15,XBOOLE_1:12;
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
A17: l < m & m < len q & k1=q.l & k2=q.m;then
m+1<=len q by NAT_1:13;then
A38: m<=len q -1 by XREAL_1:21;
A38b: m<=len q-'1 by A38,BINARITH:def 3;
A18: l in dom p
proof
l < len (p^<% k %>) -1 by A38,A14,A17,XXREAL_0:2;
then l < len p + len <% k %> -1 by AFINSQ_1:20;
then l < len p + 1 -1 & len p=dom p by AFINSQ_1:38,def 1;
hence l in dom p by NAT_1:45;
end;
A20: now
assume
A21: m=len q -'1;
k1 = p.l by A14,A17,A18,AFINSQ_1:def 4;
then
A22n: k1 in Y by A13,A18,FUNCT_1:def 5;
q.m = (p^<% k %>).((len p + len <% k %>)-'1)
by A14,A21,AFINSQ_1:20
.= (p^<% k %>).((len p + 1)-'1) by AFINSQ_1:38
.=(p^<% k %>).(len p) by BINARITH:39
.= k by AFINSQ_1:40;
hence k1 < k2 by A17,NAT_1:45,A10,A22n;
end;
now
assume m <> len q -'1;
then m < len (p^<% k %>) -'1 by A38b,A14,REAL_1:def 5;
then m < len p + len <% k %> -'1 by AFINSQ_1:20;
then m < len p + 1 -'1 by AFINSQ_1:38;
then
A23: m < len p by BINARITH:39;
then m in len p & len p=dom p by NAT_1:45,AFINSQ_1:def 1;
then
A24: k2 = p.m by A14,A17,AFINSQ_1:def 4;
k1 = p.l by A14,A17,A18,AFINSQ_1:def 4;
hence k1 < k2 by A13,A17,A23,A24;
end;
hence thesis by A20;
end;
hence thesis by A16;
end;
hence thesis by A5;
end;
for k2 being Nat holds P[k2] from NAT_1:sch 2(A2,A4);
hence thesis by A6;
end;
uniqueness
proof
let p,q be XFinSequence of NAT such that
A25: 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 and
A26: 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;
consider k being Nat such that
A6: X c= k by AE221f;
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;
A27: S[{}];
A28: for p being XFinSequence,x be set st S[p] holds S[p^<% x %>]
proof
let p be XFinSequence,x be set;
assume
A29: S[p];
let X be set;
given k being Nat such that
A30: X c= k;
assume
A31: (p^<% x %> is XFinSequence of NAT & rng (p^<% x %>) = X &
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
A32: 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;
A34: 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 A31,AFINSQ_1:34;
then rng <%x%> c= NAT by ORDINAL1:def 8;
then {x} c= NAT by AFINSQ_1:36;
then reconsider m=x as Element of NAT by ZFMISC_1:37;
take m;
thus m=x;
thus for l being Nat st l in X & l <> x holds l < m
proof
let l be Nat;
assume
A35: l in X & l <> x;
then consider y such that
A36: y in dom (p^<%x%>) & l=(p^<%x%>).y by A31,FUNCT_1:def 5;
reconsider k=y as Element of NAT by A36;
k in len (p^<%x%>) by A36,AFINSQ_1:def 1; then
k < len (p^<%x%>) by A36,NAT_1:45;
then k < len p + len <%x%> by AFINSQ_1:20;
then
k < len p + 1 by AFINSQ_1:38;then
A38b: k<=len p by NAT_1:13;
k <> len p by A35,A36,AFINSQ_1:40;
then
k< len p +1-1 by A38b,REAL_1:def 5;
then
A91: k < len p + len <%x%>-1 by AFINSQ_1:38;
A92n: len(p^<%x %>)) +1 by XREAL_1:31;
A93: len <%x%>=1 by AFINSQ_1:38;
A39: k < len(p^<%x%>)-1 & len(p^<%x%>)-1 < len(p^<%x %>)
by A91,A92n,XREAL_1:21,AFINSQ_1:20;
A98b: len(p^<%x %>) -'1=len(p^<%x %>)-1 by A39,BINARITH:def 3;
m= (p^<%x%>).(len p + len <%x%> -1) by A93,AFINSQ_1:40
.= (p^<%x%>).(len(p^<%x%>) -1) by AFINSQ_1:20;
hence l < m by A31,A36,A39,A98b;
end;
end;
then reconsider m = x as Nat;
len q <> 0
proof
assume len q = 0;
then p^<%x%> = {} by A31,A32,AFINSQ_1:18,RELAT_1:60;
then 0 = len (p^<%x%>) by CARD_1:47
.= len p + len <%x%> by AFINSQ_1:20
.= 1 + len p by AFINSQ_1:38;
hence contradiction;
end;
then consider n be Nat such that
A40: len q = n+1 by NAT_1:6;
deffunc F(Nat) = q.$1;
ex q' being XFinSequence st len q' = n &
for m being Element of NAT st m in n holds q'.m = F(m)
from AFINSQ_1:sch 2;
then consider q' being XFinSequence such that
A41b: len q' = n & for m being Element of NAT st m in n holds q'.m = q.m;
A41n: for m being Nat st m in n holds q'.m = q.m
proof let m be Nat;
assume B1: m in n;
reconsider m2=m as Element of NAT by ORDINAL1:def 13;
q'.m2=q.m2 by A41b,B1;
hence q'.m = q.m;
end;
q' is XFinSequence of NAT
proof
now
let x;
assume x in rng q';
then consider y such that
A42: y in dom q' & x=q'.y by FUNCT_1:def 5;
reconsider y as Element of NAT by A42;
q.y in NAT by ORDINAL1:def 13;
hence x in NAT by A41b,A42;
end;
then rng q' c= NAT by TARSKI:def 3;
hence thesis by ORDINAL1:def 8;
end;
then reconsider f=q' as XFinSequence of NAT;
A46: q'^<%x%> = q
proof
A47: dom q = (len q' + len <%x%>) by A41b,AFINSQ_1:38,A40;
for m being Element of NAT st m in dom <%x%> holds
q.(len q' + m) = <%x%>.m
proof
let m be Element of NAT;
assume m in dom <%x%>;
then m in len <%x%> by AFINSQ_1:def 1;then
D4: m in 1 by AFINSQ_1:38;
(0 qua Element of NAT)+1=0 \/ {0} by AFINSQ_1:4;then
A50: m=0 by TARSKI:def 1,D4;
q.(len q' + m) = x
proof
assume A51n: q.(len q' + m) <> x;
consider d being Nat such that
A52: d=x & for l being Nat st l in X & l<>x holds l by AFINSQ_1:36;
then x in rng p \/ rng <%x%> by XBOOLE_0:def 2;
hence x in rng q by A31,A32,AFINSQ_1:29;
end;
then consider y such that
A53: y in dom q & x=q.y by FUNCT_1:def 5;
reconsider y as Element of NAT by A53;
y in len q by A53,AFINSQ_1:def 1;then
A76: y.m by A50,AFINSQ_1:38;
end;
hence q'^<%x%> = q by A47,A41b,AFINSQ_1:def 4;
end;
q' = p
proof
A60: ex m being Nat st X\{x} c= m by A30,XBOOLE_1:1;
A61: (p is XFinSequence of NAT & rng p = X\{x} & for l,m,k1,k2 being Nat
st ( l < m & m < len p & k1=p.l & k2=p.m) holds k1 < k2)
proof
thus p is XFinSequence of NAT by A31,AFINSQ_1:34;
thus rng p = X\{x}
proof
A62: not x in rng p
proof
assume x in rng p;
then consider y such that
A63: y in dom p & x=p.y by FUNCT_1:def 5;
reconsider y as Element of NAT by A63;
A66: y < len p & len p < len (p^<%x%>)
proof
y in len p by A63,AFINSQ_1:def 1;
hence y < len p by A63,NAT_1:45;
len p + 1 = len p + len <%x%> by AFINSQ_1:38
.= len (p^<%x%>) by AFINSQ_1:20;
hence len p < len (p^<%x%>) by XREAL_1:31;
end;
A67: m = (p^<%x%>).y by A63,AFINSQ_1:def 4;
m = (p^<%x%>).(len p ) by AFINSQ_1:40;
hence contradiction by A31,A66,A67;
end;
A68: X = rng p \/ rng <%x%> by A31,AFINSQ_1:29
.= rng p \/ {x} by AFINSQ_1:36;
for z holds z in rng p \/ {x} \ {x} iff z in rng p
proof
let z;
thus z in rng p \/ {x} \ {x} implies z in rng p
proof
assume z in rng p \/ {x} \ {x};
then (z in rng p \/ {x}) & not z in {x} by XBOOLE_0:def 4;
hence z in rng p by XBOOLE_0:def 2;
end;
assume
A69: z in rng p;
then
A70: not z in {x} by A62,TARSKI:def 1;
z in rng p \/ {x} by A69,XBOOLE_0:def 2;
hence z in rng p \/ {x} \ {x} by A70, XBOOLE_0:def 4;
end;
hence rng p = X\{x} by A68,TARSKI:2;
end; thus
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
A71: l < m & m < len p & k1=p.l & k2=p.m;
then l < len p by XXREAL_0:2;
then BB:l in len p & len p=dom p by NAT_1:45,AFINSQ_1:def 1;
then
A72: k1 = (p^<%x%>).l by A71,AFINSQ_1:def 4;
m in dom p by BB,A71,NAT_1:45;
then
A73: k2 = (p^<%x%>).m by A71,AFINSQ_1:def 4;
len p < len p + 1 by XREAL_1:31;
then m < len p + 1 by A71,XXREAL_0:2;
then m < len p + len <%x%> by AFINSQ_1:38;
then l < m & m < len (p^<%x%>) by A71, AFINSQ_1:20;
hence k1 < k2 by A31,A72,A73;
end;
end;
rng f = X\{x} & for l,m,k1,k2 being Nat st
(l < m & m < len f & k1=f.l & k2=f.m) holds k1 < k2
proof
thus rng f = X\{x}
proof
A74: not x in rng f
proof
assume x in rng f;
then consider y such that
A75: y in dom f & x=f.y by FUNCT_1:def 5;
reconsider y as Element of NAT by A75;
A78: y < len f & len f < len (f^<%x%>)
proof
len f=dom f by AFINSQ_1:def 1;
hence y < len f by A75,NAT_1:45;
len f + 1 = len f + len <%x%> by AFINSQ_1:38
.= len (f^<%x%>) by AFINSQ_1:20;
hence len f < len (f^<%x%>) by XREAL_1:31;
end;
A79: m = q.y by A46,A75,AFINSQ_1:def 4;
m = q.(len f) by A46,AFINSQ_1:40;
hence contradiction by A32,A46,A78,A79;
end;
A80: X = rng f \/ rng <%x%> by A32,A46,AFINSQ_1:29
.= rng f \/ {x} by AFINSQ_1:36;
for z holds z in rng f \/ {x} \ {x} iff z in rng f
proof
let z;
thus z in rng f \/ {x} \ {x} implies z in rng f
proof
assume z in rng f \/ {x} \ {x};
then (z in rng f \/ {x}) & not z in {x} by XBOOLE_0:def 4;
hence z in rng f by XBOOLE_0:def 2;
end;
assume
A81: z in rng f;
then
A82: not z in {x} by A74,TARSKI:def 1;
z in rng f \/ {x} by A81,XBOOLE_0:def 2;
hence z in rng f \/ {x} \ {x} by A82, XBOOLE_0:def 4;
end;
hence rng f = X\{x} by A80,TARSKI:2;
end;
thus 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
A83: l < m & m < len f & k1=f.l & k2=f.m;
then
A84: l < m & m < len q by A40,A41b,NAT_1:13;
l in n & m in n
proof
l < n by A41b,A83,XXREAL_0:2;
hence l in n by NAT_1:45;
thus m in n by A41b,A83,NAT_1:45;
end;
then k1 = q.l & k2 = q.m by A41n,A83;
hence k1 < k2 by A32,A84;
end;
end;
hence q'=p by A29,A60,A61;
end;
hence q = p^<%x%> by A46;
end;
for p being XFinSequence holds S[p] from AFINSQ_1:sch 3(A27,A28);
hence p = q by A6,A25,A26;
end;
end;
registration
let A be finite natural-membered set;
cluster Sgm0 A -> one-to-one;
coherence
proof
consider k being Nat such that
A1: A c= k by AE221f;
for x,y being set 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 set;
assume that
A2: x in dom(Sgm0 A) & 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 A2;
reconsider k0=k as Element of NAT by ORDINAL1:def 13;
(Sgm0(A)).x in rng(Sgm0 A) & (Sgm0(A)).y in rng(Sgm0 A) & rng(Sgm0 A) = A
by A2,AC113,FUNCT_1:def 5;
then reconsider m = (Sgm0(A)).x, n = (Sgm0(A)).y as Element of NAT
by A1,AB470;
per cases by A4,REAL_1:def 5;
suppose
A6: i < j;
j < len(Sgm0 A) by A2,NAT_1:45;
hence contradiction by A6,AC113,A3;
end;
suppose
A7: j < i;
i < len(Sgm0 A) by A2,NAT_1:45;
hence contradiction by A7,AC113,A3;
end;
end;
hence thesis by FUNCT_1:def 8;
end;
end;
theorem Th44: ::from FINSEQ_3:44
for A being finite natural-membered set holds len(Sgm0 A) = Card A
proof
let A be finite natural-membered set;
dom(Sgm0 A) = (len(Sgm0 A)) & rng(Sgm0 A) = A & Sgm0 A is one-to-one
by AC113;
then (len(Sgm0 A)),A are_equipotent & (len(Sgm0 A)) is finite
by WELLORD2:def 4;
then card((len(Sgm0 A))) = len(Sgm0 A) & card A = card((len(Sgm0 A)))
by CARD_1:21;
hence thesis;
end;
theorem AE200: 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 A1: X c= Y & X <> {};
A3: rng (Sgm0 X)=X by AC113;
A4: rng (Sgm0 Y)=Y by AC113;
reconsider X0=X,Y0=Y as finite set;
0 <> card X0 by A1;then
0 < len (Sgm0 X) by Th44;then
0 in dom (Sgm0 X) by NAT_1:45;then
(Sgm0 X).0 in X by A3,FUNCT_1:def 5;then
consider x being set such that
A20: x in dom (Sgm0 Y) & (Sgm0 Y).x=(Sgm0 X).0 by FUNCT_1:def 5,A1,A4;
reconsider nx=x as Nat by A20;
A21: nx nx;
hence (Sgm0 Y).0 <= (Sgm0 X).0 by A20,AC113,A21;
end;
case 0=nx;
hence (Sgm0 Y).0 <=(Sgm0 X).0 by A20;
end;
end;
hence (Sgm0 Y).0 <= (Sgm0 X).0;
end;
theorem AE205: for n being Nat holds (Sgm0 {n}).0=n
proof let n be Nat;
A3: rng (Sgm0 {n})={n} by AC113;
A4: len (Sgm0 {n})=card {n} by Th44;
0 in dom (Sgm0 {n}) by NAT_1:45,A4;then
(Sgm0 {n}).0 in rng (Sgm0 {n}) by FUNCT_1:def 5;
hence (Sgm0 {n}).0=n by A3,TARSKI:def 1;
end;
definition let B1,B2 be set;
pred B1 {};
consider x being Element of B1/\B2/\NAT;
B2: x in B1/\B2 & x in NAT by B1,XBOOLE_0:def 3;
reconsider nx=x as Nat;
nx in B1 & nx in B2 by B2,XBOOLE_0:def 3;
hence contradiction by AE100,A1;
end;
hence B1/\B2/\NAT={};
end;
theorem AE101: for B1,B2 being finite natural-membered set st
B1 {} by XBOOLE_0:def 7;
consider x being Element of B1 /\ B2;
x in B1 & x in B2 by B2,XBOOLE_0:def 3;
hence contradiction by A1,AE100;
end;
hence B1 misses B2;
end;
theorem AE400: for A,B1,B2 being set st B1 {} & (ex x being set st x in X & {x} {} &
(ex x being set st x in X & {x} Card Y by A1;then
0 < len (Sgm0 Y) by Th44;then
0 in dom (Sgm0 Y) by NAT_1:45;then
A10: (Sgm0 Y).0 in Y by A4,FUNCT_1:def 5;
set nx=x0;
nx in {x0} by TARSKI:def 1;then
A14: nx<=(Sgm0 Y).0 by A10,A2,AE102;
(Sgm0 {x0}).0=nx by AE205;
hence (Sgm0 X).0 <= (Sgm0 Y).0 by A12,A14,XXREAL_0:2;
end;
theorem AE221e: for X0,Y0 being finite natural-membered set, i being Nat st
X0 {} by A1,XBOOLE_1:15,CARD_1:47;
set f0=(Sgm0 (X0\/Y0));
A30: rng f0=X0 \/Y0 by AC113;
set f=(Sgm0 (X0\/Y0))|(card X0);
set Z={ v where v is Element of X0 \/Y0: ex k2 being Nat st v=f.k2 &
k2 in card X0};
A2: dom f=len f;
A33: len (Sgm0 (X0\/Y0))=Card (X0\/Y0) by Th44;
A22n: X0 c= X0 \/ Y0 by XBOOLE_1:7;
A22: card X0 <= len (Sgm0 (X0\/Y0)) by XBOOLE_1:7,A33,NAT_1:44;
A4: len f=card X0 by TH80,A33,NAT_1:44,A22n;
A4d: len f0=card (X0 \/Y0) by Th44;
B4: rng f c= rng (Sgm0 (X0 \/ Y0)) by RELAT_1:99;
A3: rng f c= Z
proof let y being set; assume
B1: y in rng f;then
consider x being set such that
B2: x in dom f & y=f.x by FUNCT_1:def 5;
reconsider nx=x as Nat by B2;
B3: nx in card X0 by B2,TH80,A33,NAT_1:44,A22n,A2;
reconsider y0=y as Element of (X0 \/Y0) by B1,B4,AC113;
ex k2 being Nat st y0=f.k2 & k2 in card X0 by B3,B2;
hence y in Z;
end;
A40n: Z c= rng f
proof let y being set;assume y in Z;then
consider v0 being Element of X0 \/Y0 such that
B2: y=v0 & ex k2 being Nat st v0=f.k2 & k2 in card X0;
thus y in rng f by B2,FUNCT_1:def 5,A4;
end;then
A40: rng f=Z by A3,XBOOLE_0:def 10;
A50n: now assume B1: not Z c= X0 & not X0 c= Z;then
consider v1 being set such that
B2: v1 in Z & not v1 in X0 by TARSKI:def 3;
consider v2 being set such that
B3: v2 in X0 & not v2 in Z by TARSKI:def 3,B1;
consider v10 being Element of X0 \/Y0 such that
B4: v1=v10 & ex k2 being Nat st v10=f.k2 & k2 in card X0 by B2;
B98: v10 in Y0 by A20,XBOOLE_0:def 2,B2,B4;
consider k20 being Nat such that
B4b: v10=f.k20 & k20 in card X0 by B4;
reconsider nv10 =v10 as Nat;
X0 c= X0\/Y0 by XBOOLE_1:7;then
consider x2 being set such that
B5: x2 in dom f0 & v2=f0.x2 by FUNCT_1:def 5,B3,A30;
reconsider x20=x2 as Nat by B5;
reconsider nv2 =v2 as Nat by B5;
B61n: now assume C0: x20 < card X0;
card X0 <= card (X0 \/Y0) by NAT_1:44,XBOOLE_1:7;then
C4: card X0 <= len f0 & x20 in card X0 by Th44,C0,NAT_1:45;then
f.x20=f0.x20 by Th19;
hence contradiction by B3,B5,C4,A22n;
end;
k20 {} by A1,XBOOLE_1:15,CARD_1:47;
set f0=(Sgm0 (X\/Y));
A30: rng f0=X \/Y by AC113;
set f=(Sgm0 (X\/Y))|(card X);
set Z={ v where v is Element of X \/Y: ex k2 being Nat st v=f.k2 &
k2 in card X};
A33: len (Sgm0 (X\/Y))=Card (X\/Y) by Th44;
A22: card X <= len (Sgm0 (X\/Y)) by XBOOLE_1:7,A33,NAT_1:44;then
A4: len f=card X by TH80;
B4: rng f c= rng (Sgm0 (X\/Y)) by RELAT_1:99;
A3: rng f c= Z
proof let y being set;assume
B1: y in rng f;then
consider x being set such that
B2: x in dom f & y=f.x by FUNCT_1:def 5;
reconsider nx=x as Nat by B2;
reconsider y0=y as Element of X\/Y by B1,B4,AC113;
ex k2 being Nat st y0=f.k2 & k2 in card X by A4,B2;
hence y in Z;
end;
Z c= rng f
proof let y being set;assume y in Z;then
consider v0 being Element of X \/Y such that
B2: y=v0 & ex k2 being Nat st v0=f.k2 & k2 in card X;
thus y in rng f by B2,FUNCT_1:def 5,A4;
end;then
A40: rng f=Z by A3,XBOOLE_0:def 10;
A50n: now assume B1: not Z c= X & not X c= Z;then
consider v1 being set such that
B2: v1 in Z & not v1 in X by TARSKI:def 3;
consider v2 being set such that
B3: v2 in X & not v2 in Z by TARSKI:def 3,B1;
consider v10 being Element of X \/Y such that
B4: v1=v10 & ex k2 being Nat st v10=f.k2 & k2 in card X by B2;
B98: v10 in Y by A20,XBOOLE_0:def 2,B2,B4;
consider k20 being Nat such that
B4b: v10=f.k20 & k20 in card X by B4;
reconsider nv10 =v10 as Nat;
X c= X\/Y by XBOOLE_1:7;then
consider x2 being set such that
B5: x2 in dom f0 & v2=f0.x2 by FUNCT_1:def 5,B3,A30;
reconsider x20=x2 as Nat by B5;
reconsider nv2 =v2 as Nat by B5;
now assume C0: x20 < card X;
card X <= card (X \/Y) by NAT_1:44,XBOOLE_1:7;then
C4: card X <= len f0 & x20 in card X by C0,NAT_1:45,Th44;then
f.x20=f0.x20 by Th19;
hence contradiction by B3,B5,A40,FUNCT_1:def 5,C4,A4;
end;then
B61: len f <=x20 by TH80,A22;
k20 {} by A1,XBOOLE_1:15,CARD_1:47;
set f0=(Sgm0 (X0\/Y0));
A30: rng f0=X0 \/Y0 by AC113;
set f=(Sgm0 (X0\/Y0))/^(card X0);
set Z={ v where v is Element of X0 \/Y0: ex k2 being Nat st
v=f.k2 & k2 in card Y0};
A33: len (Sgm0 (X0\/Y0))=Card (X0\/Y0) by Th44;
A22: card X0 <= len (Sgm0 (X0\/Y0)) by A33,NAT_1:44,XBOOLE_1:7;
A74: len f=len f0 -' (card X0) by Def2
.=len f0 - (card X0) by A22,BINARITH:50;
X0/\Y0=(X0/\(Y0/\NAT)) by A1e,XBOOLE_1:28,1,A1d
.= (X0/\Y0/\NAT) by XBOOLE_1:16
.={} by A1,AG110;then
A72: X0 misses Y0 by XBOOLE_0:def 7;
A73: (X0\/Y0)\X0=(X0\X0)\/(Y0\X0) by XBOOLE_1:42
.={} \/ (Y0\X0) by XBOOLE_1:37
.=Y0 by XBOOLE_1:83,A72;
A4: len f=card Y0 by A74,A33,A73,CARD_2:63,XBOOLE_1:7;
len f0=card (X0 \/Y0) by Th44;then
A4e: len f0=(card X0)+(card Y0) by A72,CARD_2:53;
B4: rng f c= rng (Sgm0 (X0\/Y0)) by AG170;
A3: rng f c= Z
proof let y being set;assume
B1: y in rng f;then
consider x being set such that
B2: x in dom f & y=f.x by FUNCT_1:def 5;
reconsider nx=x as Nat by B2;
reconsider y0=y as Element of X0\/Y0 by B1,B4,AC113;
ex k2 being Nat st y0=f.(k2) & k2 in card Y0 by B2,A4;
hence y in Z;
end;
A40n: Z c= rng f
proof let y being set;assume y in Z;then
consider v0 being Element of X0 \/Y0 such that
B2: y=v0 & ex k2 being Nat st v0=f.k2 & k2 in card Y0;
thus y in rng f by B2,FUNCT_1:def 5,A4;
end;then
A40: rng f=Z by A3,XBOOLE_0:def 10;
A50n: now assume B1: not Z c= Y0 & not Y0 c= Z;then
consider v1 being set such that
B2: v1 in Z & not v1 in Y0 by TARSKI:def 3;
consider v2 being set such that
B3: v2 in Y0 & not v2 in Z by TARSKI:def 3,B1;
consider v10 being Element of X0 \/Y0 such that
B4: v1=v10 & ex k2 being Nat st v10=f.k2 & k2 in card Y0 by B2;
B98: v10 in X0 by A20,XBOOLE_0:def 2,B2,B4;
consider k20 being Nat such that
B4b: v10=f.k20 & k20 in card Y0 by B4;
reconsider nv10 =v10 as Nat;
Y0 c= X0\/Y0 by XBOOLE_1:7;then
consider x2 being set such that
B5: x2 in dom f0 & v2=f0.x2 by FUNCT_1:def 5,B3,A30;
reconsider x20=x2 as Nat by B5;
set nx20=x20 -' (card X0);
B57d: v2 in X0 \/Y0 by A30,B5,FUNCT_1:def 5;
reconsider ev2=v2 as Element of X0\/Y0 by A30,B5,FUNCT_1:def 5;
reconsider nv2 =v2 as Nat by B5;
B36n: now assume C0bn: x20 >= card X0;then
C0b: x20-'card X0=x20-card X0 by BINARITH:50;
x20x20 by B36n,XXREAL_0:2;
k20nv2 by B5,B53,AC113,B62,B4b;
hence contradiction by AE100,A1,B3,B98;
end;
A51: dom f,(f.:(dom f)) are_equipotent by CARD_1:60;
f.:(dom f)=rng f by RELAT_1:146;then
Card Z=card (len f) by A40,A51,CARD_1:21;then
A53: Card Z=Card Y0 by A74,A33,A73,CARD_2:63,XBOOLE_1:7;then
Y0,Z are_equipotent by CARD_1:21;then
reconsider Z0=Z as finite set by CARD_1:68;
A77n: now per cases by A50n;
case Z0 c= Y0;
hence Z0=Y0 by CARD_FIN:1,A53;
end;
case Y0 c=Z0;
hence Z0=Y0 by CARD_FIN:1,A53;
end;
end;
i+card X0 < len f0 by A1,A4,XREAL_1:22,A74;
hence thesis by A3,XBOOLE_0:def 10,A40n,A77n,Th19b;
end;
theorem AE222f: for X,Y being finite natural-membered set,i being Nat st
X {} & X {} & X 0 by A1;
0 {} & X {} & X 0 by A1;
0{} by CARD_1:47,Th44;
A8: len r = card(X1 \/ Y1) by Th44
.= card X1 + card Y1 by A7,CARD_2:53
.= len p + card Y1 by Th44
.= len p + len q by Th44;
defpred P[Element of NAT] means $1 in dom p implies r.$1 = p.$1;
A9: P[0] by A40,A51,AE220;
A10: now
let k be Element of NAT;
assume
A11: P[k];
thus P[k+1]
proof
assume
A12: k + 1 in dom p;
assume
A13: r.(k + 1) <> p.(k + 1);
A14: p.(k + 1) in rng p & rng p c= NAT by A12,ORDINAL1:def 8,FUNCT_1:def 5;
reconsider n = p.(k + 1) as Element of NAT by ORDINAL1:def 13;
len p <= len r by A8,NAT_1:12;
then
A15: (len p) c= (len r) by NAT_1:40;
then
A17: r.(k + 1) in rng r & rng r c= NAT by A12,ORDINAL1:def 8,FUNCT_1:def 5;
reconsider m = r.(k + 1) as Element of NAT by ORDINAL1:def 13;
A18: n in X & m in X \/ Y by A14,A17,AC113;
now per cases;
suppose
A19: k in dom p;
reconsider n1 = p.k as Element of NAT by ORDINAL1:def 13;
reconsider m1 = r.k as Element of NAT by ORDINAL1:def 13;
now per cases by A13,XXREAL_0:1;
suppose
A20: m < n;
then not m in Y by AE100,A40,A18;
then m in X by A18,XBOOLE_0:def 2;
then m in rng p by AC113;
then consider x such that
A21: x in dom p and
A22: p.x = m by FUNCT_1:def 5;
reconsider x as Element of NAT by A21;
k < k + 1 & k + 1 < len r
by NAT_1:45,XREAL_1:31,A15,A12;
then
A23: n1 < m by A11,A19,AC113;
k < len p by A19,NAT_1:45;
then
A24: k < x by A22,A23,Th46;
x < len p by A21,NAT_1:45;
then x < k + 1 by A20,A22,Th46;
hence contradiction by A24,NAT_1:13;
end;
suppose
A25: n < m;
n in X \/ Y by A18,XBOOLE_0:def 2;
then n in rng r by AC113;
then consider x such that
A26: x in dom r and
A27: r.x = n by FUNCT_1:def 5;
reconsider x as Element of NAT by A26;
k < k + 1 & k + 1 < len p by A12,NAT_1:45,XREAL_1:31;
then
A28: m1 < n by A11,A19,AC113;
k < len r by A15,A19,NAT_1:45;
then
A29: k < x by A27,A28,Th46;
x < len r by A26,NAT_1:45;
then x < k + 1 by A25,A27,Th46;
hence contradiction by A29,NAT_1:13;
end;
end;
hence contradiction;
end;
suppose not k in dom p;
then (len p <= k) & k < k + 1 by NAT_1:45,XREAL_1:31;
then
(len p < k + 1 & k + 1 < len p) by A12, NAT_1:45,XXREAL_0:2;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
A37: for k being Element of NAT holds P[k] from NAT_1:sch 1(A9,A10);
defpred P[Element of NAT] means $1 in dom q implies r.(len p + $1) = q.$1;
len q>0 implies Y <>{} by CARD_1:47,Th44;then
A38: P[0] by A40,AE222;
A39: now
let k be Element of NAT;
assume
A40: P[k];
thus P[k+1]
proof
assume
A41: k + 1 in dom q;
assume
A42: r.(len p + (k + 1)) <> q.(k + 1);
set a = len p + (k + 1);
A43: q.(k + 1) in rng q & rng q c= NAT by A41,ORDINAL1:def 8,FUNCT_1:def 5;
reconsider n = q.(k + 1) as Element of NAT by ORDINAL1:def 13;
k + 1 XFinSequence equals
f*Sgm0(B /\ len f);
coherence
proof
B/\ len f c= dom f by XBOOLE_1:17;
then rng Sgm0(B/\ len f) c= dom f by AC113;
hence f*Sgm0(B/\ len f) is XFinSequence by AFINSQ_1:13;
end;
end;
theorem AC200:
for f being XFinSequence for B being set holds
len SubXFinS (f,B)=Card (B/\ (len f)) &
(for i being Nat st i < len SubXFinS (f,B) holds
SubXFinS (f,B).i=f.((Sgm0 (B/\ (len f))).i))
proof let f being XFinSequence, B be set;
B/\ len f c= dom f by XBOOLE_1:17;
then rng Sgm0(B/\ len f) c= dom f by AC113;
then dom SubXFinS (f,B) = len Sgm0(B/\ len f) by RELAT_1:46
.= Card(B/\ len f) by Th44;
hence len SubXFinS (f,B)=Card (B/\ len f);
let i be Nat;
assume i < len SubXFinS (f,B);
then i in dom SubXFinS (f,B) by NAT_1:45;
hence SubXFinS (f,B).i = f.((Sgm0(B/\ len f)).i) by FUNCT_1:22;
end;
definition let D be set;let f be XFinSequence of D, B be set;
redefine func SubXFinS(f,B) -> XFinSequence of D;
coherence
proof
A: rng f c= D by ORDINAL1:def 8;
rng (SubXFinS(f,B))c= rng f by RELAT_1:45;
then rng (SubXFinS(f,B)) c= D by A,XBOOLE_1:1;
hence SubXFinS(f,B) is XFinSequence of D by ORDINAL1:def 8;
end;
end;
registration
let f be XFinSequence;
cluster SubXFinS (f,{}) -> empty;
coherence
proof
len (SubXFinS (f,{})) =card {} by AC200;
hence SubXFinS (f,{})= {};
end;
end;
registration let B be set;
cluster SubXFinS ({},B) -> empty;
coherence;
end;
theorem for B1,B2 being finite natural-membered set,
f being XFinSequence of REAL st
B1 0;
set f3=SubXFinS(f,B1);
F3: len f3=Card (B1/\(len f)) by AC200;
per cases;
suppose D1: len f3>0;
set f4=SubXFinS(f,B2);
F4: len f4=Card (B2/\(len f)) by AC200;
A1b: B1 /\ (len f)<>{} by CARD_1:47,D1,AC200;
per cases;
suppose E1: len f4>0;
consider g1 being XFinSequence of REAL such that
E2: len f3=len g1 & f3.0=g1.0 & (for i being Nat st i+1= len g1;
set X0=B10/\(len f);
set Y0=B20/\(len f);
per cases by G1,REAL_1:def 5;
suppose i+1>len g1;then
i>=len g1 by NAT_1:13;then
i-'len g1=i-len g1 by BINARITH:50;then
reconsider i1=i-len g1 as Nat;
G67: i+1=i1+1+len f3 by E2.=i1+1+card(X0) by AC200;
G3dn: i+1-len g10 by AC200,E1; then
f4.(0)=f2.(i+1) by H0,G21,G20,AC200,E2,F3,F4h,G55,A92,XREAL_1:31;
hence g4.(i+1)=(g4.i)+(f2.(i+1)) by G2,G4,E3,AC500,E1;
end;
end;
end;
R4n: len g3>=(0 qua Element of NAT)+1 by E3,E4,E1,NAT_1:13;then
R4: len g3-'1=len g3-1 by BINARITH:50;
len g1 + len g3>= (0 qua Element of NAT)+1 by E8b,C1,NAT_1:13;then
R2: len g1 + len g3 -'1=len g1 + len g3 -1 by BINARITH:50
.= len g1 +(len g3-1)
.= len g1 +(len g3-'1) by R4n,BINARITH:50;
len g3-'1