:: Introduction to Theory of Rearrangment
:: by Yuji Sakai and Jaros{\l}aw Kotowicz
::
:: Received May 22, 1993
:: Copyright (c) 1993-2026 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, REAL_1, XBOOLE_0, MEMBERED, PARTFUN1,
VALUED_1, FUNCT_1, RELAT_1, FINSEQ_1, NAT_1, XXREAL_0, FINSET_1, CARD_1,
ARYTM_1, TARSKI, ARYTM_3, ZFMISC_1, ORDINAL4, RFINSEQ, RFUNCT_3,
CLASSES1, CARD_3, PBOOLE, FINSEQ_2, FUNCT_3, VALUED_0, REARRAN1, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, MEMBERED, FUNCT_1,
RELSET_1, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, NAT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, VALUED_1, RFUNCT_1,
FINSEQOP, RVSUM_1, CLASSES1, RFINSEQ, RFUNCT_3;
constructors REAL_1, NAT_1, FINSEQOP, RVSUM_1, RFINSEQ, RFUNCT_3, CLASSES1,
RELSET_1, BINOP_2;
registrations SUBSET_1, RELSET_1, PARTFUN1, FINSET_1, NUMBERS, XXREAL_0,
XREAL_0, NAT_1, MEMBERED, FINSEQ_1, VALUED_0, CARD_1, FINSEQ_2, FUNCT_1,
INT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, FINSEQ_2, RELAT_1;
expansions TARSKI, XBOOLE_0;
theorems FINSEQ_1, NAT_1, FUNCT_1, FINSEQ_2, TARSKI, CARD_2, CARD_1, PARTFUN1,
FINSET_1, FINSEQ_3, RFUNCT_1, RVSUM_1, ZFMISC_1, RFINSEQ, RFUNCT_3,
RELAT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, FUNCOP_1, ORDINAL1,
VALUED_1, CLASSES1, INT_1, XREAL_0;
schemes NAT_1, FINSEQ_1;
begin
reserve n,m,k for Nat,
x,y for set,
r for Real;
definition
let D be non empty set, E be real-membered set,
F be PartFunc of D,E, r be Real;
redefine func r(#)F -> Element of PFuncs(D,REAL); :: redefines (#) (VALUED_1, definition)
coherence
proof
reconsider F as PartFunc of D,E;
r(#)F is PartFunc of D,REAL;
hence thesis by PARTFUN1:45;
end;
end;
Lm1: for f be Function,x be object st not x in rng f holds f"{x}={}
proof
let f be Function,x be object;
assume
A1: not x in rng f;
rng f misses {x}
proof
set y = the Element of rng f /\ {x};
assume rng f /\ {x} <> {};
then y in rng f & y in {x} by XBOOLE_0:def 4;
hence contradiction by A1,TARSKI:def 1;
end;
hence thesis by RELAT_1:138;
end;
definition
let IT be FinSequence;
attr IT is terms've_same_card_as_number means
:Def1:
for n be Nat st 1<=n &
n<=len IT for B being finite set st B = IT.n holds card B = n;
attr IT is ascending means
:Def2:
for n be Nat st 1<=n & n<=len IT - 1 holds IT.n c= IT.(n+1);
end;
Lm2: for D be non empty finite set, A be FinSequence of bool D, k be Nat
st 1 <= k & k <= len A holds A.k is finite
proof
let D be non empty finite set, A be FinSequence of bool D, k be Nat;
assume 1 <= k & k <= len A;
then k in dom A by FINSEQ_3:25;
then A.k in bool D by FINSEQ_2:11;
hence thesis;
end;
Lm3: for D be non empty finite set, A be FinSequence of bool D st len A = card
D & A is terms've_same_card_as_number for B being finite set st B = A.(len A)
holds B = D
proof
let D be non empty finite set, A be FinSequence of bool D;
assume that
A1: len A = card D and
A2: A is terms've_same_card_as_number;
A3: 0+1<=len A by A1,NAT_1:13;
then len A in dom A by FINSEQ_3:25;
then
A4: A.(len A) in bool D by FINSEQ_2:11;
let B be finite set such that
A5: B = A.(len A);
assume B <> D;
then
A6: B c< D by A5,A4;
card B = card D by A1,A2,A5,A3;
hence contradiction by A6,CARD_2:48;
end;
Lm4: for D be non empty finite set holds ex B be FinSequence of bool(D) st len
B = card D & B is ascending & B is terms've_same_card_as_number
proof
let D be non empty finite set;
defpred P[Nat] means for D be non empty finite set st card D = $1
holds ex B be FinSequence of bool(D) st len B = card D & B is ascending & B is
terms've_same_card_as_number;
A1: for n st P[n] holds P[n+1]
proof
let n;
assume
A2: P[n];
let D be non empty finite set;
assume
A3: card D = n+1;
set x = the Element of D;
set Y = D\{x};
{x} c= D by ZFMISC_1:31;
then
A4: card Y = card D - card {x} by CARD_2:44
.= n+1-1 by A3,CARD_1:30
.= n;
now
per cases;
case
A5: n=0;
set f = <*D*>;
A6: len f = 1 by FINSEQ_1:39;
A7: rng f = {D} by FINSEQ_1:39;
rng f c= bool D
proof
let z be object;
assume z in rng f;
then z=D by A7,TARSKI:def 1;
hence thesis by ZFMISC_1:def 1;
end;
then reconsider f as FinSequence of bool D by FINSEQ_1:def 4;
take f;
thus card D = len f by A3,A5,FINSEQ_1:40;
thus f is ascending
by A6,XXREAL_0:2;
thus f is terms've_same_card_as_number
proof
let m be Nat;
assume 1<=m & m<=len f;
then
A8: m = 1 by A6,XXREAL_0:1;
let B be finite set;
assume B = f.m;
hence thesis by A3,A5,A8;
end;
end;
case
n<>0;
then reconsider Y as non empty finite set by A4;
D in bool D by ZFMISC_1:def 1;
then
A9: {D} c= bool D by ZFMISC_1:31;
consider f be FinSequence of bool Y such that
A10: len f = card Y and
A11: f is ascending and
A12: f is terms've_same_card_as_number by A2,A4;
set g = f ^ <*D*>;
A13: rng <*D*> = {D} & rng g = rng f \/ rng <*D*> by FINSEQ_1:31,39;
bool Y c= bool D by ZFMISC_1:67;
then rng f c= bool D;
then rng g c= bool D \/ bool D by A9,A13,XBOOLE_1:13;
then reconsider g as FinSequence of bool D by FINSEQ_1:def 4;
take g;
A14: len <*D*> = 1 by FINSEQ_1:39;
then
A15: len g = len f + 1 by FINSEQ_1:22;
thus len g = card D by A3,A4,A10,A14,FINSEQ_1:22;
thus g is ascending
proof
let m be Nat;
assume that
A16: 1 <= m and
A17: m <= len g - 1;
m in dom f by A15,A16,A17,FINSEQ_3:25;
then
A18: g.m = f.m by FINSEQ_1:def 7;
per cases;
suppose
A19: m=len f;
then reconsider gm = g.m as finite set by A16,A18,Lm2;
gm = Y & g.(m+1) = D by A10,A12,A18,A19,Lm3,FINSEQ_1:42;
hence thesis;
end;
suppose
m<>len f;
then m<len f by A15,A17,XXREAL_0:1;
then
A20: m+1<=len f by NAT_1:13;
1<=m+1 by A16,NAT_1:13;
then m+1 in dom f by A20,FINSEQ_3:25;
then
A21: g.(m+1) = f.(m+1) by FINSEQ_1:def 7;
m<=len f -1 by A20,XREAL_1:19;
hence thesis by A11,A16,A18,A21;
end;
end;
thus g is terms've_same_card_as_number
proof
let m be Nat such that
A22: 1<=m and
A23: m<=len g;
let B be finite set such that
A24: B = g.m;
per cases;
suppose
m=len g;
hence thesis by A3,A4,A10,A15,A24,FINSEQ_1:42;
end;
suppose
m<>len g;
then m<len g by A23,XXREAL_0:1;
then
A25: m<=len f by A15,NAT_1:13;
then m in dom f by A22,FINSEQ_3:25;
then g.m= f.m by FINSEQ_1:def 7;
hence thesis by A12,A22,A24,A25;
end;
end;
end;
end;
hence thesis;
end;
A26: P[ 0 ];
for n holds P[n] from NAT_1:sch 2(A26,A1);
hence thesis;
end;
definition
let X be set;
let IT be FinSequence of X;
attr IT is length_equal_card_of_set means
ex B being finite set st B = union X & len IT = card B;
end;
registration
let D be non empty finite set;
cluster terms've_same_card_as_number ascending length_equal_card_of_set
for FinSequence of bool(D);
existence
proof
consider B be FinSequence of bool(D) such that
A1: len B = card D & B is ascending & B is terms've_same_card_as_number by Lm4;
take B;
union bool D = D by ZFMISC_1:81;
hence thesis by A1;
end;
end;
definition
let D be non empty finite set;
mode RearrangmentGen of D is terms've_same_card_as_number ascending
length_equal_card_of_set FinSequence of bool(D);
end;
reserve C,D for non empty finite set,
a for FinSequence of bool D;
theorem Th1:
for a be FinSequence of bool D holds a is
length_equal_card_of_set iff len a = card D
proof
let A be FinSequence of bool D;
thus A is length_equal_card_of_set implies len A = card D
by ZFMISC_1:81;
assume
A1: len A = card D;
take D;
thus thesis by A1,ZFMISC_1:81;
end;
theorem Th2:
for a be FinSequence holds a is ascending iff for n,m st n<=m & n
in dom a & m in dom a holds a.n c= a.m
proof
let A be FinSequence;
thus A is ascending implies for n,m st n<=m & n in dom A & m in dom A holds
A.n c= A.m
proof
defpred P[Nat] means for n st n<=$1 & n in dom A & $1 in dom A
holds A.n c= A.$1;
assume
A1: A is ascending;
A2: for m st P[m] holds P[m+1]
proof
let m;
assume
A3: P[m];
let n;
assume that
A4: n<=m+1 and
A5: n in dom A and
A6: m+1 in dom A;
now
per cases;
case
n=m+1;
hence thesis;
end;
case
n<>m+1;
then n<m+1 by A4,XXREAL_0:1;
then
A7: n<=m by NAT_1:13;
1<=n by A5,FINSEQ_3:25;
then
A8: 1<=m by A7,XXREAL_0:2;
A9: m+1<=len A by A6,FINSEQ_3:25;
m<=m+1 by NAT_1:11;
then m<=len A by A9,XXREAL_0:2;
then m in dom A by A8,FINSEQ_3:25;
then
A10: A.n c= A.m by A3,A5,A7;
m<=len A - 1 by A9,XREAL_1:19;
then A.m c= A.(m+1) by A1,A8;
hence thesis by A10;
end;
end;
hence thesis;
end;
let n,m;
assume
A11: n<=m & n in dom A & m in dom A;
A12: P[ 0 ];
for m holds P[m] from NAT_1:sch 2(A12,A2);
hence thesis by A11;
end;
assume
A13: for n,m st n<=m & n in dom A & m in dom A holds A.n c= A.m;
let n be Nat;
assume that
A14: 1<=n and
A15: n<=len A - 1;
A16: n+1<=len A by A15,XREAL_1:19;
n<=n+1 by NAT_1:11;
then n<=len A by A16,XXREAL_0:2;
then
A17: n in dom A by A14,FINSEQ_3:25;
1<=n+1 by NAT_1:11;
then n+1 in dom A by A16,FINSEQ_3:25;
hence thesis by A13,A17,NAT_1:11;
end;
theorem Th3:
for a be terms've_same_card_as_number length_equal_card_of_set
FinSequence of bool D holds a.(len a) = D
proof
let A be terms've_same_card_as_number length_equal_card_of_set FinSequence
of bool D;
A1: len A = card D by Th1;
then 1 <= len A by NAT_1:14;
then A.(len A) is finite set by Lm2;
hence thesis by A1,Lm3;
end;
theorem Th4:
for a be length_equal_card_of_set FinSequence of bool D holds len a <> 0
proof
let A be length_equal_card_of_set FinSequence of bool D;
assume len A = 0;
then card(D)=0 by Th1;
hence contradiction;
end;
theorem Th5:
for a be ascending terms've_same_card_as_number FinSequence of
bool D holds for n,m holds n in dom a & m in dom a & n<>m implies a.n <> a.m
proof
let A be ascending terms've_same_card_as_number FinSequence of bool D;
let n,m;
assume that
A1: n in dom A and
A2: m in dom A and
A3: n <> m & A.n = A.m;
A4: 1 <= m & m <= len A by A2,FINSEQ_3:25;
A5: 1 <= n & n <= len A by A1,FINSEQ_3:25;
reconsider Am = A.m as finite set by A4,Lm2;
card(Am)=m by A4,Def1;
hence contradiction by A3,A5,Def1;
end;
theorem
for a be ascending terms've_same_card_as_number FinSequence of bool D
holds for n holds 1 <= n & n <= len a - 1 implies a.n <> a.(n+1)
proof
let A be ascending terms've_same_card_as_number FinSequence of bool D;
let n;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
n<=n+1 by NAT_1:11;
then n<=len A by A3,XXREAL_0:2;
then
A4: n in dom A by A1,FINSEQ_3:25;
1<=n+1 by NAT_1:11;
then
A5: n+1 in dom A by A3,FINSEQ_3:25;
n <> n+1;
hence thesis by A4,A5,Th5;
end;
Lm5: n in dom a implies a.n c= D
proof
assume n in dom a;
then a.n in bool D by FINSEQ_2:11;
hence thesis;
end;
theorem Th7:
for a be terms've_same_card_as_number FinSequence of bool D st n
in dom a holds a.n <> {}
proof
let A be terms've_same_card_as_number FinSequence of bool D;
assume n in dom A;
then
A1: 1<=n & n<=len A by FINSEQ_3:25;
assume A.n = {};
hence contradiction by A1,Def1,CARD_1:27;
end;
theorem Th8:
for a be terms've_same_card_as_number FinSequence of bool D st 1
<=n & n<=len a - 1 holds a.(n+1) \ a.n <> {}
proof
let A be terms've_same_card_as_number FinSequence of bool D;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
n<=n+1 by NAT_1:11;
then
A4: n<=len A by A3,XXREAL_0:2;
then reconsider An1 = A.(n+1), An = A.n as finite set by A1,A3,Lm2,NAT_1:11;
1<=n+1 by NAT_1:11;
then
A5: card (An1) = n+1 by A3,Def1;
assume A.(n+1) \ A.n = {};
then
A6: A.(n+1) c= A.n by XBOOLE_1:37;
card (An) = n by A1,A4,Def1;
then n+1 <= n by A5,A6,NAT_1:43;
then 1<=n-n by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
theorem Th9:
for a be terms've_same_card_as_number length_equal_card_of_set
FinSequence of bool D ex d be Element of D st a.1 = {d}
proof
let A be terms've_same_card_as_number length_equal_card_of_set FinSequence
of bool D;
len A <> 0 by Th4;
then
A1: 0+1<=len A by NAT_1:13;
then reconsider A1 = A.1 as finite set by Lm2;
card(A1)=1 by A1,Def1;
then consider x being object such that
A2: {x} = A.1 by CARD_2:42;
1 in dom A by A1,FINSEQ_3:25;
then A.1 c= D by Lm5;
then reconsider x as Element of D by A2,ZFMISC_1:31;
take x;
thus thesis by A2;
end;
theorem Th10:
for a be terms've_same_card_as_number ascending FinSequence of
bool D st 1<=n & n<=len a - 1 ex d be Element of D st a.(n+1) \ a.n = {d} & a.(
n+1) = a.n \/ {d} & a.(n+1) \ {d} = a.n
proof
let A be terms've_same_card_as_number ascending FinSequence of bool D;
assume that
A1: 1<=n and
A2: n<=len A - 1;
A3: n+1<=len A by A2,XREAL_1:19;
A4: A.n c= A.(n+1) by A1,A2,Def2;
n<=n+1 by NAT_1:11;
then
A5: n<=len A by A3,XXREAL_0:2;
then reconsider An1 = A.(n+1), An = A.n as finite set by A1,A3,Lm2,NAT_1:11;
A6: card(An) = n by A1,A5,Def1;
A7: 1<=n+1 by NAT_1:11;
then card(An1) = n+1 by A3,Def1;
then card (An1 \ An) = n+1-n by A4,A6,CARD_2:44
.= 1;
then consider x being object such that
A8: {x} = A.(n+1) \ A.n by CARD_2:42;
x in A.(n+1) \ A.n by A8,ZFMISC_1:31;
then
A9: not x in A.n by XBOOLE_0:def 5;
A10: x in A.(n+1) by A8,ZFMISC_1:31;
n+1 in dom A by A3,A7,FINSEQ_3:25;
then A.(n+1) c= D by Lm5;
then reconsider x as Element of D by A10;
take x;
thus {x} = A.(n+1) \ A.n by A8;
thus A.n \/ {x} = A.(n+1) \/ A.n by A8,XBOOLE_1:39
.= A.(n+1) by A4,XBOOLE_1:12;
hence A.(n+1) \ {x} = (A.n \ {x}) \/ ({x} \ {x}) by XBOOLE_1:42
.= (A.n \ {x}) \/ {} by XBOOLE_1:37
.= A.n by A9,ZFMISC_1:57;
end;
definition
let D be non empty finite set, A be RearrangmentGen of D;
func Co_Gen A -> RearrangmentGen of D means
for m be Nat st 1 <= m & m <= len it - 1 holds it.m = D \ A.(len A -m);
existence
proof
deffunc F(Nat)= D \ A.(len A -$1);
set c = card D;
D c= D;
then reconsider y = D as Subset of D;
0+1 <= c by NAT_1:13;
then max(0,c -1) = c - 1 by FINSEQ_2:4;
then reconsider c1=c - 1 as Element of NAT by FINSEQ_2:5;
consider f be FinSequence such that
A1: len f = c1 and
A2: for m be Nat st m in dom f holds f.m = F(m) from FINSEQ_1:sch 2;
A3: dom f = Seg c1 by A1,FINSEQ_1:def 3;
rng f c= bool D
proof
let x be object;
assume x in rng f;
then consider m being Nat such that
A4: m in dom f & f.m = x by FINSEQ_2:10;
D \ A.(len A -m) c= D;
then x is Subset of D by A2,A4;
hence thesis;
end;
then reconsider f as FinSequence of bool(D) by FINSEQ_1:def 4;
set C = f^<*y*>;
A5: len C = len f + len <*y*> by FINSEQ_1:22
.= len f + 1 by FINSEQ_1:39;
A6: card D = len A by Th1;
A7: C is terms've_same_card_as_number
proof
let m be Nat;
assume that
A8: 1 <= m and
A9: m <= len C;
max(0,len C -m) = len C -m by A9,FINSEQ_2:4;
then reconsider l = len C - m as Element of NAT by FINSEQ_2:5;
let B be finite set such that
A10: B = C.m;
now
per cases;
case
m = len C;
hence thesis by A1,A5,A10,FINSEQ_1:42;
end;
case
m <> len C;
then m < len C by A9,XXREAL_0:1;
then
A11: m+1 <= len C by NAT_1:13;
then
A12: 1 <= l by XREAL_1:19;
A13: l <= len A by A6,A1,A5,XREAL_1:43;
then
A14: l in dom A by A12,FINSEQ_3:25;
then reconsider Al = A.l as finite set by Lm5,FINSET_1:1;
m <= len C - 1 by A11,XREAL_1:19;
then
A15: m in dom f by A5,A8,FINSEQ_3:25;
then C.m = f.m by FINSEQ_1:def 7
.= D \ A.l by A6,A1,A2,A5,A15;
hence card B = card(D) - card(Al) by A10,A14,Lm5,CARD_2:44
.= len A - l by A6,A12,A13,Def1
.= m by A6,A1,A5;
end;
end;
hence thesis;
end;
for m be Nat st 1 <= m & m <= len C - 1 holds C.m c= C.(m+1)
proof
let m be Nat;
assume that
A16: 1 <= m and
A17: m <= len C - 1;
A18: m in dom f by A5,A16,A17,FINSEQ_3:25;
then
A19: C.m = f.m by FINSEQ_1:def 7
.= D \ A.(len A - m) by A2,A18;
per cases;
suppose
m = len C - 1;
then C.(m+1) = D by A5,FINSEQ_1:42;
hence thesis by A19;
end;
suppose
m <> len C - 1;
then
A20: m < len C - 1 by A17,XXREAL_0:1;
then
A21: m+1 < len A by A6,A1,A5,XREAL_1:20;
then max(0,len A -(m+1)) = len A -(m+1) by FINSEQ_2:4;
then reconsider l = len A -(m+1) as Element of NAT by FINSEQ_2:5;
A22: 1 <= m+1 by NAT_1:11;
m+1<= len C - 1 by A5,A20,NAT_1:13;
then
A23: m+1 in dom f by A5,A22,FINSEQ_3:25;
then
A24: C.(m+1) = f.(m+1) by FINSEQ_1:def 7
.= D \ A.l by A2,A23;
m+1+1<=len A by A21,NAT_1:13;
then
A25: 1 <= len A - (m+1) by XREAL_1:19;
l <= len A - 1 by A22,XREAL_1:13;
then A.l c= A.(l+1) by A25,Def2;
hence thesis by A19,A24,XBOOLE_1:34;
end;
end;
then reconsider C as RearrangmentGen of D by A1,A5,A7,Def2,Th1;
take C;
let m be Nat;
assume 1 <= m & m <= len C - 1;
then
A26: m in Seg c1 by A1,A5,FINSEQ_1:1;
then m in dom f by A1,FINSEQ_1:def 3;
hence C.m = f.m by FINSEQ_1:def 7
.= D \ A.(len A -m) by A2,A3,A26;
end;
uniqueness
proof
let f1,f2 be RearrangmentGen of D such that
A27: for m be Nat st 1 <= m & m <= len f1 - 1 holds f1.m = D \ A.(len A -m) and
A28: for m be Nat st 1 <= m & m <= len f2 - 1 holds f2.m = D \ A.(len A -m);
A29: len f2 = card D by Th1;
A30: len A = card D by Th1;
A31: len f1 = card D by Th1;
then
A32: dom f1 = Seg len A by A30,FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1=m as Element of NAT by ORDINAL1:def 12;
assume
A33: m in dom f1;
then
A34: 1<=m by A32,FINSEQ_1:1;
A35: m<=len A by A32,A33,FINSEQ_1:1;
per cases;
suppose
A36: m = len A;
then f1.m = D by A31,A30,Th3;
hence f1.m = f2.m by A29,A30,A36,Th3;
end;
suppose
m <> len A;
then m<len A by A35,XXREAL_0:1;
then m+1<=len A by NAT_1:13;
then
A37: m<=len A - 1 by XREAL_1:19;
then f1.m1 = D \ A.(len A -m1) by A27,A31,A30,A34;
hence f1.m = f2.m by A28,A29,A30,A34,A37;
end;
end;
hence thesis by A31,A29,FINSEQ_2:9;
end;
involutiveness
proof let B,A be RearrangmentGen of D such that
A38: for m be Nat st 1 <= m & m <= len B - 1 holds B.m = D \ A.(len A -m);
let m be Nat such that
A39: 1 <= m & m <= len A - 1;
A40: len A = card D by Th1;
A41: len B = card D by Th1;
len A -1 < len A by XREAL_1:44;
then
A42: m < len A by A39,XXREAL_0:2;
then len A - m in NAT by INT_1:5;
then reconsider n = len B - m as Nat by A40,A41;
A43: len A - n = m by A40,A41;
m+1 <= len A by A39,XREAL_1:19;
then
A44: 1 <= n by A40,A41,XREAL_1:19;
A45: n <= len B - 1 by A39,XREAL_1:10;
len A - n in dom A by A43,A39,A42,FINSEQ_3:25;
then
A46: A.(len A -n) c= D by Lm5;
thus A.m = A.(len A -n) by A40,A41
.= D /\ A.(len A -n) by A46,XBOOLE_1:28
.= D \ (D \ A.(len A -n)) by XBOOLE_1:48
.= D \ B.(len B -m) by A44,A45,A38;
end;
end;
::$CT
theorem Th11:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds len MIM FinS(F,D) = len CHI(A,C)
proof
let F be PartFunc of D,REAL, A be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set a = FinS(F,D);
reconsider a9 = a as finite Function;
A3: dom F = D by A1,PARTFUN1:def 2;
then reconsider F9 = F as finite Function by FINSET_1:10;
reconsider da9 = dom a9, dF9 = dom F9 as finite set;
A4: F|D = F by A3,RELAT_1:68;
D = dom F /\ D by A3
.= dom(F|D) by RELAT_1:61;
then F, FinS(F,D) are_fiberwise_equipotent by A4,RFUNCT_3:def 13;
then
A5: dom a = Seg len a & card da9 = card dF9 by CLASSES1:81,FINSEQ_1:def 3;
thus len CHI(A,C) = len A by RFUNCT_3:def 6
.= card C by Th1
.= len a by A2,A3,A5,FINSEQ_1:57
.= len MIM(a) by RFINSEQ:def 2;
end;
definition
let D,C be non empty finite set, A be RearrangmentGen of C, F be PartFunc of
D,REAL;
func Rland (F,A) -> PartFunc of C,REAL equals
Sum (MIM(FinS(F,D)) (#) CHI(A,
C));
correctness;
func Rlor(F,A) -> PartFunc of C,REAL equals
Sum (MIM(FinS(F,D)) (#) CHI(
Co_Gen A,C));
correctness;
end;
theorem Th12:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds dom Rland(F,A) = C
proof
let F be PartFunc of D,REAL, A be RearrangmentGen of C;
A1: len CHI(A,C) = len A & len A <> 0 by Th4,RFUNCT_3:def 6;
assume F is total & card C = card D;
then
A2: len MIM(FinS(F,D)) = len CHI(A,C) by Th11;
thus dom Rland(F,A) c= C;
let x be object;
assume x in C;
then reconsider c = x as Element of C;
len (MIM(FinS(F,D))(#) CHI(A,C)) = min(len MIM(FinS(F,D)), len CHI(A,C))
& c is_common_for_dom (MIM(FinS(F,D)) (#) CHI(A,C)) by RFUNCT_3:32,def 7;
hence thesis by A2,A1,RFUNCT_3:28;
end;
theorem Th13:
for c be Element of C, F be PartFunc of D,REAL, A be
RearrangmentGen of C st F is total & card C = card D holds (c in A.1 implies (
MIM(FinS(F,D)) (#) CHI(A,C))#c = MIM(FinS(F,D))) & for n st 1<=n & n<len A & c
in A.(n+1) \ A.n holds (MIM(FinS(F,D)) (#) CHI(A,C))#c = (n |-> (0 qua Real)) ^
(MIM(FinS(F,D)/^n))
proof
let c be Element of C, F be PartFunc of D,REAL, A be RearrangmentGen of C;
set fd = FinS(F,D), mf = MIM(fd), h = CHI(A,C), fh = (mf(#)h)#c;
A1: dom A = Seg len A by FINSEQ_1:def 3;
A2: dom(mf(#)h) =Seg len(mf(#)h) by FINSEQ_1:def 3;
A3: len h = len A by RFUNCT_3:def 6;
A4: len mf = len fd by RFINSEQ:def 2;
A5: dom fh = Seg len fh by FINSEQ_1:def 3;
A6: min(len mf,len h) = len(mf(#)h) by RFUNCT_3:def 7;
assume F is total & card C = card D;
then
A7: len mf = len h by Th11;
A8: len fh =len(mf(#)h) by RFUNCT_3:def 8;
A9: dom h = Seg len h by FINSEQ_1:def 3;
thus c in A.1 implies (mf (#) h)#c = mf
proof
assume
A10: c in A.1;
A11: for n st n in dom A holds c in A.n
proof
let n;
assume
A12: n in dom A;
then
A13: 1<=n by FINSEQ_3:25;
n<=len A by A12,FINSEQ_3:25;
then 1<=len A by A13,XXREAL_0:2;
then 1 in dom A by FINSEQ_3:25;
then A.1 c= A.n by A12,A13,Th2;
hence thesis by A10;
end;
A14: dom ((mf(#)h)#c) = Seg len mf by A7,A6,A8,FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1=fd.m as Real;
assume
A15: m in dom((mf(#)h)#c);
then
A16: 1<=m by FINSEQ_3:25;
A17: h.m = chi(A.m,C) by A9,A5,A7,A6,A8,A15,RFUNCT_3:def 6;
A18: c in A.m by A1,A5,A7,A3,A6,A8,A11,A15;
m in dom mf by A14,A15,FINSEQ_1:def 3;
then
A19: m<=len mf by FINSEQ_3:25;
now
per cases;
case
A20: m=len mf;
then mf.m = r1 by A4,RFINSEQ:def 2;
then (mf(#)h).m = r1(#)chi(A.m,C) by A2,A5,A8,A15,A17,RFUNCT_3:def 7;
then
A21: ((mf(#)h)#c).m = (r1(#)chi(A.m,C)).c by A15,RFUNCT_3:def 8;
dom(r1(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = r1*(chi(A.m,C)).c by A21,VALUED_1:def 5
.= r1*1 by A18,RFUNCT_1:63
.= mf.m by A4,A20,RFINSEQ:def 2;
end;
case
A22: m<>len mf;
reconsider r2=fd.(m+1) as Real;
m<len mf by A19,A22,XXREAL_0:1;
then m+1<=len mf by NAT_1:13;
then
A23: m<=len mf - 1 by XREAL_1:19;
then mf.m1 = r1-r2 by A16,RFINSEQ:def 2;
then (mf(#)h).m = (r1-r2)(#)chi(A.m,C) by A2,A5,A8,A15,A17,
RFUNCT_3:def 7;
then
A24: ((mf(#)h)#c).m =((r1-r2)(#)chi(A.m,C)).c by A15,RFUNCT_3:def 8;
dom((r1-r2)(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = (r1-r2)*(chi(A.m,C)).c by A24,VALUED_1:def 5
.= (r1-r2)*1 by A18,RFUNCT_1:63
.= mf.m1 by A16,A23,RFINSEQ:def 2;
end;
end;
hence ((mf(#)h)#c).m = mf.m;
end;
hence thesis by A7,A6,A8,FINSEQ_2:9;
end;
let n;
assume that
A25: 1<=n and
A26: n<len A and
A27: c in A.(n+1) \ A.n;
A28: len(mf/^n) = len mf - n by A7,A3,A26,RFINSEQ:def 1;
A29: for k st k in dom A & k<=n holds not c in A.k
proof
let k;
assume
A30: k in dom A & k<=n;
assume
A31: c in A.k;
n in dom A by A25,A26,FINSEQ_3:25;
then A.k c= A.n by A30,Th2;
hence contradiction by A27,A31,XBOOLE_0:def 5;
end;
A32: c in A.(n+1) by A27;
A33: n+1<=len A by A26,NAT_1:13;
A34: 1<=n+1 by A25,NAT_1:13;
A35: for k st k in dom A & n+1<=k holds c in A.k
proof
let k;
assume
A36: k in dom A & n+1<=k;
n+1 in dom A by A33,A34,FINSEQ_3:25;
then A.(n+1) c= A.k by A36,Th2;
hence thesis by A32;
end;
set fdn = FinS(F,D)/^n, mfn = MIM(fdn), n0 = n |-> (0 qua Real);
A37: len mfn = len fdn by RFINSEQ:def 2;
A38: len n0 = n by CARD_1:def 7;
len fdn = len fd - n by A7,A3,A4,A26,RFINSEQ:def 1;
then
A39: len (n0 ^ mfn) = n + (len fd -n) by A37,A38,FINSEQ_1:22
.= len mf by RFINSEQ:def 2;
then
A40: dom(n0^mfn) = Seg len mf by FINSEQ_1:def 3;
A41: dom n0 = Seg len n0 by FINSEQ_1:def 3;
now
let m be Nat;
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
reconsider r1=fd.m as Real;
assume
A42: m in dom (n0^mfn);
then
A43: 1<=m by FINSEQ_3:25;
m in dom mf by A40,A42,FINSEQ_1:def 3;
then
A44: m<=len mf by FINSEQ_3:25;
A45: h.m = chi(A.m,C) by A9,A7,A40,A42,RFUNCT_3:def 6;
now
per cases;
case
A46: m<=n;
reconsider r2=fd.(m+1) as Real;
m<n+1 by A46,NAT_1:13;
then m<len A by A33,XXREAL_0:2;
then m+1<=len A by NAT_1:13;
then m<=len mf - 1 by A7,A3,XREAL_1:19;
then mf.m1 = r1-r2 by A43,RFINSEQ:def 2;
then (mf(#)h).m = (r1-r2)(#)chi(A.m,C) by A2,A7,A6,A40,A42,A45,
RFUNCT_3:def 7;
then
A47: ((mf(#)h)#c).m =((r1-r2)(#)chi(A.m,C)).c by A5,A7,A6,A8,A40,A42,
RFUNCT_3:def 8;
not c in A.m by A1,A7,A3,A29,A40,A42,A46;
then
A48: chi(A.m,C).c = 0 by RFUNCT_1:64;
A49: m in Seg n by A43,A46,FINSEQ_1:1;
A50: n0.m = 0;
dom((r1-r2)(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = (r1-r2)*(chi(A.m,C)).c by A47,VALUED_1:def 5
.= (n0^mfn).m by A38,A41,A48,A49,A50,FINSEQ_1:def 7;
end;
case
A51: n<m;
then max(0,m-n) = m-n by FINSEQ_2:4;
then reconsider mn = m-n as Element of NAT by FINSEQ_2:5;
A52: n+1<=m by A51,NAT_1:13;
then c in A.m by A1,A7,A3,A35,A40,A42;
then
A53: chi(A.m,C).c = 1 by RFUNCT_1:63;
A54: 1<=mn by A52,XREAL_1:19;
now
per cases;
case
A55: m = len mf;
then mf.m = r1 by A4,RFINSEQ:def 2;
then (mf(#)h).m = r1(#)chi(A.m,C) by A2,A7,A6,A40,A42,A45,
RFUNCT_3:def 7;
then
A56: ((mf(#)h)#c).m =(r1(#)chi(A.m,C)).c by A5,A7,A6,A8,A40,A42,
RFUNCT_3:def 8;
A57: mn in dom(mf/^n) by A28,A54,A55,FINSEQ_3:25;
A58: (n0^mfn).m = mfn.(m-n) by A38,A39,A44,A51,FINSEQ_1:24
.=(mf/^n).mn by RFINSEQ:15
.= mf.(mn+n) by A7,A3,A26,A57,RFINSEQ:def 1
.= r1 by A4,A55,RFINSEQ:def 2;
dom(r1(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = r1*(chi(A.m,C)).c by A56,VALUED_1:def 5
.= (n0^mfn).m by A53,A58;
end;
case
A59: m<>len mf;
reconsider r2=fd.(m+1) as Real;
m<len mf by A44,A59,XXREAL_0:1;
then m+1<=len mf by NAT_1:13;
then
A60: m<=len mf - 1 by XREAL_1:19;
then mf.m1 = r1-r2 by A43,RFINSEQ:def 2;
then (mf(#)h).m = (r1-r2)(#)chi(A.m,C) by A2,A7,A6,A40,A42,A45,
RFUNCT_3:def 7;
then
A61: ((mf(#)h)#c).m =((r1-r2)(#)chi(A.m,C)).c by A5,A7,A6,A8,A40,A42,
RFUNCT_3:def 8;
mn<=len(mf/^n) by A28,A44,XREAL_1:9;
then
A62: mn in dom(mf/^n) by A54,FINSEQ_3:25;
A63: (n0^mfn).m = mfn.(m-n) by A38,A39,A44,A51,FINSEQ_1:24
.=(mf/^n).mn by RFINSEQ:15
.= mf.(mn+n) by A7,A3,A26,A62,RFINSEQ:def 1
.= r1-r2 by A43,A60,RFINSEQ:def 2;
dom((r1-r2)(#)chi(A.m,C)) = dom chi(A.m,C) by VALUED_1:def 5
.= C by RFUNCT_1:61;
hence ((mf(#)h)#c).m = (r1-r2)*(chi(A.m,C)).c by A61,VALUED_1:def 5
.= (n0^mfn).m by A53,A63;
end;
end;
hence ((mf(#)h)#c).m = (n0^mfn).m;
end;
end;
hence ((mf(#)h)#c).m = (n0^mfn).m;
end;
hence thesis by A7,A6,A8,A39,FINSEQ_2:9;
end;
theorem Th14:
for c be Element of C, F be PartFunc of D,REAL, A be
RearrangmentGen of C st F is total & card C = card D holds (c in A.1 implies (
Rland(F,A)).c = FinS(F,D).1) & for n st 1<=n & n<len A & c in A.(n+1) \ A.n
holds Rland(F,A).c = FinS(F,D).(n+1)
proof
let c be Element of C, F be PartFunc of D,REAL, B be RearrangmentGen of C;
set fd = FinS(F,D), mf = MIM(fd), h = CHI(B,C);
A1: Rland(F,B).c = Sum((mf(#)h)#c) by RFUNCT_3:32,33;
A2: len h = len B & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
assume
A3: F is total & card C = card D;
then
A4: len mf = len h by Th11;
thus c in B.1 implies Rland(F,B).c = FinS(F,D).1
proof
assume c in B.1;
hence Rland(F,B).c = Sum mf by A3,A1,Th13
.= FinS(F,D).1 by A4,A2,Th4,RFINSEQ:16;
end;
let n;
set mfn = MIM(FinS(F,D)/^n);
assume that
A5: 1<=n and
A6: n<len B and
A7: c in B.(n+1) \ B.n;
(mf(#)h)#c = (n |-> (0 qua Real)) ^ mfn by A3,A5,A6,A7,Th13;
hence Rland(F,B).c = Sum(n |-> In(0,REAL)) + (Sum mfn)
by A1,RVSUM_1:75
.= 0 + Sum mfn by RVSUM_1:81
.= FinS(F,D).(n+1) by A4,A2,A6,RFINSEQ:17;
end;
theorem Th15:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds rng Rland(F,A) = rng FinS(F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set fd = FinS(F,D), p = Rland(F,B), mf = MIM(fd), h = CHI(B,C);
A3: len mf = len h by A1,A2,Th11;
A4: dom F = D by A1,PARTFUN1:def 2;
then reconsider fd9 = fd, F9 = F as finite Function by FINSET_1:10;
reconsider dfd = dom fd9, dF = dom F9 as finite set;
A5: len h = len B & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
A6: dom p = C by A1,A2,Th12;
A7: dom fd = Seg len fd by FINSEQ_1:def 3;
A8: dom B = Seg len B by FINSEQ_1:def 3;
F|D = F by A4,RELAT_1:68;
then fd, F are_fiberwise_equipotent by A4,RFUNCT_3:def 13;
then card dfd = card dF by CLASSES1:81;
then len fd <> 0 by A4,A7;
then
A9: 0+1<=len fd by NAT_1:13;
then
A10: 1 in dom fd by FINSEQ_3:25;
thus rng p c= rng fd
proof
let x be object;
assume x in rng p;
then consider c be Element of C such that
c in dom p and
A11: p.c = x by PARTFUN1:3;
defpred P[set] means $1 in dom B & c in B.$1;
A12: ex n be Nat st P[n]
proof
take n = len B;
B.n = C by Th3;
hence thesis by A3,A5,A9,FINSEQ_3:25;
end;
consider mi be Nat such that
A13: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A12);
A14: 1<=mi by A13,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A15: mi<=len B by A13,FINSEQ_3:25;
now
per cases;
case
mi = 1;
then p.c = fd.1 by A1,A2,A13,Th14;
hence thesis by A10,A11,FUNCT_1:def 3;
end;
case
mi <> 1;
then 1<mi by A14,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A16: 1<=m1 by XREAL_1:19;
A17: m1<mi by XREAL_1:44;
then m1<=len B by A15,XXREAL_0:2;
then m1 in dom B by A16,FINSEQ_3:25;
then not c in B.m1 by A13,XREAL_1:44;
then
A18: c in B.(m1+1) \ B.m1 by A13,XBOOLE_0:def 5;
m1<len B by A15,A17,XXREAL_0:2;
then p.c = fd.(m1+1) by A1,A2,A16,A18,Th14;
hence thesis by A3,A5,A7,A8,A11,A13,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
let x be object;
defpred P[Nat] means $1 in dom fd & fd.$1 = x;
assume x in rng fd;
then
A19: ex n be Nat st P[n] by FINSEQ_2:10;
consider mi be Nat such that
A20: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A19);
A21: 1<=mi by A20,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A22: mi<=len fd by A20,FINSEQ_3:25;
now
per cases;
case
A23: mi=1;
set y = the Element of B.1;
A24: B.1 <> {} by A3,A5,A7,A8,A10,Th7;
B.1 c= C by A3,A5,A7,A8,A10,Lm5;
then reconsider y as Element of C by A24;
p.y = fd.1 by A1,A2,A24,Th14;
hence thesis by A6,A20,A23,FUNCT_1:def 3;
end;
case
A25: mi<>1;
set y = the Element of B.(m1+1) \ B.m1;
1<mi by A21,A25,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A26: 1<=m1 by XREAL_1:19;
m1+1<=len fd by A20,FINSEQ_3:25;
then m1<=len fd -1 by XREAL_1:19;
then
A27: B.(m1+1) \ B.m1 <> {} by A3,A5,A26,Th8;
then
A28: y in B.(m1+1) by XBOOLE_0:def 5;
B.mi c= C by A3,A5,A7,A8,A20,Lm5;
then reconsider y as Element of C by A28;
m1<mi by XREAL_1:44;
then m1<len fd by A22,XXREAL_0:2;
then p.y=fd.(m1+1) by A1,A2,A3,A5,A26,A27,Th14;
hence thesis by A6,A20,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
theorem Th16:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds Rland(F,A), FinS(F,D) are_fiberwise_equipotent
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set fd = FinS(F,D), p = Rland(F,B), mf = MIM(fd), h = CHI(B,C);
dom p is finite;
then reconsider p as finite PartFunc of C,REAL by FINSET_1:10;
A1: len h = len B & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
A2: dom fd = Seg len fd & dom B = Seg len B by FINSEQ_1:def 3;
assume
A3: F is total & card C = card D;
then
A4: len mf = len h by Th11;
A5: dom p = C by A3,Th12;
A6: rng p = rng fd by A3,Th15;
now
let x be object;
now
per cases;
case
A7: not x in rng fd;
then fd"{x}={} by Lm1;
hence card (fd"{x}) = card(p"{x}) by A6,A7,Lm1;
end;
case
A8: x in rng fd;
defpred P[Nat] means $1 in dom fd & fd.$1 = x;
A9: for n be Nat st P[n] holds n<=len fd by FINSEQ_3:25;
A10: ex n be Nat st P[n] by A8,FINSEQ_2:10;
consider ma be Nat such that
A11: P[ma] & for n being Nat st P[n] holds n<=ma from NAT_1:sch 6(
A9,A10 );
A12: ex n be Nat st P[n] by A8,FINSEQ_2:10;
consider mi be Nat such that
A13: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A12
);
reconsider r=x as Real by A13;
A14: 1<=mi by A13,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A15: m1+1=mi;
A16: ma<=len fd by A11,FINSEQ_3:25;
A17: Seg ma \ Seg m1 = fd"{x}
proof
thus Seg ma \ Seg m1 c= fd"{x}
proof
let y be object;
assume
A18: y in Seg ma \ Seg m1;
then reconsider l=y as Element of NAT;
reconsider o=fd.l as Real;
A19: y in Seg ma by A18,XBOOLE_0:def 5;
then
A20: 1<=l by FINSEQ_1:1;
A21: l<=ma by A19,FINSEQ_1:1;
then l<=len fd by A16,XXREAL_0:2;
then
A22: l in dom fd by A20,FINSEQ_3:25;
not y in Seg m1 by A18,XBOOLE_0:def 5;
then l<1 or m1<l by FINSEQ_1:1;
then mi<l+1 by A19,FINSEQ_1:1,XREAL_1:19;
then
A23: mi<=l by NAT_1:13;
now
per cases;
case
l=ma;
then o in {x} by A11,TARSKI:def 1;
hence thesis by A22,FUNCT_1:def 7;
end;
case
l<>ma;
then l<ma by A21,XXREAL_0:1;
then
A24: o>=r by A11,A22,RFINSEQ:19;
now
per cases;
case
l=mi;
then o in {x} by A13,TARSKI:def 1;
hence thesis by A22,FUNCT_1:def 7;
end;
case
l<>mi;
then mi<l by A23,XXREAL_0:1;
then r>=o by A13,A22,RFINSEQ:19;
then r=o by A24,XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence thesis by A22,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let y be object;
assume
A25: y in fd"{x};
then
A26: y in dom fd by FUNCT_1:def 7;
reconsider l=y as Element of NAT by A25;
A27: 1<=l by A26,FINSEQ_3:25;
fd.y in {x} by A25,FUNCT_1:def 7;
then
A28: fd.l=x by TARSKI:def 1;
then mi<=l by A13,A26;
then mi<l+1 by NAT_1:13;
then m1<l or l<1 by XREAL_1:19;
then
A29: not l in Seg m1 by FINSEQ_1:1;
l<=ma by A11,A26,A28;
then l in Seg ma by A27,FINSEQ_1:1;
hence thesis by A29,XBOOLE_0:def 5;
end;
A30: 1<=ma by A11,FINSEQ_3:25;
A31: mi<=ma by A13,A11;
m1<=mi by XREAL_1:43;
then
A32: m1<=ma by A31,XXREAL_0:2;
then Seg m1 c= Seg ma by FINSEQ_1:5;
then
A33: card(fd"{x}) = card(Seg ma) - card(Seg m1) by A17,CARD_2:44
.= ma - card(Seg m1) by FINSEQ_1:57
.= ma - m1 by FINSEQ_1:57;
A34: mi<=len fd by A13,FINSEQ_3:25;
then 1<=len fd by A14,XXREAL_0:2;
then
A35: 1 in dom fd by FINSEQ_3:25;
now
per cases;
case
A36: mi=1;
B.ma = p"{x}
proof
thus B.ma c= p"{x}
proof
defpred P[Nat] means $1 in dom B & $1<=ma implies
for c be Element of C st c in B.$1 holds c in p"{x};
let y be object;
assume
A37: y in B.ma;
B.ma c= C by A4,A1,A2,A11,Lm5;
then reconsider cy = y as Element of C by A37;
A38: for n st P[n] holds P[n+1]
proof
let n;
assume
A39: P[n];
assume that
A40: n+1 in dom B and
A41: n+1<=ma;
A42: n+1<=len B by A40,FINSEQ_3:25;
then
A43: n<=len B -1 by XREAL_1:19;
A44: n<len B by A42,NAT_1:13;
let c be Element of C;
assume
A45: c in B.(n+1);
A46: n<=len B by A42,NAT_1:13;
now
per cases;
case
n=0;
then p.c = x by A3,A13,A36,A45,Th14;
then p.c in {x} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
case
A47: n<>0;
then
A48: 0+1<n+1 by XREAL_1:6;
A49: 0+1<=n by A47,NAT_1:13;
then B.n c= B.(n+1) by A43,Def2;
then
A50: B.(n+1) = B.(n+1) \/ B.n by XBOOLE_1:12
.= (B.(n+1) \ B.n) \/ B.n by XBOOLE_1:39;
now
per cases by A45,A50,XBOOLE_0:def 3;
case
c in B.(n+1) \ B.n;
then
A51: p.c = fd.(n+1) by A3,A44,A49,Th14;
now
per cases;
case
n+1=ma;
then p.c in {x} by A11,A51,TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
case
n+1<>ma;
then n+1<ma by A41,XXREAL_0:1;
then
A52: p.c>=r by A4,A1,A2,A11,A40,A51,RFINSEQ:19;
r>=p.c by A4,A1,A2,A13,A36,A40,A48,A51,RFINSEQ:19
;
then r=p.c by A52,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in B.n;
hence thesis by A39,A41,A46,A49,FINSEQ_3:25,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A53: P[ 0 ] by FINSEQ_3:25;
A54: for n holds P[n] from NAT_1:sch 2(A53,A38);
ma in dom B by A4,A1,A11,FINSEQ_3:29;
then cy in p"{x} by A37,A54;
hence thesis;
end;
let y be object;
assume
A55: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A55,FUNCT_1:def 7;
then
A56: p.cy = x by TARSKI:def 1;
defpred Q[Nat] means $1 in dom B & ma<$1 & cy in B.$1;
assume
A57: not y in B.ma;
A58: ex n be Nat st Q[n]
proof
take n=len B;
len B <> 0 by Th4;
then 0+1<=len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25;
A59: B.n= C by Th3;
now
assume n <= ma;
then ma=len B by A4,A1,A16,XXREAL_0:1;
then cy in B.ma by A59;
hence contradiction by A57;
end;
hence thesis by A59;
end;
consider mm be Nat such that
A60: Q[mm] & for n be Nat st Q[n] holds mm<=n from NAT_1:
sch 5(A58);
1<=mm by A60,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A60,NAT_1:13;
then
A61: ma<=1m by XREAL_1:19;
then
A62: 1<=1m by A30,XXREAL_0:2;
A63: mm in dom fd by A4,A1,A60,FINSEQ_3:29;
A64: mm<=len B by A60,FINSEQ_3:25;
A65: mm<mm+1 by NAT_1:13;
then 1m<mm by XREAL_1:19;
then
A66: 1m<len B by A64,XXREAL_0:2;
1m<=mm by A65,XREAL_1:19;
then 1m<=len B by A64,XXREAL_0:2;
then
A67: 1m in dom B by A62,FINSEQ_3:25;
now
per cases;
case
ma=1m;
then cy in B.(1m+1) \ B.(1m) by A57,A60,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A62,A66,Th14;
hence contradiction by A11,A56,A60,A63;
end;
case
ma <> 1m;
then
A68: ma < 1m by A61,XXREAL_0:1;
now
assume cy in B.(1m);
then mm<=1m by A60,A67,A68;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in B.(1m+1) \ B.(1m) by A60,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A62,A66,Th14;
hence contradiction by A11,A56,A60,A63;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(fd"{x}) by A4,A1,A30,A16,A33,A36,Def1;
end;
case
A69: mi<>1;
then 1<mi by A14,XXREAL_0:1;
then
A70: 1<=m1 by A15,NAT_1:13;
A71: m1<=len fd by A34,A15,NAT_1:13;
then
A72: m1 in dom B by A4,A1,A70,FINSEQ_3:25;
then
A73: B.m1 c= B.ma by A4,A1,A2,A11,A32,Th2;
B.ma c= C by A4,A1,A2,A11,Lm5;
then reconsider Bma = B.ma, Bm1 = B.m1 as finite set by A73;
B.ma \ B.m1 = p"{x}
proof
thus B.ma \ B.m1 c= p"{x}
proof
defpred P[Nat] means $1 in dom B & mi<=$1 & $1<=ma
implies for c be Element of C st c in B.$1 \ B.m1 holds c in p"{x};
let y be object;
A74: B.ma c= C by A4,A1,A2,A11,Lm5;
A75: for n st P[n] holds P[n+1]
proof
let n;
assume
A76: P[n];
assume that
A77: n+1 in dom B and
A78: mi<=n+1 and
A79: n+1<=ma;
let c be Element of C;
n+1<=len B by A77,FINSEQ_3:25;
then
A80: n<len B by NAT_1:13;
assume
A81: c in B.(n+1) \ B.m1;
now
per cases;
case
A82: n+1=mi;
then p.c = fd.(n+1) by A3,A70,A80,A81,Th14;
then p.c in {x} by A13,A82,TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
case
mi <> n+1;
then
A83: mi<n+1 by A78,XXREAL_0:1;
then mi<=n by NAT_1:13;
then
A84: 1<=n by A14,XXREAL_0:2;
n<=ma by A79,NAT_1:13;
then
A85: n<=len B by A4,A1,A16,XXREAL_0:2;
then n<=n+1 & n in dom B by A84,FINSEQ_3:25,NAT_1:11;
then B.n c= B.(n+1) by A77,Th2;
then
A86: B.(n+1) \ B.m1 = (B.(n+1) \/ B .n) \ B.m1 by XBOOLE_1:12
.= ((B.(n+1) \B.n) \/ B.n) \ B.m1 by XBOOLE_1:39
.= (B.(n+1) \ B.n)\ B.m1 \/ (B.n \ B.m1) by XBOOLE_1:42
;
now
per cases by A81,A86,XBOOLE_0:def 3;
case
c in (B.(n+1) \ B.n) \ B.m1;
then c in B.(n+1) \ B.n by XBOOLE_0:def 5;
then
A87: p.c = fd.(n+1) by A3,A80,A84,Th14;
now
per cases;
case
n+1=ma;
then p.c in {x} by A11,A87,TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
case
n+1<>ma;
then n+1<ma by A79,XXREAL_0:1;
then
A88: p.c>=r by A4,A1,A2,A11,A77,A87,RFINSEQ:19;
r>=p.c by A4,A1,A2,A13,A77,A83,A87,RFINSEQ:19;
then r=p.c by A88,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in B.n \ B.m1;
hence thesis by A76,A79,A83,A84,A85,FINSEQ_3:25
,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A89: P[ 0 ];
A90: for n holds P[n] from NAT_1:sch 2(A89,A75);
assume
A91: y in B.ma \ B.m1;
then y in B.ma;
then reconsider cy = y as Element of C by A74;
ma in dom B by A4,A1,A11,FINSEQ_3:29;
then cy in p"{x} by A31,A91,A90;
hence thesis;
end;
let y be object;
assume
A92: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A92,FUNCT_1:def 7;
then
A93: p.cy = x by TARSKI:def 1;
assume
A94: not y in B.ma \ B.m1;
now
per cases by A94,XBOOLE_0:def 5;
case
A95: not y in B.ma;
defpred Q[Nat] means $1 in dom B & ma<$1 & cy in B.$1;
A96: ex n be Nat st Q[n]
proof
take n=len B;
len B <> 0 by Th4;
then 0+1<=len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25;
A97: B.n= C by Th3;
now
assume n <= ma;
then ma=len B by A4,A1,A16,XXREAL_0:1;
then cy in B.ma by A97;
hence contradiction by A95;
end;
hence thesis by A97;
end;
consider mm be Nat such that
A98: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A96);
1<=mm by A98,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A98,NAT_1:13;
then
A99: ma<=1m by XREAL_1:19;
then
A100: 1<=1m by A30,XXREAL_0:2;
A101: mm in dom fd by A4,A1,A98,FINSEQ_3:29;
A102: mm<=len B by A98,FINSEQ_3:25;
A103: mm<mm+1 by NAT_1:13;
then 1m<mm by XREAL_1:19;
then
A104: 1m<len B by A102,XXREAL_0:2;
1m<=mm by A103,XREAL_1:19;
then 1m<=len B by A102,XXREAL_0:2;
then
A105: 1m in dom B by A100,FINSEQ_3:25;
now
per cases;
case
ma=1m;
then cy in B.(1m+1) \ B.(1m) by A95,A98,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A100,A104,Th14;
hence contradiction by A11,A93,A98,A101;
end;
case
ma <> 1m;
then
A106: ma < 1m by A99,XXREAL_0:1;
now
assume cy in B.(1m);
then mm<=1m by A98,A105,A106;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in B.(1m+1) \ B.(1m) by A98,XBOOLE_0:def 5;
then p.cy = fd.mm by A3,A100,A104,Th14;
hence contradiction by A11,A93,A98,A101;
end;
end;
hence contradiction;
end;
case
A107: y in B.m1;
defpred Q[Nat] means $1 in dom B & $1<=m1 & cy in B.$1;
A108: ex n be Nat st Q[n] by A72,A107;
consider mm be Nat such that
A109: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A108);
A110: 1<=mm by A109,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m=mm-1 as Element of NAT by FINSEQ_2:5;
A111: mm<=len B by A109,FINSEQ_3:25;
A112: mm in dom fd by A4,A1,A109,FINSEQ_3:29;
now
per cases;
case
mm=1;
then p.cy = fd.1 by A3,A109,Th14;
then mi<=1 by A13,A35,A93;
hence contradiction by A14,A69,XXREAL_0:1;
end;
case
mm<>1;
then 1<mm by A110,XXREAL_0:1;
then 1+1<=mm by NAT_1:13;
then
A113: 1<=1m by XREAL_1:19;
A114: mm<mm+1 by NAT_1:13;
then
A115: 1m<=mm by XREAL_1:19;
then 1m<=len B by A111,XXREAL_0:2;
then
A116: 1m in dom B by A113,FINSEQ_3:25;
A117: 1m<mm by A114,XREAL_1:19;
then
A118: 1m<len B by A111,XXREAL_0:2;
1m<=m1 by A109,A115,XXREAL_0:2;
then not cy in B.1m by A109,A117,A116;
then cy in B.(1m+1) \ B.1m by A109,XBOOLE_0:def 5;
then p.cy = fd.(1m+1) by A3,A113,A118,Th14;
then mi<=mm by A13,A93,A112;
then m1+1<=m1 by A109,XXREAL_0:2;
then 1<=m1-m1 by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(Bma) - card(Bm1) by A73,CARD_2:44
.= ma - card(Bm1) by A4,A1,A30,A16,Def1
.= card (fd"{x}) by A4,A1,A33,A70,A71,Def1;
end;
end;
hence card (fd"{x}) = card(p"{x});
end;
end;
hence card Coim(fd,x) = card Coim(p,x);
end;
hence thesis by CLASSES1:def 10;
end;
theorem Th17:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds FinS(Rland(F,A),C) = FinS(F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume
A1: F is total & card C = card D;
then
A2: Rland(F,B), FinS(F,D) are_fiberwise_equipotent by Th16;
A3: dom Rland(F,B) = C by A1,Th12;
then (Rland(F,B))|C = Rland(F,B) by RELAT_1:68;
hence thesis by A2,A3,RFUNCT_3:def 13;
end;
theorem Th18:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds Sum (Rland(F,A),C) = Sum (F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume F is total & card C = card D;
then FinS(Rland(F,B),C) = FinS(F,D) by Th17;
hence Sum(Rland(F,B),C) = Sum FinS(F,D) by RFUNCT_3:def 14
.= Sum (F,D) by RFUNCT_3:def 14;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds FinS(Rland(F,A) - r,C) = FinS(F-r,D) & Sum (Rland(F,A)-r,
C) = Sum (F-r,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rland(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th16;
then Rland(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then
A5: Rland(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
A6: dom (Rland(F,B) - r) = dom Rland (F,B) by VALUED_1:3;
then (Rland(F,B) - r)|C = Rland(F,B) -r by RELAT_1:68;
then FinS(Rland(F,B) - r, C), Rland(F,B) -r are_fiberwise_equipotent by A6,
RFUNCT_3:def 13;
then
A7: FinS(Rland(F,B) - r, C), F-r are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom(F-r) = dom F by VALUED_1:3;
then (F-r)|D = F-r by RELAT_1:68;
hence FinS(Rland(F,B) - r,C) = FinS(F-r,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(Rland(F,B)-r,C) = Sum FinS(F-r,D) by RFUNCT_3:def 14
.= Sum (F-r,D) by RFUNCT_3:def 14;
end;
theorem Th20:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds dom Rlor(F,A) = C
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set b = Co_Gen(B);
A1: len CHI(b,C) = len b & len (MIM(FinS(F,D))(#) CHI(b,C)) = min(len MIM(
FinS(F,D)), len CHI(b,C)) by RFUNCT_3:def 6,def 7;
assume F is total & card C = card D;
then
A2: len MIM(FinS(F,D)) = len CHI(b,C) & len b = card D by Th1,Th11;
thus dom Rlor(F,B) c= C;
let x be object;
assume x in C;
then reconsider c = x as Element of C;
c is_common_for_dom (MIM(FinS(F,D)) (#) CHI(b,C)) by RFUNCT_3:32;
hence thesis by A1,A2,RFUNCT_3:28;
end;
theorem Th21:
for c be Element of C, F be PartFunc of D,REAL, A be
RearrangmentGen of C st F is total & card C = card D holds (c in (Co_Gen A).1
implies (Rlor(F,A)).c = FinS(F,D).1) & for n st 1<=n & n<len (Co_Gen A) & c in
(Co_Gen A).(n+1) \ (Co_Gen A).n holds Rlor(F,A).c = FinS(F,D).(n+1)
proof
let c be Element of C, F be PartFunc of D,REAL, B be RearrangmentGen of C;
set fd = FinS(F,D), mf = MIM(fd), b = Co_Gen B, h = CHI(b,C);
A1: Rlor(F,B).c = Sum((mf(#)h)#c) by RFUNCT_3:32,33;
A2: len h = len b & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
assume
A3: F is total & card C = card D;
then
A4: len mf = len h by Th11;
thus c in b.1 implies Rlor(F,B).c = FinS(F,D).1
proof
assume c in b.1;
hence Rlor(F,B).c = Sum mf by A3,A1,Th13
.= FinS(F,D).1 by A4,A2,Th4,RFINSEQ:16;
end;
let n;
set mfn = MIM(FinS(F,D)/^n);
assume that
A5: 1<=n and
A6: n<len b and
A7: c in b.(n+1) \ b.n;
(mf(#)h)#c = (n |-> (0 qua Real)) ^ mfn by A3,A5,A6,A7,Th13;
hence Rlor(F,B).c = Sum(n |-> In(0,REAL)) + (Sum mfn)
by A1,RVSUM_1:75
.= 0 + Sum mfn by RVSUM_1:81
.= FinS(F,D).(n+1) by A4,A2,A6,RFINSEQ:17;
end;
theorem Th22:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds rng Rlor(F,A) = rng FinS(F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set fd = FinS(F,D), p = Rlor(F,B), mf = MIM(fd), b = Co_Gen B, h = CHI(b,C);
A3: len mf = len h by A1,A2,Th11;
dom F is finite;
then reconsider F9 = F as finite Function by FINSET_1:10;
A4: dom fd = Seg len fd by FINSEQ_1:def 3;
A5: dom p = C by A1,A2,Th20;
A6: dom b = Seg len b by FINSEQ_1:def 3;
reconsider dfd = dom fd, dF = dom F9 as finite set;
A7: len h = len b & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
A8: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then fd, F are_fiberwise_equipotent by A8,RFUNCT_3:def 13;
then card dfd = card dF by CLASSES1:81;
then len fd <> 0 by A8,A4;
then
A9: 0+1<=len fd by NAT_1:13;
then
A10: 1 in dom fd by FINSEQ_3:25;
thus rng p c= rng fd
proof
let x be object;
assume x in rng p;
then consider c be Element of C such that
c in dom p and
A11: p.c = x by PARTFUN1:3;
defpred P[set] means $1 in dom b & c in b.$1;
A12: ex n be Nat st P[n]
proof
take n = len b;
b.n = C by Th3;
hence thesis by A3,A7,A9,FINSEQ_3:25;
end;
consider mi be Nat such that
A13: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A12);
A14: 1<=mi by A13,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A15: mi<=len b by A13,FINSEQ_3:25;
now
per cases;
case
mi = 1;
then p.c = fd.1 by A1,A2,A13,Th21;
hence thesis by A10,A11,FUNCT_1:def 3;
end;
case
mi <> 1;
then 1<mi by A14,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A16: 1<=m1 by XREAL_1:19;
A17: m1<mi by XREAL_1:44;
then m1<=len b by A15,XXREAL_0:2;
then m1 in dom b by A16,FINSEQ_3:25;
then not c in b.m1 by A13,XREAL_1:44;
then
A18: c in b.(m1+1) \ b.m1 by A13,XBOOLE_0:def 5;
m1<len b by A15,A17,XXREAL_0:2;
then p.c = fd.(m1+1) by A1,A2,A16,A18,Th21;
hence thesis by A3,A7,A4,A6,A11,A13,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
let x be object;
defpred P[Nat] means $1 in dom fd & fd.$1 = x;
assume x in rng fd;
then
A19: ex n be Nat st P[n] by FINSEQ_2:10;
consider mi be Nat such that
A20: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A19);
A21: 1<=mi by A20,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A22: mi<=len fd by A20,FINSEQ_3:25;
now
per cases;
case
A23: mi=1;
set y = the Element of b.1;
A24: b.1 <> {} by A3,A7,A4,A6,A10,Th7;
b.1 c= C by A3,A7,A4,A6,A10,Lm5;
then reconsider y as Element of C by A24;
p.y = fd.1 by A1,A2,A24,Th21;
hence thesis by A5,A20,A23,FUNCT_1:def 3;
end;
case
A25: mi<>1;
set y = the Element of b.(m1+1) \ b.m1;
1<mi by A21,A25,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A26: 1<=m1 by XREAL_1:19;
m1+1<=len fd by A20,FINSEQ_3:25;
then m1<=len fd -1 by XREAL_1:19;
then
A27: b.(m1+1) \ b.m1 <> {} by A3,A7,A26,Th8;
then
A28: y in b.(m1+1) by XBOOLE_0:def 5;
b.mi c= C by A3,A7,A4,A6,A20,Lm5;
then reconsider y as Element of C by A28;
m1<mi by XREAL_1:44;
then m1<len fd by A22,XXREAL_0:2;
then p.y=fd.(m1+1) by A1,A2,A3,A7,A26,A27,Th21;
hence thesis by A5,A20,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
theorem Th23:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds Rlor(F,A), FinS(F,D) are_fiberwise_equipotent
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set fd = FinS(F,D), p = Rlor(F,B), mf = MIM(fd), b = Co_Gen B, h = CHI(b,C);
A1: len h = len b & len mf = len fd by RFINSEQ:def 2,RFUNCT_3:def 6;
assume
A2: F is total & card C = card D;
then
A3: rng p = rng fd by Th22;
A4: dom p = C by A2,Th20;
then reconsider p as finite PartFunc of C,REAL by FINSET_1:10;
A5: len mf = len h by A2,Th11;
A6: dom fd = Seg len fd & dom b = Seg len b by FINSEQ_1:def 3;
now
let x be object;
now
per cases;
case
A7: not x in rng fd;
then fd"{x}={} by Lm1;
hence card (fd"{x}) = card(p"{x}) by A3,A7,Lm1;
end;
case
A8: x in rng fd;
defpred P[Nat] means $1 in dom fd & fd.$1 = x;
A9: ex n be Nat st P[n] by A8,FINSEQ_2:10;
consider mi be Nat such that
A10: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A9
);
reconsider r=x as Real by A10;
A11: 1<=mi by A10,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi -1 as Element of NAT by FINSEQ_2:5;
A12: m1+1=mi;
A13: for n be Nat st P[n] holds n<=len fd by FINSEQ_3:25;
consider ma be Nat such that
A14: P[ma] & for n be Nat st P[n] holds n<=ma from NAT_1:sch 6(A13
,A9);
A15: ma<=len fd by A14,FINSEQ_3:25;
A16: Seg ma \ Seg m1 = fd"{x}
proof
thus Seg ma \ Seg m1 c= fd"{x}
proof
let y be object;
assume
A17: y in Seg ma \ Seg m1;
then reconsider l=y as Element of NAT;
reconsider o=fd.l as Real;
A18: y in Seg ma by A17,XBOOLE_0:def 5;
then
A19: 1<=l by FINSEQ_1:1;
A20: l<=ma by A18,FINSEQ_1:1;
then l<=len fd by A15,XXREAL_0:2;
then
A21: l in dom fd by A19,FINSEQ_3:25;
not y in Seg m1 by A17,XBOOLE_0:def 5;
then l<1 or m1<l by FINSEQ_1:1;
then mi<l+1 by A18,FINSEQ_1:1,XREAL_1:19;
then
A22: mi<=l by NAT_1:13;
now
per cases;
case
l=ma;
then o in {x} by A14,TARSKI:def 1;
hence thesis by A21,FUNCT_1:def 7;
end;
case
l<>ma;
then l<ma by A20,XXREAL_0:1;
then
A23: o>=r by A14,A21,RFINSEQ:19;
now
per cases;
case
l=mi;
then o in {x} by A10,TARSKI:def 1;
hence thesis by A21,FUNCT_1:def 7;
end;
case
l<>mi;
then mi<l by A22,XXREAL_0:1;
then r>=o by A10,A21,RFINSEQ:19;
then r=o by A23,XXREAL_0:1;
then o in {x} by TARSKI:def 1;
hence thesis by A21,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let y be object;
assume
A24: y in fd"{x};
then
A25: y in dom fd by FUNCT_1:def 7;
reconsider l=y as Element of NAT by A24;
A26: 1<=l by A25,FINSEQ_3:25;
fd.y in {x} by A24,FUNCT_1:def 7;
then
A27: fd.l=x by TARSKI:def 1;
then mi<=l by A10,A25;
then mi<l+1 by NAT_1:13;
then m1<l or l<1 by XREAL_1:19;
then
A28: not l in Seg m1 by FINSEQ_1:1;
l<=ma by A14,A25,A27;
then l in Seg ma by A26,FINSEQ_1:1;
hence thesis by A28,XBOOLE_0:def 5;
end;
A29: 1<=ma by A14,FINSEQ_3:25;
A30: mi<=ma by A10,A14;
m1<=mi by XREAL_1:43;
then
A31: m1<=ma by A30,XXREAL_0:2;
then Seg m1 c= Seg ma by FINSEQ_1:5;
then
A32: card(fd"{x}) = card(Seg ma) - card(Seg m1) by A16,CARD_2:44
.= ma - card(Seg m1) by FINSEQ_1:57
.= ma - m1 by FINSEQ_1:57;
A33: mi<=len fd by A10,FINSEQ_3:25;
then 1<=len fd by A11,XXREAL_0:2;
then
A34: 1 in dom fd by FINSEQ_3:25;
now
per cases;
case
A35: mi=1;
b.ma = p"{x}
proof
thus b.ma c= p"{x}
proof
defpred P[Nat] means $1 in dom b & $1<=ma implies
for c be Element of C st c in b.$1 holds c in p"{x};
let y be object;
assume
A36: y in b.ma;
b.ma c= C by A5,A1,A6,A14,Lm5;
then reconsider cy = y as Element of C by A36;
A37: for n st P[n] holds P[n+1]
proof
let n;
assume
A38: P[n];
assume that
A39: n+1 in dom b and
A40: n+1<=ma;
A41: n+1<=len b by A39,FINSEQ_3:25;
then
A42: n<=len b -1 by XREAL_1:19;
A43: n<len b by A41,NAT_1:13;
let c be Element of C;
assume
A44: c in b.(n+1);
A45: n<=len b by A41,NAT_1:13;
now
per cases;
case
n=0;
then p.c = x by A2,A10,A35,A44,Th21;
then p.c in {x} by TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
case
A46: n<>0;
then
A47: 0+1<n+1 by XREAL_1:6;
A48: 0+1<=n by A46,NAT_1:13;
then b.n c= b.(n+1) by A42,Def2;
then
A49: b.(n+1) = b.(n+1) \/ b.n by XBOOLE_1:12
.= (b.(n+1) \ b.n) \/ b.n by XBOOLE_1:39;
now
per cases by A44,A49,XBOOLE_0:def 3;
case
c in b.(n+1) \ b.n;
then
A50: p.c = fd.(n+1) by A2,A43,A48,Th21;
now
per cases;
case
n+1=ma;
then p.c in {x} by A14,A50,TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
case
n+1<>ma;
then n+1<ma by A40,XXREAL_0:1;
then
A51: p.c>=r by A5,A1,A6,A14,A39,A50,RFINSEQ:19;
r>=p.c by A5,A1,A6,A10,A35,A39,A47,A50,RFINSEQ:19
;
then r=p.c by A51,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in b.n;
hence thesis by A38,A40,A45,A48,FINSEQ_3:25,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A52: P[ 0 ] by FINSEQ_3:25;
A53: for n holds P[n] from NAT_1:sch 2(A52,A37);
ma in dom b by A5,A1,A14,FINSEQ_3:29;
then cy in p"{x} by A36,A53;
hence thesis;
end;
let y be object;
assume
A54: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A54,FUNCT_1:def 7;
then
A55: p.cy = x by TARSKI:def 1;
defpred Q[Nat] means $1 in dom b & ma<$1 & cy in b.$1;
assume
A56: not y in b.ma;
A57: ex n be Nat st Q[n]
proof
take n=len b;
len b <> 0 by Th4;
then 0+1<=len b by NAT_1:13;
hence n in dom b by FINSEQ_3:25;
A58: b.n= C by Th3;
now
assume n <= ma;
then ma=len b by A5,A1,A15,XXREAL_0:1;
then cy in b.ma by A58;
hence contradiction by A56;
end;
hence thesis by A58;
end;
consider mm be Nat such that
A59: Q[mm] & for n be Nat st Q[n] holds mm<=n from NAT_1:
sch 5(A57 );
1<=mm by A59,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A59,NAT_1:13;
then
A60: ma<=1m by XREAL_1:19;
then
A61: 1<=1m by A29,XXREAL_0:2;
A62: mm in dom fd by A5,A1,A59,FINSEQ_3:29;
A63: mm<=len b by A59,FINSEQ_3:25;
A64: mm<mm+1 by NAT_1:13;
then 1m<mm by XREAL_1:19;
then
A65: 1m<len b by A63,XXREAL_0:2;
1m<=mm by A64,XREAL_1:19;
then 1m<=len b by A63,XXREAL_0:2;
then
A66: 1m in dom b by A61,FINSEQ_3:25;
now
per cases;
case
ma=1m;
then cy in b.(1m+1) \ b.(1m) by A56,A59,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A61,A65,Th21;
hence contradiction by A14,A55,A59,A62;
end;
case
ma <> 1m;
then
A67: ma < 1m by A60,XXREAL_0:1;
now
assume cy in b.(1m);
then mm<=1m by A59,A66,A67;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in b.(1m+1) \ b.(1m) by A59,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A61,A65,Th21;
hence contradiction by A14,A55,A59,A62;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(fd"{x}) by A5,A1,A29,A15,A32,A35,Def1;
end;
case
A68: mi<>1;
then 1<mi by A11,XXREAL_0:1;
then
A69: 1<=m1 by A12,NAT_1:13;
A70: m1<=len fd by A33,A12,NAT_1:13;
then
A71: m1 in dom b by A5,A1,A69,FINSEQ_3:25;
then
A72: b.m1 c= b.ma by A5,A1,A6,A14,A31,Th2;
b.ma c= C by A5,A1,A6,A14,Lm5;
then reconsider bma = b.ma, bm1 = b.m1 as finite set by A72;
b.ma \ b.m1 = p"{x}
proof
thus b.ma \ b.m1 c= p"{x}
proof
defpred P[Nat] means $1 in dom b & mi<=$1 & $1<=ma
implies for c be Element of C st c in b.$1 \ b.m1 holds c in p"{x};
let y be object;
A73: b.ma c= C by A5,A1,A6,A14,Lm5;
A74: for n st P[n] holds P[n+1]
proof
let n;
assume
A75: P[n];
assume that
A76: n+1 in dom b and
A77: mi<=n+1 and
A78: n+1<=ma;
let c be Element of C;
n+1<=len b by A76,FINSEQ_3:25;
then
A79: n<len b by NAT_1:13;
assume
A80: c in b.(n+1) \ b.m1;
now
per cases;
case
A81: n+1=mi;
then p.c = fd.(n+1) by A2,A69,A79,A80,Th21;
then p.c in {x} by A10,A81,TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
case
mi <> n+1;
then
A82: mi<n+1 by A77,XXREAL_0:1;
then mi<=n by NAT_1:13;
then
A83: 1<=n by A11,XXREAL_0:2;
n<=ma by A78,NAT_1:13;
then
A84: n<=len b by A5,A1,A15,XXREAL_0:2;
then n<=n+1 & n in dom b by A83,FINSEQ_3:25,NAT_1:11;
then b.n c= b.(n+1) by A76,Th2;
then
A85: b.(n+1) \ b.m1 = (b.(n+1) \/ b .n) \ b.m1 by XBOOLE_1:12
.= ((b.(n+1) \b.n) \/ b.n) \ b.m1 by XBOOLE_1:39
.= (b.(n+1) \ b.n)\ b.m1 \/ (b.n \ b.m1) by XBOOLE_1:42
;
now
per cases by A80,A85,XBOOLE_0:def 3;
case
c in (b.(n+1) \ b.n) \ b.m1;
then c in b.(n+1) \ b.n by XBOOLE_0:def 5;
then
A86: p.c = fd.(n+1) by A2,A79,A83,Th21;
now
per cases;
case
n+1=ma;
then p.c in {x} by A14,A86,TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
case
n+1<>ma;
then n+1<ma by A78,XXREAL_0:1;
then
A87: p.c>=r by A5,A1,A6,A14,A76,A86,RFINSEQ:19;
r>=p.c by A5,A1,A6,A10,A76,A82,A86,RFINSEQ:19;
then r=p.c by A87,XXREAL_0:1;
then p.c in {x} by TARSKI:def 1;
hence thesis by A4,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
case
c in b.n \ b.m1;
hence thesis by A75,A78,A82,A83,A84,FINSEQ_3:25
,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A88: P[ 0 ];
A89: for n holds P[n] from NAT_1:sch 2(A88,A74);
assume
A90: y in b.ma \ b.m1;
then y in b.ma;
then reconsider cy = y as Element of C by A73;
ma in dom b by A5,A1,A14,FINSEQ_3:29;
then cy in p"{x} by A30,A90,A89;
hence thesis;
end;
let y be object;
assume
A91: y in p"{x};
then reconsider cy = y as Element of C;
p.cy in {x} by A91,FUNCT_1:def 7;
then
A92: p.cy = x by TARSKI:def 1;
assume
A93: not y in b.ma \ b.m1;
now
per cases by A93,XBOOLE_0:def 5;
case
A94: not y in b.ma;
defpred Q[Nat] means $1 in dom b & ma<$1 & cy in b.$1;
A95: ex n be Nat st Q[n]
proof
take n=len b;
len b <> 0 by Th4;
then 0+1<=len b by NAT_1:13;
hence n in dom b by FINSEQ_3:25;
A96: b.n= C by Th3;
now
assume n <= ma;
then ma=len b by A5,A1,A15,XXREAL_0:1;
then cy in b.ma by A96;
hence contradiction by A94;
end;
hence thesis by A96;
end;
consider mm be Nat such that
A97: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A95);
1<=mm by A97,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m = mm - 1 as Element of NAT by FINSEQ_2:5;
ma+1<=mm by A97,NAT_1:13;
then
A98: ma<=1m by XREAL_1:19;
then
A99: 1<=1m by A29,XXREAL_0:2;
A100: mm in dom fd by A5,A1,A97,FINSEQ_3:29;
A101: mm<=len b by A97,FINSEQ_3:25;
A102: mm<mm+1 by NAT_1:13;
then 1m<mm by XREAL_1:19;
then
A103: 1m<len b by A101,XXREAL_0:2;
1m<=mm by A102,XREAL_1:19;
then 1m<=len b by A101,XXREAL_0:2;
then
A104: 1m in dom b by A99,FINSEQ_3:25;
now
per cases;
case
ma=1m;
then cy in b.(1m+1) \ b.(1m) by A94,A97,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A99,A103,Th21;
hence contradiction by A14,A92,A97,A100;
end;
case
ma <> 1m;
then
A105: ma < 1m by A98,XXREAL_0:1;
now
assume cy in b.(1m);
then mm<=1m by A97,A104,A105;
then mm - 1m <=0 by XREAL_1:47;
hence contradiction;
end;
then cy in b.(1m+1) \ b.(1m) by A97,XBOOLE_0:def 5;
then p.cy = fd.mm by A2,A99,A103,Th21;
hence contradiction by A14,A92,A97,A100;
end;
end;
hence contradiction;
end;
case
A106: y in b.m1;
defpred Q[Nat] means $1 in dom b & $1<=m1 & cy in b.$1;
A107: ex n be Nat st Q[n] by A71,A106;
consider mm be Nat such that
A108: Q [mm] & for n be Nat st Q[n] holds mm<=n from
NAT_1:sch 5(A107);
A109: 1<=mm by A108,FINSEQ_3:25;
then max(0,mm-1)=mm-1 by FINSEQ_2:4;
then reconsider 1m=mm-1 as Element of NAT by FINSEQ_2:5;
A110: mm<=len b by A108,FINSEQ_3:25;
A111: mm in dom fd by A5,A1,A108,FINSEQ_3:29;
now
per cases;
case
mm=1;
then p.cy = fd.1 by A2,A108,Th21;
then mi<=1 by A10,A34,A92;
hence contradiction by A11,A68,XXREAL_0:1;
end;
case
mm<>1;
then 1<mm by A109,XXREAL_0:1;
then 1+1<=mm by NAT_1:13;
then
A112: 1<=1m by XREAL_1:19;
A113: mm<mm+1 by NAT_1:13;
then
A114: 1m<=mm by XREAL_1:19;
then 1m<=len b by A110,XXREAL_0:2;
then
A115: 1m in dom b by A112,FINSEQ_3:25;
A116: 1m<mm by A113,XREAL_1:19;
then
A117: 1m<len b by A110,XXREAL_0:2;
1m<=m1 by A108,A114,XXREAL_0:2;
then not cy in b.1m by A108,A116,A115;
then cy in b.(1m+1) \ b.1m by A108,XBOOLE_0:def 5;
then p.cy = fd.(1m+1) by A2,A112,A117,Th21;
then mi<=mm by A10,A92,A111;
then m1+1<=m1 by A108,XXREAL_0:2;
then 1<=m1-m1 by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
hence card(p"{x}) = card(bma) - card(bm1) by A72,CARD_2:44
.= ma - card(bm1) by A5,A1,A29,A15,Def1
.= card (fd"{x}) by A5,A1,A32,A69,A70,Def1;
end;
end;
hence card (fd"{x}) = card(p"{x});
end;
end;
hence card Coim(fd,x) = card Coim(p,x);
end;
hence thesis by CLASSES1:def 10;
end;
theorem Th24:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds FinS(Rlor(F,A),C) = FinS(F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume
A1: F is total & card C = card D;
then
A2: Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by Th23;
A3: dom Rlor(F,B) = C by A1,Th20;
then (Rlor(F,B))|C = Rlor(F,B) by RELAT_1:68;
hence thesis by A2,A3,RFUNCT_3:def 13;
end;
theorem Th25:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card C = card D holds Sum (Rlor(F,A),C) = Sum (F,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume F is total & card C = card D;
then FinS(Rlor(F,B),C) = FinS(F,D) by Th24;
hence Sum(Rlor(F,B),C) = Sum FinS(F,D) by RFUNCT_3:def 14
.= Sum (F,D) by RFUNCT_3:def 14;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds FinS((Rlor(F,A)) - r,C) = FinS(F-r,D) & Sum (Rlor(F,A)-r,
C) = Sum (F-r,D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then Rlor(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then
A5: Rlor(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
A6: dom (Rlor(F,B) - r) = dom Rlor (F,B) by VALUED_1:3;
then (Rlor(F,B) - r)|C = Rlor(F,B) -r by RELAT_1:68;
then FinS(Rlor(F,B) - r, C), Rlor(F,B) -r are_fiberwise_equipotent
by A6,RFUNCT_3:def 13; then
A7: FinS(Rlor(F,B) - r, C), F-r are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom(F-r) = dom F by VALUED_1:3;
then (F-r)|D = F-r by RELAT_1:68;
hence FinS(Rlor(F,B) - r,C) = FinS(F-r,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(Rlor(F,B)-r,C) = Sum FinS(F-r,D) by RFUNCT_3:def 14
.= Sum (F-r,D) by RFUNCT_3:def 14;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds Rlor(F,A), Rland(F,A) are_fiberwise_equipotent & FinS(
Rlor(F,A),C) = FinS(Rland(F,A),C) & Sum (Rlor(F,A),C) = Sum (Rland(F,A),C)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume
A1: F is total & card C = card D;
then
A2: Sum (Rland(F,B),C) = Sum (F,D) & Rlor(F,B), FinS(F,D)
are_fiberwise_equipotent by Th18,Th23;
Rland(F,B), FinS(F,D) are_fiberwise_equipotent & FinS(Rland (F,B),C) =
FinS( F,D) by A1,Th16,Th17;
hence thesis by A1,A2,Th24,Th25,CLASSES1:76;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds max+(Rland(F,A) - r), max+(F - r)
are_fiberwise_equipotent & FinS(max+(Rland(F,A) - r), C) = FinS(max+(F - r), D)
& Sum (max+(Rland(F,A) - r), C) = Sum (max+(F - r), D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max+(Rland(F,B)-r), mf = max+(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rland(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th16;
then Rland(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rland(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:41;
A6: dom mp = dom (Rland(F,B)-r) by RFUNCT_3:def 10;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 10;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds max-(Rland(F,A) - r), max-(F - r)
are_fiberwise_equipotent & FinS(max-(Rland(F,A) - r), C) = FinS(max-(F - r), D)
& Sum (max-(Rland(F,A) - r), C) = Sum (max-(F - r), D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max-(Rland(F,B)-r), mf = max-(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rland(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th16;
then Rland(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rland(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:42;
A6: dom mp = dom (Rland(F,B)-r) by RFUNCT_3:def 11;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 11;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem Th30:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card D = card C holds len FinS(Rland(F,A),C) = card C & 1<=len FinS(
Rland(F,A),C)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set p = Rland(F,B);
assume F is total & card D = card C;
then
A1: dom p = C by Th12;
then
A2: p|C = p by RELAT_1:68;
hence len FinS(p,C) = card C by A1,RFUNCT_3:67;
0+1<=card C by NAT_1:13;
hence thesis by A1,A2,RFUNCT_3:67;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card D = card C & n in dom A holds FinS(Rland(F,A),C) | n = FinS(Rland(F,A),A.n
)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total & card D = card C and
A2: n in dom B;
set p = Rland(F,B);
A3: len FinS(p,C) = card C by A1,Th30;
defpred P[Nat] means $1 in dom B implies FinS(Rland(F,B),C) | $1
= FinS(Rland(F,B),B.$1);
A4: len B = card C by Th1;
A5: dom B = Seg len B & dom FinS(p,C) = Seg len FinS(p,C) by FINSEQ_1:def 3;
A6: for m st P[m] holds P[m+1]
proof
set f = FinS(p,C);
let m;
assume
A7: P[m];
A8: m<=m+1 by NAT_1:11;
assume
A9: m+1 in dom B;
then 1<=m+1 by FINSEQ_3:25;
then
A10: m+1 in Seg(m+1) by FINSEQ_1:1;
A11: dom p = C by A1,Th12;
A12: m+1<=len B by A9,FINSEQ_3:25;
then
A13: m<=len B by NAT_1:13;
A14: m<len B by A12,NAT_1:13;
A15: m<=len B - 1 by A12,XREAL_1:19;
A16: len (f|(m+1)) = m+1 by A4,A3,A12,FINSEQ_1:59;
now
per cases;
case
A17: m=0;
consider d be Element of C such that
A18: B.1 = {d} by Th9;
A19: d in B.1 by A18,TARSKI:def 1;
A20: 1<=len FinS(p,C) by A1,Th30;
then 1 in Seg 1 & 1 in dom FinS(p,C) by FINSEQ_1:1,FINSEQ_3:25;
then
A21: (FinS(p,C)|(m+1)).1 = FinS(p,C).1 by A17,RFINSEQ:6
.= FinS(F,D).1 by A1,Th17
.= p.d by A1,A19,Th14;
dom p = C by A1,Th12;
then
A22: FinS(p, B.(m+1)) = <* p.d *> by A17,A18,RFUNCT_3:69;
len(FinS(p,C)|(m+1)) = 1 by A17,A20,FINSEQ_1:59;
hence thesis by A22,A21,FINSEQ_1:40;
end;
case
A23: m<>0;
A24: Seg m c= Seg(m+1) by A8,FINSEQ_1:5;
A25: (f|(m+1))|m = (f|(m+1))|(Seg m) by FINSEQ_1:def 16
.= (f|Seg(m+1))|(Seg m) by FINSEQ_1:def 16
.= f|(Seg(m+1) /\ (Seg m)) by RELAT_1:71
.= f|(Seg m) by A24,XBOOLE_1:28
.= f|m by FINSEQ_1:def 16;
A26: 0+1<=m by A23,NAT_1:13;
then consider d be Element of C such that
A27: B.(m+1) \ B.m = {d} and
B.(m+1) = B.m \/ {d} and
A28: B.(m+1) \ {d} = B.m by A15,Th10;
A29: d in {d} by TARSKI:def 1;
then p.d = FinS(F,D).(m+1) by A1,A14,A26,A27,Th14
.= FinS(p,C).(m+1) by A1,Th17
.=(f|(m+1)).(m+1) by A5,A4,A3,A9,A10,RFINSEQ:6;
then
A30: f|(m+1) = f|m ^ <*p.d*> by A16,A25,RFINSEQ:7;
d in dom p /\ B.(m+1) by A11,A27,A29,XBOOLE_0:def 4;
then
A31: d in dom(p|(B.(m+1))) by RELAT_1:61;
A32: (f|(m+1)) is non-increasing by RFINSEQ:20;
A33: dom(p|(B.(m+1))) = dom p /\ (B.(m+1)) by RELAT_1:61
.= B.(m+1) by A9,A11,Lm5,XBOOLE_1:28;
B.(m+1) is finite by A9,Lm5,FINSET_1:1;
then
f|(m+1), p|(B.(m+1)) are_fiberwise_equipotent
by A7,A13,A26,A28,A30,A31,FINSEQ_3:25,RFUNCT_3:65;
hence thesis by A33,A32,RFUNCT_3:def 13;
end;
end;
hence thesis;
end;
A34: P[ 0 ] by FINSEQ_3:25;
for m holds P[m] from NAT_1:sch 2(A34,A6);
hence thesis by A2;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card D = card C holds Rland(F-r,A) = Rland(F,A) - r
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom Rland(F,B) = C by A1,A2,Th12;
A4: dom F = D by A1,PARTFUN1:def 2;
then
A5: dom(F-r) = D by VALUED_1:3;
then
A6: F-r is total by PARTFUN1:def 2;
(F-r)|D = F-r by A5,RELAT_1:68;
then
A7: len FinS(F-r,D) = card D by A5,RFUNCT_3:67;
A8: len B = card C by Th1;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
F|D = F by A4,RELAT_1:68;
then
A9: FinS(F-r,D) = FinS(F,D) - (card D |-> rr) by A4,RFUNCT_3:73;
A10: now
let c be Element of C;
assume c in dom Rland(F-r,B);
defpred P[set] means $1 in dom B & c in B.$1;
A11: C = B.(len B) by Th3;
len B <> 0 by Th4;
then
A12: 0+1<=len B by NAT_1:13;
then
A13: 1 in dom B by FINSEQ_3:25;
len B in dom B by A12,FINSEQ_3:25;
then
A14: ex n be Nat st P[n] by A11;
consider mi be Nat such that
A15: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A14);
A16: 1<=mi by A15,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi - 1 as Element of NAT by FINSEQ_2:5;
A17: mi<=len B by A15,FINSEQ_3:25;
A18: mi<mi+1 by NAT_1:13;
then m1<mi by XREAL_1:19;
then
A19: m1<len B by A17,XXREAL_0:2;
m1<=mi by A18,XREAL_1:19;
then
A20: m1<=len B by A17,XXREAL_0:2;
now
per cases;
case
A21: mi=1;
A22: 1 in dom FinS(F-r,D) by A2,A7,A8,A12,FINSEQ_3:25;
1 in Seg card D by A2,A8,A13,FINSEQ_1:def 3;
then
A23: (card D |-> r).1 = r by FUNCOP_1:7;
(Rland(F-r,B)).c = FinS(F-r,D).1 & (Rland(F,B)).c = FinS(F,D).1
by A1,A2,A6,A15,A21,Th14;
hence (Rland(F-r,B)).c = (Rland(F,B)).c - r by A9,A22,A23,VALUED_1:13
.= (Rland(F,B) - r).c by A3,VALUED_1:3;
end;
case
mi <> 1;
then 1<mi by A16,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A24: 1<=m1 by XREAL_1:19;
then m1 in dom B by A20,FINSEQ_3:25;
then not c in B.m1 by A15,XREAL_1:44;
then c in B.(m1+1) \ B.m1 by A15,XBOOLE_0:def 5;
then
A25: (Rland(F-r,B)).c = FinS(F-r,D).(m1+1) & (Rland (F,B)).c = FinS(F,
D).(m1+1) by A1,A2,A6,A19,A24,Th14;
m1+1 in Seg card D by A2,A8,A15,FINSEQ_1:def 3;
then
A26: (card D |-> r).(m1+1) = r by FUNCOP_1:7;
m1+1 in dom FinS(F-r,D) by A2,A7,A8,A15,FINSEQ_3:29;
hence (Rland(F-r,B)).c = (Rland(F,B)).c - r by A9,A25,A26,VALUED_1:13
.= (Rland(F,B) - r).c by A3,VALUED_1:3;
end;
end;
hence (Rland(F-r,B)).c = (Rland(F,B) - r).c;
end;
dom(Rland(F,B) - r) = C by A3,VALUED_1:3;
hence thesis by A2,A6,A10,Th12,PARTFUN1:5;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds max+(Rlor(F,A) - r), max+(F - r) are_fiberwise_equipotent
& FinS(max+(Rlor(F,A) - r), C) = FinS(max+(F - r), D) & Sum (max+(Rlor(F,A) - r
), C) = Sum (max+(F - r), D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max+(Rlor(F,B)-r), mf = max+(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then Rlor(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rlor(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:41;
A6: dom mp = dom (Rlor(F,B)-r) by RFUNCT_3:def 10;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 10;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card C = card D holds max-(Rlor(F,A) - r), max-(F - r) are_fiberwise_equipotent
& FinS(max-(Rlor(F,A) - r), C) = FinS(max-(F - r), D) & Sum (max-(Rlor(F,A) - r
), C) = Sum (max-(F - r), D)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card C = card D;
set mp = max-(Rlor(F,B)-r), mf = max-(F-r);
A3: dom F = D by A1,PARTFUN1:def 2;
then F|D = F by RELAT_1:68;
then
A4: FinS(F,D), F are_fiberwise_equipotent by A3,RFUNCT_3:def 13;
Rlor(F,B), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then Rlor(F,B), F are_fiberwise_equipotent by A4,CLASSES1:76;
then Rlor(F,B)-r, F-r are_fiberwise_equipotent by RFUNCT_3:51;
hence
A5: mp, mf are_fiberwise_equipotent by RFUNCT_3:42;
A6: dom mp = dom (Rlor(F,B)-r) by RFUNCT_3:def 11;
then mp|C = mp by RELAT_1:68;
then FinS(mp, C), mp are_fiberwise_equipotent by A6,RFUNCT_3:def 13;
then
A7: FinS(mp, C), mf are_fiberwise_equipotent by A5,CLASSES1:76;
A8: dom mf=dom(F-r) by RFUNCT_3:def 11;
then mf|D = mf by RELAT_1:68;
hence FinS(mp,C) = FinS(mf,D) by A8,A7,RFUNCT_3:def 13;
hence Sum(mp,C) = Sum FinS(mf,D) by RFUNCT_3:def 14
.= Sum (mf,D) by RFUNCT_3:def 14;
end;
theorem Th35:
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is
total & card D = card C holds len FinS(Rlor(F,A),C) = card C & 1<=len FinS(Rlor
(F,A),C)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
set p = Rlor(F,B);
assume F is total & card D = card C;
then
A1: dom p = C by Th20;
then
A2: p|C = p by RELAT_1:68;
hence len FinS(p,C) = card C by A1,RFUNCT_3:67;
0+1<=card C by NAT_1:13;
hence thesis by A1,A2,RFUNCT_3:67;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card D = card C & n in dom A holds FinS(Rlor(F,A),C) | n = FinS(Rlor(F,A),(
Co_Gen A).n)
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total & card D = card C and
A2: n in dom B;
set p = Rlor(F,B), b = Co_Gen B;
A3: len FinS(p,C) = card C by A1,Th35;
defpred P[Nat] means $1 in dom b implies FinS(Rlor(F,B),C) | $1 =
FinS(Rlor(F,B),b.$1);
A4: dom b = Seg len b by FINSEQ_1:def 3;
A5: len b = card C by Th1;
A6: dom FinS(p,C) = Seg len FinS(p,C) by FINSEQ_1:def 3;
A7: for m st P[m] holds P[m+1]
proof
set f = FinS(p,C);
let m;
assume
A8: P[m];
A9: m<=m+1 by NAT_1:11;
assume
A10: m+1 in dom b;
then 1<=m+1 by FINSEQ_3:25;
then
A11: m+1 in Seg(m+1) by FINSEQ_1:1;
A12: dom p = C by A1,Th20;
A13: m+1<=len b by A10,FINSEQ_3:25;
then
A14: m<=len b by NAT_1:13;
A15: m<len b by A13,NAT_1:13;
A16: m<=len b - 1 by A13,XREAL_1:19;
A17: len (f|(m+1)) = m+1 by A5,A3,A13,FINSEQ_1:59;
now
per cases;
case
A18: m=0;
consider d be Element of C such that
A19: b.1 = {d} by Th9;
A20: d in b.1 by A19,TARSKI:def 1;
A21: 1<=len FinS(p,C) by A1,Th35;
then 1 in Seg 1 & 1 in dom FinS(p,C) by FINSEQ_1:1,FINSEQ_3:25;
then
A22: (FinS(p,C)|(m+1)).1 = FinS(p,C).1 by A18,RFINSEQ:6
.= FinS(F,D).1 by A1,Th24
.= p.d by A1,A20,Th21;
dom p = C by A1,Th20;
then
A23: FinS(p, b.(m+1)) = <* p.d *> by A18,A19,RFUNCT_3:69;
len(FinS(p,C)|(m+1)) = 1 by A18,A21,FINSEQ_1:59;
hence thesis by A23,A22,FINSEQ_1:40;
end;
case
A24: m<>0;
A25: Seg m c= Seg(m+1) by A9,FINSEQ_1:5;
A26: (f|(m+1))|m = (f|(m+1))|(Seg m) by FINSEQ_1:def 16
.= (f|Seg(m+1))|(Seg m) by FINSEQ_1:def 16
.= f|(Seg(m+1) /\ (Seg m)) by RELAT_1:71
.= f|(Seg m) by A25,XBOOLE_1:28
.= f|m by FINSEQ_1:def 16;
A27: 0+1<=m by A24,NAT_1:13;
then consider d be Element of C such that
A28: b.(m+1) \ b.m = {d} and
b.(m+1) = b.m \/ {d} and
A29: b.(m+1) \ {d} = b.m by A16,Th10;
A30: d in {d} by TARSKI:def 1;
then p.d = FinS(F,D).(m+1) by A1,A15,A27,A28,Th21
.= FinS(p,C).(m+1) by A1,Th24
.=(f|(m+1)).(m+1) by A4,A6,A5,A3,A10,A11,RFINSEQ:6;
then
A31: f|(m+1) = f|m ^ <*p.d*> by A17,A26,RFINSEQ:7;
d in dom p /\ b.(m+1) by A12,A28,A30,XBOOLE_0:def 4;
then
A32: d in dom(p|(b.(m+1))) by RELAT_1:61;
A33: (f|(m+1)) is non-increasing by RFINSEQ:20;
A34: dom(p|(b.(m+1))) = dom p /\ (b.(m+1)) by RELAT_1:61
.= b.(m+1) by A10,A12,Lm5,XBOOLE_1:28;
b.(m+1) is finite by A10,Lm5,FINSET_1:1;
then
f|(m+1), p|(b.(m+1)) are_fiberwise_equipotent by A8,A14,A27,A29,A31,A32
,FINSEQ_3:25,RFUNCT_3:65;
hence thesis by A34,A33,RFUNCT_3:def 13;
end;
end;
hence thesis;
end;
A35: dom B = Seg len B & len B = card C by Th1,FINSEQ_1:def 3;
A36: P[ 0 ] by FINSEQ_3:25;
for m holds P[m] from NAT_1:sch 2(A36,A7);
hence thesis by A2,A4,A35,A5;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card D = card C holds Rlor(F-r,A) = Rlor(F,A) - r
proof
let F be PartFunc of D,REAL, B be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom Rlor(F,B) = C by A1,A2,Th20;
set b = Co_Gen B;
A4: len b = card C by Th1;
A5: dom F = D by A1,PARTFUN1:def 2;
then
A6: dom(F-r) = D by VALUED_1:3;
then
A7: F-r is total by PARTFUN1:def 2;
(F-r)|D = F-r by A6,RELAT_1:68;
then
A8: len FinS(F-r,D) = card D by A6,RFUNCT_3:67;
reconsider rr=r as Element of REAL by XREAL_0:def 1;
F|D = F by A5,RELAT_1:68;
then
A9: FinS(F-r,D) = FinS(F,D) - (card D |-> rr) by A5,RFUNCT_3:73;
A10: now
let c be Element of C;
assume c in dom Rlor(F-r,B);
defpred P[set] means $1 in dom b & c in b.$1;
A11: C = b.(len b) by Th3;
len b <> 0 by Th4;
then
A12: 0+1<=len b by NAT_1:13;
then
A13: 1 in dom b by FINSEQ_3:25;
len b in dom b by A12,FINSEQ_3:25;
then
A14: ex n be Nat st P[n] by A11;
consider mi be Nat such that
A15: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A14);
A16: 1<=mi by A15,FINSEQ_3:25;
then max(0,mi-1)=mi-1 by FINSEQ_2:4;
then reconsider m1 = mi - 1 as Element of NAT by FINSEQ_2:5;
A17: mi<=len b by A15,FINSEQ_3:25;
A18: mi<mi+1 by NAT_1:13;
then m1<mi by XREAL_1:19;
then
A19: m1<len b by A17,XXREAL_0:2;
m1<=mi by A18,XREAL_1:19;
then
A20: m1<=len b by A17,XXREAL_0:2;
now
per cases;
case
A21: mi=1;
A22: 1 in dom FinS(F-r,D) by A2,A8,A4,A12,FINSEQ_3:25;
1 in Seg card D by A2,A4,A13,FINSEQ_1:def 3;
then
A23: (card D |-> r).1 = r by FUNCOP_1:7;
(Rlor(F-r,B)).c = FinS(F-r,D).1 & (Rlor(F,B)).c = FinS(F,D ).1 by A1,A2
,A7,A15,A21,Th21;
hence (Rlor(F-r,B)).c = (Rlor(F,B)).c - r by A9,A22,A23,VALUED_1:13
.= (Rlor(F,B) - r).c by A3,VALUED_1:3;
end;
case
mi <> 1;
then 1<mi by A16,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A24: 1<=m1 by XREAL_1:19;
then m1 in dom b by A20,FINSEQ_3:25;
then not c in b.m1 by A15,XREAL_1:44;
then c in b.(m1+1) \ b.m1 by A15,XBOOLE_0:def 5;
then
A25: (Rlor(F-r,B)).c = FinS(F-r,D).(m1+1) & (Rlor (F,B)).c = FinS(F,D)
.(m1+1) by A1,A2,A7,A19,A24,Th21;
m1+1 in Seg card D by A2,A4,A15,FINSEQ_1:def 3;
then
A26: (card D |-> r).(m1+1) = r by FUNCOP_1:7;
m1+1 in dom FinS(F-r,D) by A2,A8,A4,A15,FINSEQ_3:29;
hence (Rlor(F-r,B)).c = (Rlor(F,B)).c - r by A9,A25,A26,VALUED_1:13
.= (Rlor(F,B) - r).c by A3,VALUED_1:3;
end;
end;
hence (Rlor(F-r,B)).c = (Rlor(F,B) - r).c;
end;
dom(Rlor(F,B) - r) = C by A3,VALUED_1:3;
hence thesis by A2,A7,A10,Th20,PARTFUN1:5;
end;
theorem
for F be PartFunc of D,REAL, A be RearrangmentGen of C st F is total &
card D = card C holds Rland(F,A) , F are_fiberwise_equipotent & Rlor (F,A) , F
are_fiberwise_equipotent & rng Rland(F,A) = rng F & rng Rlor(F,A) = rng F
proof
let F be PartFunc of D,REAL, A be RearrangmentGen of C;
assume that
A1: F is total and
A2: card D = card C;
A3: dom F = D by A1,PARTFUN1:def 2;
dom(F|D) = dom F /\ D by RELAT_1:61
.= D by A3;
then
A4: FinS(F,D), F|D are_fiberwise_equipotent by RFUNCT_3:def 13;
Rlor(F,A), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th23;
then
A5: Rlor (F,A), F|D are_fiberwise_equipotent by A4,CLASSES1:76;
Rland(F,A), FinS(F,D) are_fiberwise_equipotent by A1,A2,Th16;
then Rland(F,A), F|D are_fiberwise_equipotent by A4,CLASSES1:76;
hence Rland(F,A), F are_fiberwise_equipotent & Rlor(F,A), F
are_fiberwise_equipotent by A3,A5,RELAT_1:68;
hence thesis by CLASSES1:75;
end;