:: REARRAN1 semantic presentation
begin
definition
let D be non empty set ;
let E be real-membered set ;
let F be PartFunc of D,E;
let r be Real;
:: original: (#)
redefine funcr (#) F -> Element of PFuncs (D,REAL);
coherence
r (#) F is Element of PFuncs (D,REAL)
proof
reconsider F = F as PartFunc of D,E ;
r (#) F is PartFunc of D,REAL ;
hence r (#) F is Element of PFuncs (D,REAL) by PARTFUN1:45; ::_thesis: verum
end;
end;
Lm1: for f being Function
for x being set st not x in rng f holds
f " {x} = {}
proof
let f be Function; ::_thesis: for x being set st not x in rng f holds
f " {x} = {}
let x be set ; ::_thesis: ( not x in rng f implies f " {x} = {} )
assume A1: not x in rng f ; ::_thesis: f " {x} = {}
rng f misses {x}
proof
set y = the Element of (rng f) /\ {x};
assume (rng f) /\ {x} <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then ( the Element of (rng f) /\ {x} in rng f & the Element of (rng f) /\ {x} in {x} ) by XBOOLE_0:def_4;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
hence f " {x} = {} by RELAT_1:138; ::_thesis: verum
end;
definition
let IT be FinSequence;
attrIT is terms've_same_card_as_number means :Def1: :: REARRAN1:def 1
for n being Nat st 1 <= n & n <= len IT holds
for B being finite set st B = IT . n holds
card B = n;
attrIT is ascending means :Def2: :: REARRAN1:def 2
for n being Nat st 1 <= n & n <= (len IT) - 1 holds
IT . n c= IT . (n + 1);
end;
:: deftheorem Def1 defines terms've_same_card_as_number REARRAN1:def_1_:_
for IT being FinSequence holds
( IT is terms've_same_card_as_number iff for n being Nat st 1 <= n & n <= len IT holds
for B being finite set st B = IT . n holds
card B = n );
:: deftheorem Def2 defines ascending REARRAN1:def_2_:_
for IT being FinSequence holds
( IT is ascending iff for n being Nat st 1 <= n & n <= (len IT) - 1 holds
IT . n c= IT . (n + 1) );
Lm2: for D being non empty finite set
for A being FinSequence of bool D
for k being Element of NAT st 1 <= k & k <= len A holds
A . k is finite
proof
let D be non empty finite set ; ::_thesis: for A being FinSequence of bool D
for k being Element of NAT st 1 <= k & k <= len A holds
A . k is finite
let A be FinSequence of bool D; ::_thesis: for k being Element of NAT st 1 <= k & k <= len A holds
A . k is finite
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len A implies A . k is finite )
assume ( 1 <= k & k <= len A ) ; ::_thesis: A . k is finite
then k in dom A by FINSEQ_3:25;
then A . k in bool D by FINSEQ_2:11;
hence A . k is finite ; ::_thesis: verum
end;
Lm3: for D being non empty finite set
for A being FinSequence of bool D st len A = card D & A is terms've_same_card_as_number holds
for B being finite set st B = A . (len A) holds
B = D
proof
let D be non empty finite set ; ::_thesis: for A being FinSequence of bool D st len A = card D & A is terms've_same_card_as_number holds
for B being finite set st B = A . (len A) holds
B = D
let A be FinSequence of bool D; ::_thesis: ( len A = card D & A is terms've_same_card_as_number implies for B being finite set st B = A . (len A) holds
B = D )
assume that
A1: len A = card D and
A2: A is terms've_same_card_as_number ; ::_thesis: for B being finite set st B = A . (len A) holds
B = D
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 ; ::_thesis: ( B = A . (len A) implies B = D )
assume A5: B = A . (len A) ; ::_thesis: B = D
assume B <> D ; ::_thesis: contradiction
then A6: B c< D by A5, A4, XBOOLE_0:def_8;
card B = card D by A1, A2, A5, A3, Def1;
hence contradiction by A6, CARD_2:48; ::_thesis: verum
end;
Lm4: for D being non empty finite set ex B being 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 ; ::_thesis: ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number )
defpred S1[ Element of NAT ] means for D being non empty finite set st card D = $1 holds
ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number );
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; ::_thesis: S1[n + 1]
let D be non empty finite set ; ::_thesis: ( card D = n + 1 implies ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) )
assume A3: card D = n + 1 ; ::_thesis: ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number )
set x = the Element of D;
set Y = D \ { the Element of D};
{ the Element of D} c= D by ZFMISC_1:31;
then A4: card (D \ { the Element of D}) = (card D) - (card { the Element of D}) by CARD_2:44
.= (n + 1) - 1 by A3, CARD_1:30
.= n ;
now__::_thesis:_(_(_n_=_0_&_ex_f_being_FinSequence_of_bool_D_st_
(_card_D_=_len_f_&_f_is_ascending_&_f_is_terms've_same_card_as_number_)_)_or_(_n_<>_0_&_ex_g_being_FinSequence_of_bool_D_st_
(_len_g_=_card_D_&_g_is_ascending_&_g_is_terms've_same_card_as_number_)_)_)
percases ( n = 0 or n <> 0 ) ;
caseA5: n = 0 ; ::_thesis: ex f being FinSequence of bool D st
( card D = len f & f is ascending & f is terms've_same_card_as_number )
set f = <*D*>;
A6: len <*D*> = 1 by FINSEQ_1:39;
A7: rng <*D*> = {D} by FINSEQ_1:39;
rng <*D*> c= bool D
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng <*D*> or z in bool D )
assume z in rng <*D*> ; ::_thesis: z in bool D
then z = D by A7, TARSKI:def_1;
hence z in bool D by ZFMISC_1:def_1; ::_thesis: verum
end;
then reconsider f = <*D*> as FinSequence of bool D by FINSEQ_1:def_4;
take f = f; ::_thesis: ( card D = len f & f is ascending & f is terms've_same_card_as_number )
thus card D = len f by A3, A5, FINSEQ_1:40; ::_thesis: ( f is ascending & f is terms've_same_card_as_number )
thus f is ascending ::_thesis: f is terms've_same_card_as_number
proof
let m be Nat; :: according to REARRAN1:def_2 ::_thesis: ( 1 <= m & m <= (len f) - 1 implies f . m c= f . (m + 1) )
assume ( 1 <= m & m <= (len f) - 1 ) ; ::_thesis: f . m c= f . (m + 1)
hence f . m c= f . (m + 1) by A6, XXREAL_0:2; ::_thesis: verum
end;
thus f is terms've_same_card_as_number ::_thesis: verum
proof
let m be Nat; :: according to REARRAN1:def_1 ::_thesis: ( 1 <= m & m <= len f implies for B being finite set st B = f . m holds
card B = m )
assume ( 1 <= m & m <= len f ) ; ::_thesis: for B being finite set st B = f . m holds
card B = m
then A8: m = 1 by A6, XXREAL_0:1;
let B be finite set ; ::_thesis: ( B = f . m implies card B = m )
assume B = f . m ; ::_thesis: card B = m
hence card B = m by A3, A5, A8, FINSEQ_1:40; ::_thesis: verum
end;
end;
case n <> 0 ; ::_thesis: ex g being FinSequence of bool D st
( len g = card D & g is ascending & g is terms've_same_card_as_number )
then reconsider Y = D \ { the Element of D} 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 being 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 (f ^ <*D*>) = (rng f) \/ (rng <*D*>) ) by FINSEQ_1:31, FINSEQ_1:39;
bool Y c= bool D by ZFMISC_1:67;
then rng f c= bool D by XBOOLE_1:1;
then rng (f ^ <*D*>) c= (bool D) \/ (bool D) by A9, A13, XBOOLE_1:13;
then reconsider g = f ^ <*D*> as FinSequence of bool D by FINSEQ_1:def_4;
take g = g; ::_thesis: ( len g = card D & g is ascending & g is terms've_same_card_as_number )
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; ::_thesis: ( g is ascending & g is terms've_same_card_as_number )
thus g is ascending ::_thesis: g is terms've_same_card_as_number
proof
let m be Nat; :: according to REARRAN1:def_2 ::_thesis: ( 1 <= m & m <= (len g) - 1 implies g . m c= g . (m + 1) )
assume that
A16: 1 <= m and
A17: m <= (len g) - 1 ; ::_thesis: g . m c= g . (m + 1)
m in dom f by A15, A16, A17, FINSEQ_3:25;
then A18: g . m = f . m by FINSEQ_1:def_7;
percases ( m = len f or m <> len f ) ;
supposeA19: m = len f ; ::_thesis: g . m c= g . (m + 1)
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 g . m c= g . (m + 1) ; ::_thesis: verum
end;
suppose m <> len f ; ::_thesis: g . m c= g . (m + 1)
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 g . m c= g . (m + 1) by A11, A16, A18, A21, Def2; ::_thesis: verum
end;
end;
end;
thus g is terms've_same_card_as_number ::_thesis: verum
proof
let m be Nat; :: according to REARRAN1:def_1 ::_thesis: ( 1 <= m & m <= len g implies for B being finite set st B = g . m holds
card B = m )
assume that
A22: 1 <= m and
A23: m <= len g ; ::_thesis: for B being finite set st B = g . m holds
card B = m
let B be finite set ; ::_thesis: ( B = g . m implies card B = m )
assume A24: B = g . m ; ::_thesis: card B = m
percases ( m = len g or m <> len g ) ;
suppose m = len g ; ::_thesis: card B = m
hence card B = m by A3, A4, A10, A15, A24, FINSEQ_1:42; ::_thesis: verum
end;
suppose m <> len g ; ::_thesis: card B = m
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 card B = m by A12, A22, A24, A25, Def1; ::_thesis: verum
end;
end;
end;
end;
end;
end;
hence ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) ; ::_thesis: verum
end;
A26: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A26, A1);
hence ex B being FinSequence of bool D st
( len B = card D & B is ascending & B is terms've_same_card_as_number ) ; ::_thesis: verum
end;
definition
let X be set ;
let IT be FinSequence of X;
attrIT is lenght_equal_card_of_set means :Def3: :: REARRAN1:def 3
ex B being finite set st
( B = union X & len IT = card B );
end;
:: deftheorem Def3 defines lenght_equal_card_of_set REARRAN1:def_3_:_
for X being set
for IT being FinSequence of X holds
( IT is lenght_equal_card_of_set iff ex B being finite set st
( B = union X & len IT = card B ) );
registration
let D be non empty finite set ;
cluster Relation-like NAT -defined bool D -valued Function-like finite FinSequence-like FinSubsequence-like terms've_same_card_as_number ascending lenght_equal_card_of_set for FinSequence of bool D;
existence
ex b1 being FinSequence of bool D st
( b1 is terms've_same_card_as_number & b1 is ascending & b1 is lenght_equal_card_of_set )
proof
consider B being 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 ; ::_thesis: ( B is terms've_same_card_as_number & B is ascending & B is lenght_equal_card_of_set )
union (bool D) = D by ZFMISC_1:81;
hence ( B is terms've_same_card_as_number & B is ascending & B is lenght_equal_card_of_set ) by A1, Def3; ::_thesis: verum
end;
end;
definition
let D be non empty finite set ;
mode RearrangmentGen of D is terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool D;
end;
theorem Th1: :: REARRAN1:1
for D being non empty finite set
for a being FinSequence of bool D holds
( a is lenght_equal_card_of_set iff len a = card D )
proof
let D be non empty finite set ; ::_thesis: for a being FinSequence of bool D holds
( a is lenght_equal_card_of_set iff len a = card D )
let A be FinSequence of bool D; ::_thesis: ( A is lenght_equal_card_of_set iff len A = card D )
thus ( A is lenght_equal_card_of_set implies len A = card D ) ::_thesis: ( len A = card D implies A is lenght_equal_card_of_set )
proof
assume A is lenght_equal_card_of_set ; ::_thesis: len A = card D
then ex B being finite set st
( B = union (bool D) & len A = card B ) by Def3;
hence len A = card D by ZFMISC_1:81; ::_thesis: verum
end;
assume A1: len A = card D ; ::_thesis: A is lenght_equal_card_of_set
take D ; :: according to REARRAN1:def_3 ::_thesis: ( D = union (bool D) & len A = card D )
thus ( D = union (bool D) & len A = card D ) by A1, ZFMISC_1:81; ::_thesis: verum
end;
theorem Th2: :: REARRAN1:2
for a being FinSequence holds
( a is ascending iff for n, m being Element of NAT st n <= m & n in dom a & m in dom a holds
a . n c= a . m )
proof
let A be FinSequence; ::_thesis: ( A is ascending iff for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m )
thus ( A is ascending implies for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) ::_thesis: ( ( for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m ) implies A is ascending )
proof
defpred S1[ Element of NAT ] means for n being Element of NAT st n <= $1 & n in dom A & $1 in dom A holds
A . n c= A . $1;
assume A1: A is ascending ; ::_thesis: for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m
A2: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A3: S1[m] ; ::_thesis: S1[m + 1]
let n be Element of NAT ; ::_thesis: ( n <= m + 1 & n in dom A & m + 1 in dom A implies A . n c= A . (m + 1) )
assume that
A4: n <= m + 1 and
A5: n in dom A and
A6: m + 1 in dom A ; ::_thesis: A . n c= A . (m + 1)
now__::_thesis:_(_(_n_=_m_+_1_&_A_._n_c=_A_._(m_+_1)_)_or_(_n_<>_m_+_1_&_A_._n_c=_A_._(m_+_1)_)_)
percases ( n = m + 1 or n <> m + 1 ) ;
case n = m + 1 ; ::_thesis: A . n c= A . (m + 1)
hence A . n c= A . (m + 1) ; ::_thesis: verum
end;
case n <> m + 1 ; ::_thesis: A . n c= A . (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, Def2;
hence A . n c= A . (m + 1) by A10, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
hence A . n c= A . (m + 1) ; ::_thesis: verum
end;
let n, m be Element of NAT ; ::_thesis: ( n <= m & n in dom A & m in dom A implies A . n c= A . m )
assume A11: ( n <= m & n in dom A & m in dom A ) ; ::_thesis: A . n c= A . m
A12: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A12, A2);
hence A . n c= A . m by A11; ::_thesis: verum
end;
assume A13: for n, m being Element of NAT st n <= m & n in dom A & m in dom A holds
A . n c= A . m ; ::_thesis: A is ascending
let n be Nat; :: according to REARRAN1:def_2 ::_thesis: ( 1 <= n & n <= (len A) - 1 implies A . n c= A . (n + 1) )
assume that
A14: 1 <= n and
A15: n <= (len A) - 1 ; ::_thesis: A . n c= A . (n + 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 A . n c= A . (n + 1) by A13, A17, NAT_1:11; ::_thesis: verum
end;
theorem Th3: :: REARRAN1:3
for D being non empty finite set
for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D holds a . (len a) = D
proof
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D holds a . (len a) = D
let A be terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D; ::_thesis: A . (len A) = 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 A . (len A) = D by A1, Lm3; ::_thesis: verum
end;
theorem Th4: :: REARRAN1:4
for D being non empty finite set
for a being lenght_equal_card_of_set FinSequence of bool D holds len a <> 0
proof
let D be non empty finite set ; ::_thesis: for a being lenght_equal_card_of_set FinSequence of bool D holds len a <> 0
let A be lenght_equal_card_of_set FinSequence of bool D; ::_thesis: len A <> 0
assume len A = 0 ; ::_thesis: contradiction
then card D = 0 by Th1;
hence contradiction ; ::_thesis: verum
end;
theorem Th5: :: REARRAN1:5
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D
for n, m being Element of NAT st n in dom a & m in dom a & n <> m holds
a . n <> a . m
proof
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D
for n, m being Element of NAT st n in dom a & m in dom a & n <> m holds
a . n <> a . m
let A be terms've_same_card_as_number ascending FinSequence of bool D; ::_thesis: for n, m being Element of NAT st n in dom A & m in dom A & n <> m holds
A . n <> A . m
let n, m be Element of NAT ; ::_thesis: ( n in dom A & m in dom A & n <> m implies A . n <> A . m )
assume that
A1: n in dom A and
A2: m in dom A and
A3: ( n <> m & A . n = A . m ) ; ::_thesis: contradiction
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; ::_thesis: verum
end;
theorem :: REARRAN1:6
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D
for n being Element of NAT st 1 <= n & n <= (len a) - 1 holds
a . n <> a . (n + 1)
proof
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D
for n being Element of NAT st 1 <= n & n <= (len a) - 1 holds
a . n <> a . (n + 1)
let A be terms've_same_card_as_number ascending FinSequence of bool D; ::_thesis: for n being Element of NAT st 1 <= n & n <= (len A) - 1 holds
A . n <> A . (n + 1)
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= (len A) - 1 implies A . n <> A . (n + 1) )
assume that
A1: 1 <= n and
A2: n <= (len A) - 1 ; ::_thesis: A . n <> A . (n + 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 A . n <> A . (n + 1) by A4, A5, Th5; ::_thesis: verum
end;
Lm5: for n being Element of NAT
for D being non empty finite set
for a being FinSequence of bool D st n in dom a holds
a . n c= D
proof
let n be Element of NAT ; ::_thesis: for D being non empty finite set
for a being FinSequence of bool D st n in dom a holds
a . n c= D
let D be non empty finite set ; ::_thesis: for a being FinSequence of bool D st n in dom a holds
a . n c= D
let a be FinSequence of bool D; ::_thesis: ( n in dom a implies a . n c= D )
assume n in dom a ; ::_thesis: a . n c= D
then a . n in bool D by FINSEQ_2:11;
hence a . n c= D ; ::_thesis: verum
end;
theorem Th7: :: REARRAN1:7
for n being Element of NAT
for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
proof
let n be Element of NAT ; ::_thesis: for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number FinSequence of bool D st n in dom a holds
a . n <> {}
let A be terms've_same_card_as_number FinSequence of bool D; ::_thesis: ( n in dom A implies A . n <> {} )
assume n in dom A ; ::_thesis: A . n <> {}
then A1: ( 1 <= n & n <= len A ) by FINSEQ_3:25;
assume A . n = {} ; ::_thesis: contradiction
hence contradiction by A1, Def1, CARD_1:27; ::_thesis: verum
end;
theorem Th8: :: REARRAN1:8
for n being Element of NAT
for D being non empty finite set
for a being 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 n be Element of NAT ; ::_thesis: for D being non empty finite set
for a being terms've_same_card_as_number FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
(a . (n + 1)) \ (a . n) <> {}
let A be terms've_same_card_as_number FinSequence of bool D; ::_thesis: ( 1 <= n & n <= (len A) - 1 implies (A . (n + 1)) \ (A . n) <> {} )
assume that
A1: 1 <= n and
A2: n <= (len A) - 1 ; ::_thesis: (A . (n + 1)) \ (A . n) <> {}
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) = {} ; ::_thesis: contradiction
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 ; ::_thesis: verum
end;
theorem Th9: :: REARRAN1:9
for D being non empty finite set
for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D ex d being Element of D st a . 1 = {d}
proof
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D ex d being Element of D st a . 1 = {d}
let A be terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D; ::_thesis: ex d being Element of D st A . 1 = {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 set 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 = x as Element of D by A2, ZFMISC_1:31;
take x ; ::_thesis: A . 1 = {x}
thus A . 1 = {x} by A2; ::_thesis: verum
end;
theorem Th10: :: REARRAN1:10
for n being Element of NAT
for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )
proof
let n be Element of NAT ; ::_thesis: for D being non empty finite set
for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )
let D be non empty finite set ; ::_thesis: for a being terms've_same_card_as_number ascending FinSequence of bool D st 1 <= n & n <= (len a) - 1 holds
ex d being Element of D st
( (a . (n + 1)) \ (a . n) = {d} & a . (n + 1) = (a . n) \/ {d} & (a . (n + 1)) \ {d} = a . n )
let A be terms've_same_card_as_number ascending FinSequence of bool D; ::_thesis: ( 1 <= n & n <= (len A) - 1 implies ex d being Element of D st
( (A . (n + 1)) \ (A . n) = {d} & A . (n + 1) = (A . n) \/ {d} & (A . (n + 1)) \ {d} = A . n ) )
assume that
A1: 1 <= n and
A2: n <= (len A) - 1 ; ::_thesis: ex d being Element of D st
( (A . (n + 1)) \ (A . n) = {d} & A . (n + 1) = (A . n) \/ {d} & (A . (n + 1)) \ {d} = A . n )
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 set 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 = x as Element of D by A10;
take x ; ::_thesis: ( (A . (n + 1)) \ (A . n) = {x} & A . (n + 1) = (A . n) \/ {x} & (A . (n + 1)) \ {x} = A . n )
thus {x} = (A . (n + 1)) \ (A . n) by A8; ::_thesis: ( A . (n + 1) = (A . n) \/ {x} & (A . (n + 1)) \ {x} = A . n )
thus (A . n) \/ {x} = (A . (n + 1)) \/ (A . n) by A8, XBOOLE_1:39
.= A . (n + 1) by A4, XBOOLE_1:12 ; ::_thesis: (A . (n + 1)) \ {x} = A . n
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 ;
::_thesis: verum
end;
definition
let D be non empty finite set ;
let A be RearrangmentGen of D;
func Co_Gen A -> RearrangmentGen of D means :: REARRAN1:def 4
for m being Nat st 1 <= m & m <= (len it) - 1 holds
it . m = D \ (A . ((len A) - m));
existence
ex b1 being RearrangmentGen of D st
for m being Nat st 1 <= m & m <= (len b1) - 1 holds
b1 . m = D \ (A . ((len A) - m))
proof
deffunc H1( Nat) -> Element of bool D = D \ (A . ((len A) - $1));
set c = card D;
D c= D ;
then reconsider y = D as Subset of D ;
0 + 1 <= card D by NAT_1:13;
then max (0,((card D) - 1)) = (card D) - 1 by FINSEQ_2:4;
then reconsider c1 = (card D) - 1 as Element of NAT by FINSEQ_2:5;
consider f being FinSequence such that
A1: len f = c1 and
A2: for m being Nat st m in dom f holds
f . m = H1(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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in bool D )
assume x in rng f ; ::_thesis: x in bool D
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 x in bool D ; ::_thesis: verum
end;
then reconsider f = f as FinSequence of bool D by FINSEQ_1:def_4;
set C = f ^ <*y*>;
A5: len (f ^ <*y*>) = (len f) + (len <*y*>) by FINSEQ_1:22
.= (len f) + 1 by FINSEQ_1:39 ;
A6: card D = len A by Th1;
A7: f ^ <*y*> is terms've_same_card_as_number
proof
let m be Nat; :: according to REARRAN1:def_1 ::_thesis: ( 1 <= m & m <= len (f ^ <*y*>) implies for B being finite set st B = (f ^ <*y*>) . m holds
card B = m )
assume that
A8: 1 <= m and
A9: m <= len (f ^ <*y*>) ; ::_thesis: for B being finite set st B = (f ^ <*y*>) . m holds
card B = m
max (0,((len (f ^ <*y*>)) - m)) = (len (f ^ <*y*>)) - m by A9, FINSEQ_2:4;
then reconsider l = (len (f ^ <*y*>)) - m as Element of NAT by FINSEQ_2:5;
let B be finite set ; ::_thesis: ( B = (f ^ <*y*>) . m implies card B = m )
assume A10: B = (f ^ <*y*>) . m ; ::_thesis: card B = m
now__::_thesis:_(_(_m_=_len_(f_^_<*y*>)_&_card_B_=_m_)_or_(_m_<>_len_(f_^_<*y*>)_&_card_B_=_m_)_)
percases ( m = len (f ^ <*y*>) or m <> len (f ^ <*y*>) ) ;
case m = len (f ^ <*y*>) ; ::_thesis: card B = m
hence card B = m by A1, A5, A10, FINSEQ_1:42; ::_thesis: verum
end;
case m <> len (f ^ <*y*>) ; ::_thesis: card B = m
then m < len (f ^ <*y*>) by A9, XXREAL_0:1;
then A11: m + 1 <= len (f ^ <*y*>) 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 (f ^ <*y*>)) - 1 by A11, XREAL_1:19;
then A15: m in dom f by A5, A8, FINSEQ_3:25;
then (f ^ <*y*>) . 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 ;
::_thesis: verum
end;
end;
end;
hence card B = m ; ::_thesis: verum
end;
for m being Nat st 1 <= m & m <= (len (f ^ <*y*>)) - 1 holds
(f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
proof
let m be Nat; ::_thesis: ( 1 <= m & m <= (len (f ^ <*y*>)) - 1 implies (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) )
assume that
A16: 1 <= m and
A17: m <= (len (f ^ <*y*>)) - 1 ; ::_thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
A18: m in dom f by A5, A16, A17, FINSEQ_3:25;
then A19: (f ^ <*y*>) . m = f . m by FINSEQ_1:def_7
.= D \ (A . ((len A) - m)) by A2, A18 ;
percases ( m = (len (f ^ <*y*>)) - 1 or m <> (len (f ^ <*y*>)) - 1 ) ;
suppose m = (len (f ^ <*y*>)) - 1 ; ::_thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
then (f ^ <*y*>) . (m + 1) = D by A5, FINSEQ_1:42;
hence (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) by A19; ::_thesis: verum
end;
suppose m <> (len (f ^ <*y*>)) - 1 ; ::_thesis: (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1)
then A20: m < (len (f ^ <*y*>)) - 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 (f ^ <*y*>)) - 1 by A5, A20, NAT_1:13;
then A23: m + 1 in dom f by A5, A22, FINSEQ_3:25;
then A24: (f ^ <*y*>) . (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 (f ^ <*y*>) . m c= (f ^ <*y*>) . (m + 1) by A19, A24, XBOOLE_1:34; ::_thesis: verum
end;
end;
end;
then reconsider C = f ^ <*y*> as RearrangmentGen of D by A1, A5, A7, Def2, Th1;
take C ; ::_thesis: for m being Nat st 1 <= m & m <= (len C) - 1 holds
C . m = D \ (A . ((len A) - m))
let m be Nat; ::_thesis: ( 1 <= m & m <= (len C) - 1 implies C . m = D \ (A . ((len A) - m)) )
assume ( 1 <= m & m <= (len C) - 1 ) ; ::_thesis: C . m = D \ (A . ((len A) - m))
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 ;
::_thesis: verum
end;
uniqueness
for b1, b2 being RearrangmentGen of D st ( for m being Nat st 1 <= m & m <= (len b1) - 1 holds
b1 . m = D \ (A . ((len A) - m)) ) & ( for m being Nat st 1 <= m & m <= (len b2) - 1 holds
b2 . m = D \ (A . ((len A) - m)) ) holds
b1 = b2
proof
let f1, f2 be RearrangmentGen of D; ::_thesis: ( ( for m being Nat st 1 <= m & m <= (len f1) - 1 holds
f1 . m = D \ (A . ((len A) - m)) ) & ( for m being Nat st 1 <= m & m <= (len f2) - 1 holds
f2 . m = D \ (A . ((len A) - m)) ) implies f1 = f2 )
assume that
A27: for m being Nat st 1 <= m & m <= (len f1) - 1 holds
f1 . m = D \ (A . ((len A) - m)) and
A28: for m being Nat st 1 <= m & m <= (len f2) - 1 holds
f2 . m = D \ (A . ((len A) - m)) ; ::_thesis: f1 = f2
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__::_thesis:_for_m_being_Nat_st_m_in_dom_f1_holds_
f1_._m_=_f2_._m
let m be Nat; ::_thesis: ( m in dom f1 implies f1 . b1 = f2 . b1 )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
assume A33: m in dom f1 ; ::_thesis: f1 . b1 = f2 . b1
then A34: 1 <= m by A32, FINSEQ_1:1;
A35: m <= len A by A32, A33, FINSEQ_1:1;
percases ( m = len A or m <> len A ) ;
supposeA36: m = len A ; ::_thesis: f1 . b1 = f2 . b1
then f1 . m = D by A31, A30, Th3;
hence f1 . m = f2 . m by A29, A30, A36, Th3; ::_thesis: verum
end;
suppose m <> len A ; ::_thesis: f1 . b1 = f2 . b1
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; ::_thesis: verum
end;
end;
end;
hence f1 = f2 by A31, A29, FINSEQ_2:9; ::_thesis: verum
end;
involutiveness
for b1, b2 being RearrangmentGen of D st ( for m being Nat st 1 <= m & m <= (len b1) - 1 holds
b1 . m = D \ (b2 . ((len b2) - m)) ) holds
for m being Nat st 1 <= m & m <= (len b2) - 1 holds
b2 . m = D \ (b1 . ((len b1) - m))
proof
let B, A be RearrangmentGen of D; ::_thesis: ( ( for m being Nat st 1 <= m & m <= (len B) - 1 holds
B . m = D \ (A . ((len A) - m)) ) implies for m being Nat st 1 <= m & m <= (len A) - 1 holds
A . m = D \ (B . ((len B) - m)) )
assume A38: for m being Nat st 1 <= m & m <= (len B) - 1 holds
B . m = D \ (A . ((len A) - m)) ; ::_thesis: for m being Nat st 1 <= m & m <= (len A) - 1 holds
A . m = D \ (B . ((len B) - m))
let m be Nat; ::_thesis: ( 1 <= m & m <= (len A) - 1 implies A . m = D \ (B . ((len B) - m)) )
assume A39: ( 1 <= m & m <= (len A) - 1 ) ; ::_thesis: A . m = D \ (B . ((len B) - m))
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 ; ::_thesis: verum
end;
end;
:: deftheorem defines Co_Gen REARRAN1:def_4_:_
for D being non empty finite set
for A, b3 being RearrangmentGen of D holds
( b3 = Co_Gen A iff for m being Nat st 1 <= m & m <= (len b3) - 1 holds
b3 . m = D \ (A . ((len A) - m)) );
theorem :: REARRAN1:11
canceled;
theorem Th12: :: REARRAN1:12
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
len (MIM (FinS (F,D))) = len (CHI (A,C))
let A be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies len (MIM (FinS (F,D))) = len (CHI (A,C)) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: len (MIM (FinS (F,D))) = len (CHI (A,C))
set a = FinS (F,D);
reconsider a9 = FinS (F,D) 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 (FinS (F,D)) = Seg (len (FinS (F,D))) & 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 (FinS (F,D)) by A2, A3, A5, FINSEQ_1:57
.= len (MIM (FinS (F,D))) by RFINSEQ:def_2 ; ::_thesis: verum
end;
definition
let D, C be non empty finite set ;
let A be RearrangmentGen of C;
let F be PartFunc of D,REAL;
func Rland (F,A) -> PartFunc of C,REAL equals :: REARRAN1:def 5
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));
correctness
coherence
Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is PartFunc of C,REAL;
;
func Rlor (F,A) -> PartFunc of C,REAL equals :: REARRAN1:def 6
Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C)));
correctness
coherence
Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C))) is PartFunc of C,REAL;
;
end;
:: deftheorem defines Rland REARRAN1:def_5_:_
for D, C being non empty finite set
for A being RearrangmentGen of C
for F being PartFunc of D,REAL holds Rland (F,A) = Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));
:: deftheorem defines Rlor REARRAN1:def_6_:_
for D, C being non empty finite set
for A being RearrangmentGen of C
for F being PartFunc of D,REAL holds Rlor (F,A) = Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C)));
theorem Th13: :: REARRAN1:13
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rland (F,A)) = C
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rland (F,A)) = C
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rland (F,A)) = C
let A be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies dom (Rland (F,A)) = 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 ) ; ::_thesis: dom (Rland (F,A)) = C
then A2: len (MIM (FinS (F,D))) = len (CHI (A,C)) by Th12;
thus dom (Rland (F,A)) c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= dom (Rland (F,A))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in dom (Rland (F,A)) )
assume x in C ; ::_thesis: x in dom (Rland (F,A))
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, RFUNCT_3:def_7;
hence x in dom (Rland (F,A)) by A2, A1, RFUNCT_3:28; ::_thesis: verum
end;
theorem Th14: :: REARRAN1:14
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
proof
let C, D be non empty finite set ; ::_thesis: for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
let c be Element of C; ::_thesis: for F being PartFunc of D,REAL
for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
let A be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) ) )
set fd = FinS (F,D);
set mf = MIM (FinS (F,D));
set h = CHI (A,C);
set fh = ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c;
A1: dom A = Seg (len A) by FINSEQ_1:def_3;
A2: dom ((MIM (FinS (F,D))) (#) (CHI (A,C))) = Seg (len ((MIM (FinS (F,D))) (#) (CHI (A,C)))) by FINSEQ_1:def_3;
A3: len (CHI (A,C)) = len A by RFUNCT_3:def_6;
A4: len (MIM (FinS (F,D))) = len (FinS (F,D)) by RFINSEQ:def_2;
A5: dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = Seg (len (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c)) by FINSEQ_1:def_3;
A6: min ((len (MIM (FinS (F,D)))),(len (CHI (A,C)))) = len ((MIM (FinS (F,D))) (#) (CHI (A,C))) by RFUNCT_3:def_7;
assume ( F is total & card C = card D ) ; ::_thesis: ( ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) & ( for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) ) )
then A7: len (MIM (FinS (F,D))) = len (CHI (A,C)) by Th12;
A8: len (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = len ((MIM (FinS (F,D))) (#) (CHI (A,C))) by RFUNCT_3:def_8;
A9: dom (CHI (A,C)) = Seg (len (CHI (A,C))) by FINSEQ_1:def_3;
thus ( c in A . 1 implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) ) ::_thesis: for n being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))
proof
assume A10: c in A . 1 ; ::_thesis: ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D))
A11: for n being Element of NAT st n in dom A holds
c in A . n
proof
let n be Element of NAT ; ::_thesis: ( n in dom A implies c in A . n )
assume A12: n in dom A ; ::_thesis: c in A . n
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 c in A . n by A10; ::_thesis: verum
end;
A14: dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) = Seg (len (MIM (FinS (F,D)))) by A7, A6, A8, FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_holds_
(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_(MIM_(FinS_(F,D)))_._m
let m be Nat; ::_thesis: ( m in dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) implies (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
reconsider r1 = (FinS (F,D)) . m as Real ;
assume A15: m in dom (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m
then A16: 1 <= m by FINSEQ_3:25;
A17: (CHI (A,C)) . 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 (MIM (FinS (F,D))) by A14, A15, FINSEQ_1:def_3;
then A19: m <= len (MIM (FinS (F,D))) by FINSEQ_3:25;
now__::_thesis:_(_(_m_=_len_(MIM_(FinS_(F,D)))_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_(MIM_(FinS_(F,D)))_._m_)_or_(_m_<>_len_(MIM_(FinS_(F,D)))_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_(MIM_(FinS_(F,D)))_._m1_)_)
percases ( m = len (MIM (FinS (F,D))) or m <> len (MIM (FinS (F,D))) ) ;
caseA20: m = len (MIM (FinS (F,D))) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m
then (MIM (FinS (F,D))) . m = r1 by A4, RFINSEQ:def_2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = r1 (#) (chi ((A . m),C)) by A2, A5, A8, A15, A17, RFUNCT_3:def_7;
then A21: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # 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 (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = r1 * ((chi ((A . m),C)) . c) by A21, VALUED_1:def_5
.= r1 * 1 by A18, RFUNCT_1:63
.= (MIM (FinS (F,D))) . m by A4, A20, RFINSEQ:def_2 ;
::_thesis: verum
end;
caseA22: m <> len (MIM (FinS (F,D))) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m1
reconsider r2 = (FinS (F,D)) . (m + 1) as Real ;
m < len (MIM (FinS (F,D))) by A19, A22, XXREAL_0:1;
then m + 1 <= len (MIM (FinS (F,D))) by NAT_1:13;
then A23: m <= (len (MIM (FinS (F,D)))) - 1 by XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A16, RFINSEQ:def_2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A5, A8, A15, A17, RFUNCT_3:def_7;
then A24: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # 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 (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 - r2) * ((chi ((A . m),C)) . c) by A24, VALUED_1:def_5
.= (r1 - r2) * 1 by A18, RFUNCT_1:63
.= (MIM (FinS (F,D))) . m1 by A16, A23, RFINSEQ:def_2 ;
::_thesis: verum
end;
end;
end;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (MIM (FinS (F,D))) . m ; ::_thesis: verum
end;
hence ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = MIM (FinS (F,D)) by A7, A6, A8, FINSEQ_2:9; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) implies ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) )
assume that
A25: 1 <= n and
A26: n < len A and
A27: c in (A . (n + 1)) \ (A . n) ; ::_thesis: ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))
A28: len ((MIM (FinS (F,D))) /^ n) = (len (MIM (FinS (F,D)))) - n by A7, A3, A26, RFINSEQ:def_1;
A29: for k being Element of NAT st k in dom A & k <= n holds
not c in A . k
proof
let k be Element of NAT ; ::_thesis: ( k in dom A & k <= n implies not c in A . k )
assume A30: ( k in dom A & k <= n ) ; ::_thesis: not c in A . k
assume A31: c in A . k ; ::_thesis: contradiction
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; ::_thesis: verum
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 being Element of NAT st k in dom A & n + 1 <= k holds
c in A . k
proof
let k be Element of NAT ; ::_thesis: ( k in dom A & n + 1 <= k implies c in A . k )
assume A36: ( k in dom A & n + 1 <= k ) ; ::_thesis: c in A . k
n + 1 in dom A by A33, A34, FINSEQ_3:25;
then A . (n + 1) c= A . k by A36, Th2;
hence c in A . k by A32; ::_thesis: verum
end;
set fdn = (FinS (F,D)) /^ n;
set mfn = MIM ((FinS (F,D)) /^ n);
set n0 = n |-> 0;
A37: len (MIM ((FinS (F,D)) /^ n)) = len ((FinS (F,D)) /^ n) by RFINSEQ:def_2;
A38: len (n |-> 0) = n by CARD_1:def_7;
len ((FinS (F,D)) /^ n) = (len (FinS (F,D))) - n by A7, A3, A4, A26, RFINSEQ:def_1;
then A39: len ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) = n + ((len (FinS (F,D))) - n) by A37, A38, FINSEQ_1:22
.= len (MIM (FinS (F,D))) by RFINSEQ:def_2 ;
then A40: dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) = Seg (len (MIM (FinS (F,D)))) by FINSEQ_1:def_3;
A41: dom (n |-> 0) = Seg (len (n |-> 0)) by FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_m_in_dom_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_holds_
(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_._m
let m be Nat; ::_thesis: ( m in dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) implies (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m )
reconsider m1 = m as Element of NAT by ORDINAL1:def_12;
reconsider r1 = (FinS (F,D)) . m as Real ;
assume A42: m in dom ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m
then A43: 1 <= m by FINSEQ_3:25;
m in dom (MIM (FinS (F,D))) by A40, A42, FINSEQ_1:def_3;
then A44: m <= len (MIM (FinS (F,D))) by FINSEQ_3:25;
A45: (CHI (A,C)) . m = chi ((A . m),C) by A9, A7, A40, A42, RFUNCT_3:def_6;
now__::_thesis:_(_(_m_<=_n_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_._m_)_or_(_n_<_m_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_._m_)_)
percases ( m <= n or n < m ) ;
caseA46: m <= n ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m
reconsider r2 = (FinS (F,D)) . (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 (MIM (FinS (F,D)))) - 1 by A7, A3, XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A43, RFINSEQ:def_2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def_7;
then A47: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # 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: (n |-> 0) . 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 (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 - r2) * ((chi ((A . m),C)) . c) by A47, VALUED_1:def_5
.= ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m by A38, A41, A48, A49, A50, FINSEQ_1:def_7 ;
::_thesis: verum
end;
caseA51: n < m ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ 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__::_thesis:_(_(_m_=_len_(MIM_(FinS_(F,D)))_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_._m_)_or_(_m_<>_len_(MIM_(FinS_(F,D)))_&_(((MIM_(FinS_(F,D)))_(#)_(CHI_(A,C)))_#_c)_._m_=_((n_|->_0)_^_(MIM_((FinS_(F,D))_/^_n)))_._m_)_)
percases ( m = len (MIM (FinS (F,D))) or m <> len (MIM (FinS (F,D))) ) ;
caseA55: m = len (MIM (FinS (F,D))) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m
then (MIM (FinS (F,D))) . m = r1 by A4, RFINSEQ:def_2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = r1 (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def_7;
then A56: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 (#) (chi ((A . m),C))) . c by A5, A7, A6, A8, A40, A42, RFUNCT_3:def_8;
A57: mn in dom ((MIM (FinS (F,D))) /^ n) by A28, A54, A55, FINSEQ_3:25;
A58: ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m = (MIM ((FinS (F,D)) /^ n)) . (m - n) by A38, A39, A44, A51, FINSEQ_1:24
.= ((MIM (FinS (F,D))) /^ n) . mn by RFINSEQ:15
.= (MIM (FinS (F,D))) . (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 (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = r1 * ((chi ((A . m),C)) . c) by A56, VALUED_1:def_5
.= ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m by A53, A58 ;
::_thesis: verum
end;
caseA59: m <> len (MIM (FinS (F,D))) ; ::_thesis: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m
reconsider r2 = (FinS (F,D)) . (m + 1) as Real ;
m < len (MIM (FinS (F,D))) by A44, A59, XXREAL_0:1;
then m + 1 <= len (MIM (FinS (F,D))) by NAT_1:13;
then A60: m <= (len (MIM (FinS (F,D)))) - 1 by XREAL_1:19;
then (MIM (FinS (F,D))) . m1 = r1 - r2 by A43, RFINSEQ:def_2;
then ((MIM (FinS (F,D))) (#) (CHI (A,C))) . m = (r1 - r2) (#) (chi ((A . m),C)) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def_7;
then A61: (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((r1 - r2) (#) (chi ((A . m),C))) . c by A5, A7, A6, A8, A40, A42, RFUNCT_3:def_8;
mn <= len ((MIM (FinS (F,D))) /^ n) by A28, A44, XREAL_1:9;
then A62: mn in dom ((MIM (FinS (F,D))) /^ n) by A54, FINSEQ_3:25;
A63: ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m = (MIM ((FinS (F,D)) /^ n)) . (m - n) by A38, A39, A44, A51, FINSEQ_1:24
.= ((MIM (FinS (F,D))) /^ n) . mn by RFINSEQ:15
.= (MIM (FinS (F,D))) . (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 (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = (r1 - r2) * ((chi ((A . m),C)) . c) by A61, VALUED_1:def_5
.= ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m by A53, A63 ;
::_thesis: verum
end;
end;
end;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m ; ::_thesis: verum
end;
end;
end;
hence (((MIM (FinS (F,D))) (#) (CHI (A,C))) # c) . m = ((n |-> 0) ^ (MIM ((FinS (F,D)) /^ n))) . m ; ::_thesis: verum
end;
hence ((MIM (FinS (F,D))) (#) (CHI (A,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) by A7, A6, A8, A39, FINSEQ_2:9; ::_thesis: verum
end;
theorem Th15: :: REARRAN1:15
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT 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, D be non empty finite set ; ::_thesis: for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let c be Element of C; ::_thesis: for F being PartFunc of D,REAL
for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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 being Element of NAT st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds
(Rland (F,A)) . c = (FinS (F,D)) . (n + 1) ) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( ( c in B . 1 implies (Rland (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland (F,B)) . c = (FinS (F,D)) . (n + 1) ) ) )
set fd = FinS (F,D);
set mf = MIM (FinS (F,D));
set h = CHI (B,C);
A1: (Rland (F,B)) . c = Sum (((MIM (FinS (F,D))) (#) (CHI (B,C))) # c) by RFUNCT_3:32, RFUNCT_3:33;
A2: ( len (CHI (B,C)) = len B & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def_2, RFUNCT_3:def_6;
assume A3: ( F is total & card C = card D ) ; ::_thesis: ( ( c in B . 1 implies (Rland (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland (F,B)) . c = (FinS (F,D)) . (n + 1) ) )
then A4: len (MIM (FinS (F,D))) = len (CHI (B,C)) by Th12;
thus ( c in B . 1 implies (Rland (F,B)) . c = (FinS (F,D)) . 1 ) ::_thesis: for n being Element of NAT st 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) holds
(Rland (F,B)) . c = (FinS (F,D)) . (n + 1)
proof
assume c in B . 1 ; ::_thesis: (Rland (F,B)) . c = (FinS (F,D)) . 1
hence (Rland (F,B)) . c = Sum (MIM (FinS (F,D))) by A3, A1, Th14
.= (FinS (F,D)) . 1 by A4, A2, Th4, RFINSEQ:16 ;
::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len B & c in (B . (n + 1)) \ (B . n) implies (Rland (F,B)) . c = (FinS (F,D)) . (n + 1) )
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) ; ::_thesis: (Rland (F,B)) . c = (FinS (F,D)) . (n + 1)
((MIM (FinS (F,D))) (#) (CHI (B,C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) by A3, A5, A6, A7, Th14;
hence (Rland (F,B)) . c = (Sum (n |-> 0)) + (Sum (MIM ((FinS (F,D)) /^ n))) by A1, RVSUM_1:75
.= 0 + (Sum (MIM ((FinS (F,D)) /^ n))) by RVSUM_1:81
.= (FinS (F,D)) . (n + 1) by A4, A2, A6, RFINSEQ:17 ;
::_thesis: verum
end;
theorem Th16: :: REARRAN1:16
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rland (F,A)) = rng (FinS (F,D))
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rland (F,A)) = rng (FinS (F,D))
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rland (F,A)) = rng (FinS (F,D))
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies rng (Rland (F,B)) = rng (FinS (F,D)) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: rng (Rland (F,B)) = rng (FinS (F,D))
set fd = FinS (F,D);
set p = Rland (F,B);
set mf = MIM (FinS (F,D));
set h = CHI (B,C);
A3: len (MIM (FinS (F,D))) = len (CHI (B,C)) by A1, A2, Th12;
A4: dom F = D by A1, PARTFUN1:def_2;
then reconsider fd9 = FinS (F,D), F9 = F as finite Function by FINSET_1:10;
reconsider dfd = dom fd9, dF = dom F9 as finite set ;
A5: ( len (CHI (B,C)) = len B & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def_2, RFUNCT_3:def_6;
A6: dom (Rland (F,B)) = C by A1, A2, Th13;
A7: dom (FinS (F,D)) = Seg (len (FinS (F,D))) 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 FinS (F,D),F are_fiberwise_equipotent by A4, RFUNCT_3:def_13;
then card dfd = card dF by CLASSES1:81;
then len (FinS (F,D)) <> 0 by A4, A7;
then A9: 0 + 1 <= len (FinS (F,D)) by NAT_1:13;
then A10: 1 in dom (FinS (F,D)) by FINSEQ_3:25;
thus rng (Rland (F,B)) c= rng (FinS (F,D)) :: according to XBOOLE_0:def_10 ::_thesis: rng (FinS (F,D)) c= rng (Rland (F,B))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rland (F,B)) or x in rng (FinS (F,D)) )
assume x in rng (Rland (F,B)) ; ::_thesis: x in rng (FinS (F,D))
then consider c being Element of C such that
c in dom (Rland (F,B)) and
A11: (Rland (F,B)) . c = x by PARTFUN1:3;
defpred S1[ set ] means ( $1 in dom B & c in B . $1 );
A12: ex n being Nat st S1[n]
proof
take n = len B; ::_thesis: S1[n]
B . n = C by Th3;
hence S1[n] by A3, A5, A9, FINSEQ_3:25; ::_thesis: verum
end;
consider mi being Nat such that
A13: ( S1[mi] & ( for n being Nat st S1[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__::_thesis:_(_(_mi_=_1_&_x_in_rng_(FinS_(F,D))_)_or_(_mi_<>_1_&_x_in_rng_(FinS_(F,D))_)_)
percases ( mi = 1 or mi <> 1 ) ;
case mi = 1 ; ::_thesis: x in rng (FinS (F,D))
then (Rland (F,B)) . c = (FinS (F,D)) . 1 by A1, A2, A13, Th15;
hence x in rng (FinS (F,D)) by A10, A11, FUNCT_1:def_3; ::_thesis: verum
end;
case mi <> 1 ; ::_thesis: x in rng (FinS (F,D))
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 (Rland (F,B)) . c = (FinS (F,D)) . (m1 + 1) by A1, A2, A16, A18, Th15;
hence x in rng (FinS (F,D)) by A3, A5, A7, A8, A11, A13, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence x in rng (FinS (F,D)) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (FinS (F,D)) or x in rng (Rland (F,B)) )
defpred S1[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
assume x in rng (FinS (F,D)) ; ::_thesis: x in rng (Rland (F,B))
then A19: ex n being Nat st S1[n] by FINSEQ_2:10;
consider mi being Nat such that
A20: ( S1[mi] & ( for n being Nat st S1[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 (FinS (F,D)) by A20, FINSEQ_3:25;
now__::_thesis:_(_(_mi_=_1_&_x_in_rng_(Rland_(F,B))_)_or_(_mi_<>_1_&_x_in_rng_(Rland_(F,B))_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA23: mi = 1 ; ::_thesis: x in rng (Rland (F,B))
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 = the Element of B . 1 as Element of C by A24, TARSKI:def_3;
(Rland (F,B)) . y = (FinS (F,D)) . 1 by A1, A2, A24, Th15;
hence x in rng (Rland (F,B)) by A6, A20, A23, FUNCT_1:def_3; ::_thesis: verum
end;
caseA25: mi <> 1 ; ::_thesis: x in rng (Rland (F,B))
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 (FinS (F,D)) by A20, FINSEQ_3:25;
then m1 <= (len (FinS (F,D))) - 1 by XREAL_1:19;
then A27: (B . (m1 + 1)) \ (B . m1) <> {} by A3, A5, A26, Th8;
then A28: the Element of (B . (m1 + 1)) \ (B . m1) in B . (m1 + 1) by XBOOLE_0:def_5;
B . mi c= C by A3, A5, A7, A8, A20, Lm5;
then reconsider y = the Element of (B . (m1 + 1)) \ (B . m1) as Element of C by A28;
m1 < mi by XREAL_1:44;
then m1 < len (FinS (F,D)) by A22, XXREAL_0:2;
then (Rland (F,B)) . y = (FinS (F,D)) . (m1 + 1) by A1, A2, A3, A5, A26, A27, Th15;
hence x in rng (Rland (F,B)) by A6, A20, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence x in rng (Rland (F,B)) ; ::_thesis: verum
end;
theorem Th17: :: REARRAN1:17
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Rland (F,A), FinS (F,D) are_fiberwise_equipotent
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies Rland (F,B), FinS (F,D) are_fiberwise_equipotent )
set fd = FinS (F,D);
set p = Rland (F,B);
set mf = MIM (FinS (F,D));
set h = CHI (B,C);
dom (Rland (F,B)) is finite ;
then reconsider p = Rland (F,B) as finite PartFunc of C,REAL by FINSET_1:10;
A1: ( len (CHI (B,C)) = len B & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def_2, RFUNCT_3:def_6;
A2: ( dom (FinS (F,D)) = Seg (len (FinS (F,D))) & dom B = Seg (len B) ) by FINSEQ_1:def_3;
assume A3: ( F is total & card C = card D ) ; ::_thesis: Rland (F,B), FinS (F,D) are_fiberwise_equipotent
then A4: len (MIM (FinS (F,D))) = len (CHI (B,C)) by Th12;
A5: dom p = C by A3, Th13;
A6: rng p = rng (FinS (F,D)) by A3, Th16;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((FinS_(F,D)),x))_=_card_(Coim_(p,x))
let x be set ; ::_thesis: card (Coim ((FinS (F,D)),x)) = card (Coim (p,x))
now__::_thesis:_(_(_not_x_in_rng_(FinS_(F,D))_&_card_((FinS_(F,D))_"_{x})_=_card_(p_"_{x})_)_or_(_x_in_rng_(FinS_(F,D))_&_card_((FinS_(F,D))_"_{x})_=_card_(p_"_{x})_)_)
percases ( not x in rng (FinS (F,D)) or x in rng (FinS (F,D)) ) ;
caseA7: not x in rng (FinS (F,D)) ; ::_thesis: card ((FinS (F,D)) " {x}) = card (p " {x})
then (FinS (F,D)) " {x} = {} by Lm1;
hence card ((FinS (F,D)) " {x}) = card (p " {x}) by A6, A7, Lm1; ::_thesis: verum
end;
caseA8: x in rng (FinS (F,D)) ; ::_thesis: card ((FinS (F,D)) " {x}) = card (p " {x})
defpred S1[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
A9: for n being Nat st S1[n] holds
n <= len (FinS (F,D)) by FINSEQ_3:25;
A10: ex n being Nat st S1[n] by A8, FINSEQ_2:10;
consider ma being Nat such that
A11: ( S1[ma] & ( for n being Nat st S1[n] holds
n <= ma ) ) from NAT_1:sch_6(A9, A10);
A12: ex n being Nat st S1[n] by A8, FINSEQ_2:10;
consider mi being Nat such that
A13: ( S1[mi] & ( for n being Nat st S1[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 (FinS (F,D)) by A11, FINSEQ_3:25;
A17: (Seg ma) \ (Seg m1) = (FinS (F,D)) " {x}
proof
thus (Seg ma) \ (Seg m1) c= (FinS (F,D)) " {x} :: according to XBOOLE_0:def_10 ::_thesis: (FinS (F,D)) " {x} c= (Seg ma) \ (Seg m1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Seg ma) \ (Seg m1) or y in (FinS (F,D)) " {x} )
assume A18: y in (Seg ma) \ (Seg m1) ; ::_thesis: y in (FinS (F,D)) " {x}
then reconsider l = y as Element of NAT ;
reconsider o = (FinS (F,D)) . 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 (FinS (F,D)) by A16, XXREAL_0:2;
then A22: l in dom (FinS (F,D)) 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__::_thesis:_(_(_l_=_ma_&_y_in_(FinS_(F,D))_"_{x}_)_or_(_l_<>_ma_&_y_in_(FinS_(F,D))_"_{x}_)_)
percases ( l = ma or l <> ma ) ;
case l = ma ; ::_thesis: y in (FinS (F,D)) " {x}
then o in {x} by A11, TARSKI:def_1;
hence y in (FinS (F,D)) " {x} by A22, FUNCT_1:def_7; ::_thesis: verum
end;
case l <> ma ; ::_thesis: y in (FinS (F,D)) " {x}
then l < ma by A21, XXREAL_0:1;
then A24: o >= r by A11, A22, RFINSEQ:19;
now__::_thesis:_(_(_l_=_mi_&_y_in_(FinS_(F,D))_"_{x}_)_or_(_l_<>_mi_&_y_in_(FinS_(F,D))_"_{x}_)_)
percases ( l = mi or l <> mi ) ;
case l = mi ; ::_thesis: y in (FinS (F,D)) " {x}
then o in {x} by A13, TARSKI:def_1;
hence y in (FinS (F,D)) " {x} by A22, FUNCT_1:def_7; ::_thesis: verum
end;
case l <> mi ; ::_thesis: y in (FinS (F,D)) " {x}
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 y in (FinS (F,D)) " {x} by A22, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence y in (FinS (F,D)) " {x} ; ::_thesis: verum
end;
end;
end;
hence y in (FinS (F,D)) " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (FinS (F,D)) " {x} or y in (Seg ma) \ (Seg m1) )
assume A25: y in (FinS (F,D)) " {x} ; ::_thesis: y in (Seg ma) \ (Seg m1)
then A26: y in dom (FinS (F,D)) by FUNCT_1:def_7;
reconsider l = y as Element of NAT by A25;
A27: 1 <= l by A26, FINSEQ_3:25;
(FinS (F,D)) . y in {x} by A25, FUNCT_1:def_7;
then A28: (FinS (F,D)) . 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 y in (Seg ma) \ (Seg m1) by A29, XBOOLE_0:def_5; ::_thesis: verum
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 ((FinS (F,D)) " {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 (FinS (F,D)) by A13, FINSEQ_3:25;
then 1 <= len (FinS (F,D)) by A14, XXREAL_0:2;
then A35: 1 in dom (FinS (F,D)) by FINSEQ_3:25;
now__::_thesis:_(_(_mi_=_1_&_card_(p_"_{x})_=_card_((FinS_(F,D))_"_{x})_)_or_(_mi_<>_1_&_card_(p_"_{x})_=_card_((FinS_(F,D))_"_{x})_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA36: mi = 1 ; ::_thesis: card (p " {x}) = card ((FinS (F,D)) " {x})
B . ma = p " {x}
proof
thus B . ma c= p " {x} :: according to XBOOLE_0:def_10 ::_thesis: p " {x} c= B . ma
proof
defpred S2[ Element of NAT ] means ( $1 in dom B & $1 <= ma implies for c being Element of C st c in B . $1 holds
c in p " {x} );
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in B . ma or y in p " {x} )
assume A37: y in B . ma ; ::_thesis: y in p " {x}
B . ma c= C by A4, A1, A2, A11, Lm5;
then reconsider cy = y as Element of C by A37;
A38: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A39: S2[n] ; ::_thesis: S2[n + 1]
assume that
A40: n + 1 in dom B and
A41: n + 1 <= ma ; ::_thesis: for c being Element of C st c in B . (n + 1) holds
c in p " {x}
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; ::_thesis: ( c in B . (n + 1) implies c in p " {x} )
assume A45: c in B . (n + 1) ; ::_thesis: c in p " {x}
A46: n <= len B by A42, NAT_1:13;
now__::_thesis:_(_(_n_=_0_&_c_in_p_"_{x}_)_or_(_n_<>_0_&_c_in_p_"_{x}_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: c in p " {x}
then p . c = x by A3, A13, A36, A45, Th15;
then p . c in {x} by TARSKI:def_1;
hence c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
caseA47: n <> 0 ; ::_thesis: c in p " {x}
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__::_thesis:_(_(_c_in_(B_._(n_+_1))_\_(B_._n)_&_c_in_p_"_{x}_)_or_(_c_in_B_._n_&_c_in_p_"_{x}_)_)
percases ( c in (B . (n + 1)) \ (B . n) or c in B . n ) by A45, A50, XBOOLE_0:def_3;
case c in (B . (n + 1)) \ (B . n) ; ::_thesis: c in p " {x}
then A51: p . c = (FinS (F,D)) . (n + 1) by A3, A44, A49, Th15;
now__::_thesis:_(_(_n_+_1_=_ma_&_c_in_p_"_{x}_)_or_(_n_+_1_<>_ma_&_c_in_p_"_{x}_)_)
percases ( n + 1 = ma or n + 1 <> ma ) ;
case n + 1 = ma ; ::_thesis: c in p " {x}
then p . c in {x} by A11, A51, TARSKI:def_1;
hence c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
case n + 1 <> ma ; ::_thesis: c in p " {x}
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 c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
case c in B . n ; ::_thesis: c in p " {x}
hence c in p " {x} by A39, A41, A46, A49, FINSEQ_3:25, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
A53: S2[ 0 ] by FINSEQ_3:25;
A54: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A53, A38);
ma in dom B by A4, A1, A11, FINSEQ_3:29;
then cy in p " {x} by A37, A54;
hence y in p " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p " {x} or y in B . ma )
assume A55: y in p " {x} ; ::_thesis: y in B . ma
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 S2[ Nat] means ( $1 in dom B & ma < $1 & cy in B . $1 );
assume A57: not y in B . ma ; ::_thesis: contradiction
A58: ex n being Nat st S2[n]
proof
take n = len B; ::_thesis: S2[n]
len B <> 0 by Th4;
then 0 + 1 <= len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25; ::_thesis: ( ma < n & cy in B . n )
A59: B . n = C by Th3;
now__::_thesis:_not_n_<=_ma
assume n <= ma ; ::_thesis: contradiction
then ma = len B by A4, A1, A16, XXREAL_0:1;
then cy in B . ma by A59;
hence contradiction by A57; ::_thesis: verum
end;
hence ( ma < n & cy in B . n ) by A59; ::_thesis: verum
end;
consider mm being Nat such that
A60: ( S2[mm] & ( for n being Nat st S2[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 (FinS (F,D)) 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__::_thesis:_(_(_ma_=_1m_&_contradiction_)_or_(_ma_<>_1m_&_contradiction_)_)
percases ( ma = 1m or ma <> 1m ) ;
case ma = 1m ; ::_thesis: contradiction
then cy in (B . (1m + 1)) \ (B . 1m) by A57, A60, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A3, A62, A66, Th15;
hence contradiction by A11, A56, A60, A63; ::_thesis: verum
end;
case ma <> 1m ; ::_thesis: contradiction
then A68: ma < 1m by A61, XXREAL_0:1;
now__::_thesis:_not_cy_in_B_._1m
assume cy in B . 1m ; ::_thesis: contradiction
then mm <= 1m by A60, A67, A68;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; ::_thesis: verum
end;
then cy in (B . (1m + 1)) \ (B . 1m) by A60, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A3, A62, A66, Th15;
hence contradiction by A11, A56, A60, A63; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence card (p " {x}) = card ((FinS (F,D)) " {x}) by A4, A1, A30, A16, A33, A36, Def1; ::_thesis: verum
end;
caseA69: mi <> 1 ; ::_thesis: card (p " {x}) = card ((FinS (F,D)) " {x})
then 1 < mi by A14, XXREAL_0:1;
then A70: 1 <= m1 by A15, NAT_1:13;
A71: m1 <= len (FinS (F,D)) 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} :: according to XBOOLE_0:def_10 ::_thesis: p " {x} c= (B . ma) \ (B . m1)
proof
defpred S2[ Element of NAT ] means ( $1 in dom B & mi <= $1 & $1 <= ma implies for c being Element of C st c in (B . $1) \ (B . m1) holds
c in p " {x} );
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (B . ma) \ (B . m1) or y in p " {x} )
A74: B . ma c= C by A4, A1, A2, A11, Lm5;
A75: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A76: S2[n] ; ::_thesis: S2[n + 1]
assume that
A77: n + 1 in dom B and
A78: mi <= n + 1 and
A79: n + 1 <= ma ; ::_thesis: for c being Element of C st c in (B . (n + 1)) \ (B . m1) holds
c in p " {x}
let c be Element of C; ::_thesis: ( c in (B . (n + 1)) \ (B . m1) implies c in p " {x} )
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) ; ::_thesis: c in p " {x}
now__::_thesis:_(_(_n_+_1_=_mi_&_c_in_p_"_{x}_)_or_(_mi_<>_n_+_1_&_c_in_p_"_{x}_)_)
percases ( n + 1 = mi or mi <> n + 1 ) ;
caseA82: n + 1 = mi ; ::_thesis: c in p " {x}
then p . c = (FinS (F,D)) . (n + 1) by A3, A70, A80, A81, Th15;
then p . c in {x} by A13, A82, TARSKI:def_1;
hence c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
case mi <> n + 1 ; ::_thesis: c in p " {x}
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__::_thesis:_(_(_c_in_((B_._(n_+_1))_\_(B_._n))_\_(B_._m1)_&_c_in_p_"_{x}_)_or_(_c_in_(B_._n)_\_(B_._m1)_&_c_in_p_"_{x}_)_)
percases ( c in ((B . (n + 1)) \ (B . n)) \ (B . m1) or c in (B . n) \ (B . m1) ) by A81, A86, XBOOLE_0:def_3;
case c in ((B . (n + 1)) \ (B . n)) \ (B . m1) ; ::_thesis: c in p " {x}
then c in (B . (n + 1)) \ (B . n) by XBOOLE_0:def_5;
then A87: p . c = (FinS (F,D)) . (n + 1) by A3, A80, A84, Th15;
now__::_thesis:_(_(_n_+_1_=_ma_&_c_in_p_"_{x}_)_or_(_n_+_1_<>_ma_&_c_in_p_"_{x}_)_)
percases ( n + 1 = ma or n + 1 <> ma ) ;
case n + 1 = ma ; ::_thesis: c in p " {x}
then p . c in {x} by A11, A87, TARSKI:def_1;
hence c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
case n + 1 <> ma ; ::_thesis: c in p " {x}
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 c in p " {x} by A5, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
case c in (B . n) \ (B . m1) ; ::_thesis: c in p " {x}
hence c in p " {x} by A76, A79, A83, A84, A85, FINSEQ_3:25, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
A89: S2[ 0 ] ;
A90: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A89, A75);
assume A91: y in (B . ma) \ (B . m1) ; ::_thesis: y in p " {x}
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 y in p " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p " {x} or y in (B . ma) \ (B . m1) )
assume A92: y in p " {x} ; ::_thesis: y in (B . ma) \ (B . m1)
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) ; ::_thesis: contradiction
now__::_thesis:_(_(_not_y_in_B_._ma_&_contradiction_)_or_(_y_in_B_._m1_&_contradiction_)_)
percases ( not y in B . ma or y in B . m1 ) by A94, XBOOLE_0:def_5;
caseA95: not y in B . ma ; ::_thesis: contradiction
defpred S2[ Nat] means ( $1 in dom B & ma < $1 & cy in B . $1 );
A96: ex n being Nat st S2[n]
proof
take n = len B; ::_thesis: S2[n]
len B <> 0 by Th4;
then 0 + 1 <= len B by NAT_1:13;
hence n in dom B by FINSEQ_3:25; ::_thesis: ( ma < n & cy in B . n )
A97: B . n = C by Th3;
now__::_thesis:_not_n_<=_ma
assume n <= ma ; ::_thesis: contradiction
then ma = len B by A4, A1, A16, XXREAL_0:1;
then cy in B . ma by A97;
hence contradiction by A95; ::_thesis: verum
end;
hence ( ma < n & cy in B . n ) by A97; ::_thesis: verum
end;
consider mm being Nat such that
A98: ( S2[mm] & ( for n being Nat st S2[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 (FinS (F,D)) 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__::_thesis:_(_(_ma_=_1m_&_contradiction_)_or_(_ma_<>_1m_&_contradiction_)_)
percases ( ma = 1m or ma <> 1m ) ;
case ma = 1m ; ::_thesis: contradiction
then cy in (B . (1m + 1)) \ (B . 1m) by A95, A98, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A3, A100, A104, Th15;
hence contradiction by A11, A93, A98, A101; ::_thesis: verum
end;
case ma <> 1m ; ::_thesis: contradiction
then A106: ma < 1m by A99, XXREAL_0:1;
now__::_thesis:_not_cy_in_B_._1m
assume cy in B . 1m ; ::_thesis: contradiction
then mm <= 1m by A98, A105, A106;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; ::_thesis: verum
end;
then cy in (B . (1m + 1)) \ (B . 1m) by A98, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A3, A100, A104, Th15;
hence contradiction by A11, A93, A98, A101; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
caseA107: y in B . m1 ; ::_thesis: contradiction
defpred S2[ Nat] means ( $1 in dom B & $1 <= m1 & cy in B . $1 );
A108: ex n being Nat st S2[n] by A72, A107;
consider mm being Nat such that
A109: ( S2[mm] & ( for n being Nat st S2[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 (FinS (F,D)) by A4, A1, A109, FINSEQ_3:29;
now__::_thesis:_(_(_mm_=_1_&_contradiction_)_or_(_mm_<>_1_&_contradiction_)_)
percases ( mm = 1 or mm <> 1 ) ;
case mm = 1 ; ::_thesis: contradiction
then p . cy = (FinS (F,D)) . 1 by A3, A109, Th15;
then mi <= 1 by A13, A35, A93;
hence contradiction by A14, A69, XXREAL_0:1; ::_thesis: verum
end;
case mm <> 1 ; ::_thesis: contradiction
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 = (FinS (F,D)) . (1m + 1) by A3, A113, A118, Th15;
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 ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence card (p " {x}) = (card Bma) - (card Bm1) by A73, CARD_2:44
.= ma - (card Bm1) by A4, A1, A30, A16, Def1
.= card ((FinS (F,D)) " {x}) by A4, A1, A33, A70, A71, Def1 ;
::_thesis: verum
end;
end;
end;
hence card ((FinS (F,D)) " {x}) = card (p " {x}) ; ::_thesis: verum
end;
end;
end;
hence card (Coim ((FinS (F,D)),x)) = card (Coim (p,x)) ; ::_thesis: verum
end;
hence Rland (F,B), FinS (F,D) are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem Th18: :: REARRAN1:18
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rland (F,A)),C) = FinS (F,D)
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rland (F,A)),C) = FinS (F,D)
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rland (F,A)),C) = FinS (F,D)
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies FinS ((Rland (F,B)),C) = FinS (F,D) )
assume A1: ( F is total & card C = card D ) ; ::_thesis: FinS ((Rland (F,B)),C) = FinS (F,D)
then A2: Rland (F,B), FinS (F,D) are_fiberwise_equipotent by Th17;
A3: dom (Rland (F,B)) = C by A1, Th13;
then (Rland (F,B)) | C = Rland (F,B) by RELAT_1:68;
hence FinS ((Rland (F,B)),C) = FinS (F,D) by A2, A3, RFUNCT_3:def_13; ::_thesis: verum
end;
theorem Th19: :: REARRAN1:19
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rland (F,A)),C) = Sum (F,D)
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rland (F,A)),C) = Sum (F,D)
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rland (F,A)),C) = Sum (F,D)
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies Sum ((Rland (F,B)),C) = Sum (F,D) )
assume ( F is total & card C = card D ) ; ::_thesis: Sum ((Rland (F,B)),C) = Sum (F,D)
then FinS ((Rland (F,B)),C) = FinS (F,D) by Th18;
hence Sum ((Rland (F,B)),C) = Sum (FinS (F,D)) by RFUNCT_3:def_14
.= Sum (F,D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem :: REARRAN1:20
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( FinS (((Rland (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rland (F,B)) - r),C) = Sum ((F - r),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( FinS (((Rland (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rland (F,B)) - r),C) = Sum ((F - r),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, Th17;
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; ::_thesis: Sum (((Rland (F,B)) - r),C) = Sum ((F - r),D)
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 ;
::_thesis: verum
end;
theorem Th21: :: REARRAN1:21
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rlor (F,A)) = C
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rlor (F,A)) = C
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
dom (Rlor (F,A)) = C
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies dom (Rlor (F,B)) = C )
set b = Co_Gen B;
A1: ( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) = min ((len (MIM (FinS (F,D)))),(len (CHI ((Co_Gen B),C)))) ) by RFUNCT_3:def_6, RFUNCT_3:def_7;
assume ( F is total & card C = card D ) ; ::_thesis: dom (Rlor (F,B)) = C
then A2: ( len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) & len (Co_Gen B) = card D ) by Th1, Th12;
thus dom (Rlor (F,B)) c= C ; :: according to XBOOLE_0:def_10 ::_thesis: C c= dom (Rlor (F,B))
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in dom (Rlor (F,B)) )
assume x in C ; ::_thesis: x in dom (Rlor (F,B))
then reconsider c = x as Element of C ;
c is_common_for_dom (MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C)) by RFUNCT_3:32;
hence x in dom (Rlor (F,B)) by A1, A2, RFUNCT_3:28; ::_thesis: verum
end;
theorem Th22: :: REARRAN1:22
for C, D being non empty finite set
for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT 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, D be non empty finite set ; ::_thesis: for c being Element of C
for F being PartFunc of D,REAL
for A being 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 being Element of NAT 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) ) )
let c be Element of C; ::_thesis: for F being PartFunc of D,REAL
for A being 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 being Element of NAT 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) ) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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 being Element of NAT 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) ) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( ( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) ) ) )
set fd = FinS (F,D);
set mf = MIM (FinS (F,D));
set b = Co_Gen B;
set h = CHI ((Co_Gen B),C);
A1: (Rlor (F,B)) . c = Sum (((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) # c) by RFUNCT_3:32, RFUNCT_3:33;
A2: ( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def_2, RFUNCT_3:def_6;
assume A3: ( F is total & card C = card D ) ; ::_thesis: ( ( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 ) & ( for n being Element of NAT st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) ) )
then A4: len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) by Th12;
thus ( c in (Co_Gen B) . 1 implies (Rlor (F,B)) . c = (FinS (F,D)) . 1 ) ::_thesis: for n being Element of NAT st 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) holds
(Rlor (F,B)) . c = (FinS (F,D)) . (n + 1)
proof
assume c in (Co_Gen B) . 1 ; ::_thesis: (Rlor (F,B)) . c = (FinS (F,D)) . 1
hence (Rlor (F,B)) . c = Sum (MIM (FinS (F,D))) by A3, A1, Th14
.= (FinS (F,D)) . 1 by A4, A2, Th4, RFINSEQ:16 ;
::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len (Co_Gen B) & c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) implies (Rlor (F,B)) . c = (FinS (F,D)) . (n + 1) )
set mfn = MIM ((FinS (F,D)) /^ n);
assume that
A5: 1 <= n and
A6: n < len (Co_Gen B) and
A7: c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) ; ::_thesis: (Rlor (F,B)) . c = (FinS (F,D)) . (n + 1)
((MIM (FinS (F,D))) (#) (CHI ((Co_Gen B),C))) # c = (n |-> 0) ^ (MIM ((FinS (F,D)) /^ n)) by A3, A5, A6, A7, Th14;
hence (Rlor (F,B)) . c = (Sum (n |-> 0)) + (Sum (MIM ((FinS (F,D)) /^ n))) by A1, RVSUM_1:75
.= 0 + (Sum (MIM ((FinS (F,D)) /^ n))) by RVSUM_1:81
.= (FinS (F,D)) . (n + 1) by A4, A2, A6, RFINSEQ:17 ;
::_thesis: verum
end;
theorem Th23: :: REARRAN1:23
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rlor (F,A)) = rng (FinS (F,D))
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rlor (F,A)) = rng (FinS (F,D))
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
rng (Rlor (F,A)) = rng (FinS (F,D))
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies rng (Rlor (F,B)) = rng (FinS (F,D)) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: rng (Rlor (F,B)) = rng (FinS (F,D))
set fd = FinS (F,D);
set p = Rlor (F,B);
set mf = MIM (FinS (F,D));
set b = Co_Gen B;
set h = CHI ((Co_Gen B),C);
A3: len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) by A1, A2, Th12;
dom F is finite ;
then reconsider F9 = F as finite Function by FINSET_1:10;
A4: dom (FinS (F,D)) = Seg (len (FinS (F,D))) by FINSEQ_1:def_3;
A5: dom (Rlor (F,B)) = C by A1, A2, Th21;
A6: dom (Co_Gen B) = Seg (len (Co_Gen B)) by FINSEQ_1:def_3;
reconsider dfd = dom (FinS (F,D)), dF = dom F9 as finite set ;
A7: ( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) 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 FinS (F,D),F are_fiberwise_equipotent by A8, RFUNCT_3:def_13;
then card dfd = card dF by CLASSES1:81;
then len (FinS (F,D)) <> 0 by A8, A4;
then A9: 0 + 1 <= len (FinS (F,D)) by NAT_1:13;
then A10: 1 in dom (FinS (F,D)) by FINSEQ_3:25;
thus rng (Rlor (F,B)) c= rng (FinS (F,D)) :: according to XBOOLE_0:def_10 ::_thesis: rng (FinS (F,D)) c= rng (Rlor (F,B))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (Rlor (F,B)) or x in rng (FinS (F,D)) )
assume x in rng (Rlor (F,B)) ; ::_thesis: x in rng (FinS (F,D))
then consider c being Element of C such that
c in dom (Rlor (F,B)) and
A11: (Rlor (F,B)) . c = x by PARTFUN1:3;
defpred S1[ set ] means ( $1 in dom (Co_Gen B) & c in (Co_Gen B) . $1 );
A12: ex n being Nat st S1[n]
proof
take n = len (Co_Gen B); ::_thesis: S1[n]
(Co_Gen B) . n = C by Th3;
hence S1[n] by A3, A7, A9, FINSEQ_3:25; ::_thesis: verum
end;
consider mi being Nat such that
A13: ( S1[mi] & ( for n being Nat st S1[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 (Co_Gen B) by A13, FINSEQ_3:25;
now__::_thesis:_(_(_mi_=_1_&_x_in_rng_(FinS_(F,D))_)_or_(_mi_<>_1_&_x_in_rng_(FinS_(F,D))_)_)
percases ( mi = 1 or mi <> 1 ) ;
case mi = 1 ; ::_thesis: x in rng (FinS (F,D))
then (Rlor (F,B)) . c = (FinS (F,D)) . 1 by A1, A2, A13, Th22;
hence x in rng (FinS (F,D)) by A10, A11, FUNCT_1:def_3; ::_thesis: verum
end;
case mi <> 1 ; ::_thesis: x in rng (FinS (F,D))
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 (Co_Gen B) by A15, XXREAL_0:2;
then m1 in dom (Co_Gen B) by A16, FINSEQ_3:25;
then not c in (Co_Gen B) . m1 by A13, XREAL_1:44;
then A18: c in ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) by A13, XBOOLE_0:def_5;
m1 < len (Co_Gen B) by A15, A17, XXREAL_0:2;
then (Rlor (F,B)) . c = (FinS (F,D)) . (m1 + 1) by A1, A2, A16, A18, Th22;
hence x in rng (FinS (F,D)) by A3, A7, A4, A6, A11, A13, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence x in rng (FinS (F,D)) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (FinS (F,D)) or x in rng (Rlor (F,B)) )
defpred S1[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
assume x in rng (FinS (F,D)) ; ::_thesis: x in rng (Rlor (F,B))
then A19: ex n being Nat st S1[n] by FINSEQ_2:10;
consider mi being Nat such that
A20: ( S1[mi] & ( for n being Nat st S1[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 (FinS (F,D)) by A20, FINSEQ_3:25;
now__::_thesis:_(_(_mi_=_1_&_x_in_rng_(Rlor_(F,B))_)_or_(_mi_<>_1_&_x_in_rng_(Rlor_(F,B))_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA23: mi = 1 ; ::_thesis: x in rng (Rlor (F,B))
set y = the Element of (Co_Gen B) . 1;
A24: (Co_Gen B) . 1 <> {} by A3, A7, A4, A6, A10, Th7;
(Co_Gen B) . 1 c= C by A3, A7, A4, A6, A10, Lm5;
then reconsider y = the Element of (Co_Gen B) . 1 as Element of C by A24, TARSKI:def_3;
(Rlor (F,B)) . y = (FinS (F,D)) . 1 by A1, A2, A24, Th22;
hence x in rng (Rlor (F,B)) by A5, A20, A23, FUNCT_1:def_3; ::_thesis: verum
end;
caseA25: mi <> 1 ; ::_thesis: x in rng (Rlor (F,B))
set y = the Element of ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen 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 (FinS (F,D)) by A20, FINSEQ_3:25;
then m1 <= (len (FinS (F,D))) - 1 by XREAL_1:19;
then A27: ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) <> {} by A3, A7, A26, Th8;
then A28: the Element of ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) in (Co_Gen B) . (m1 + 1) by XBOOLE_0:def_5;
(Co_Gen B) . mi c= C by A3, A7, A4, A6, A20, Lm5;
then reconsider y = the Element of ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen B) . m1) as Element of C by A28;
m1 < mi by XREAL_1:44;
then m1 < len (FinS (F,D)) by A22, XXREAL_0:2;
then (Rlor (F,B)) . y = (FinS (F,D)) . (m1 + 1) by A1, A2, A3, A7, A26, A27, Th22;
hence x in rng (Rlor (F,B)) by A5, A20, FUNCT_1:def_3; ::_thesis: verum
end;
end;
end;
hence x in rng (Rlor (F,B)) ; ::_thesis: verum
end;
theorem Th24: :: REARRAN1:24
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Rlor (F,A), FinS (F,D) are_fiberwise_equipotent
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Rlor (F,A), FinS (F,D) are_fiberwise_equipotent
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Rlor (F,A), FinS (F,D) are_fiberwise_equipotent
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies Rlor (F,B), FinS (F,D) are_fiberwise_equipotent )
set fd = FinS (F,D);
set p = Rlor (F,B);
set mf = MIM (FinS (F,D));
set b = Co_Gen B;
set h = CHI ((Co_Gen B),C);
A1: ( len (CHI ((Co_Gen B),C)) = len (Co_Gen B) & len (MIM (FinS (F,D))) = len (FinS (F,D)) ) by RFINSEQ:def_2, RFUNCT_3:def_6;
assume A2: ( F is total & card C = card D ) ; ::_thesis: Rlor (F,B), FinS (F,D) are_fiberwise_equipotent
then A3: rng (Rlor (F,B)) = rng (FinS (F,D)) by Th23;
A4: dom (Rlor (F,B)) = C by A2, Th21;
then reconsider p = Rlor (F,B) as finite PartFunc of C,REAL by FINSET_1:10;
A5: len (MIM (FinS (F,D))) = len (CHI ((Co_Gen B),C)) by A2, Th12;
A6: ( dom (FinS (F,D)) = Seg (len (FinS (F,D))) & dom (Co_Gen B) = Seg (len (Co_Gen B)) ) by FINSEQ_1:def_3;
now__::_thesis:_for_x_being_set_holds_card_(Coim_((FinS_(F,D)),x))_=_card_(Coim_(p,x))
let x be set ; ::_thesis: card (Coim ((FinS (F,D)),x)) = card (Coim (p,x))
now__::_thesis:_(_(_not_x_in_rng_(FinS_(F,D))_&_card_((FinS_(F,D))_"_{x})_=_card_(p_"_{x})_)_or_(_x_in_rng_(FinS_(F,D))_&_card_((FinS_(F,D))_"_{x})_=_card_(p_"_{x})_)_)
percases ( not x in rng (FinS (F,D)) or x in rng (FinS (F,D)) ) ;
caseA7: not x in rng (FinS (F,D)) ; ::_thesis: card ((FinS (F,D)) " {x}) = card (p " {x})
then (FinS (F,D)) " {x} = {} by Lm1;
hence card ((FinS (F,D)) " {x}) = card (p " {x}) by A3, A7, Lm1; ::_thesis: verum
end;
caseA8: x in rng (FinS (F,D)) ; ::_thesis: card ((FinS (F,D)) " {x}) = card (p " {x})
defpred S1[ Nat] means ( $1 in dom (FinS (F,D)) & (FinS (F,D)) . $1 = x );
A9: ex n being Nat st S1[n] by A8, FINSEQ_2:10;
consider mi being Nat such that
A10: ( S1[mi] & ( for n being Nat st S1[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 being Nat st S1[n] holds
n <= len (FinS (F,D)) by FINSEQ_3:25;
consider ma being Nat such that
A14: ( S1[ma] & ( for n being Nat st S1[n] holds
n <= ma ) ) from NAT_1:sch_6(A13, A9);
A15: ma <= len (FinS (F,D)) by A14, FINSEQ_3:25;
A16: (Seg ma) \ (Seg m1) = (FinS (F,D)) " {x}
proof
thus (Seg ma) \ (Seg m1) c= (FinS (F,D)) " {x} :: according to XBOOLE_0:def_10 ::_thesis: (FinS (F,D)) " {x} c= (Seg ma) \ (Seg m1)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Seg ma) \ (Seg m1) or y in (FinS (F,D)) " {x} )
assume A17: y in (Seg ma) \ (Seg m1) ; ::_thesis: y in (FinS (F,D)) " {x}
then reconsider l = y as Element of NAT ;
reconsider o = (FinS (F,D)) . 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 (FinS (F,D)) by A15, XXREAL_0:2;
then A21: l in dom (FinS (F,D)) 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__::_thesis:_(_(_l_=_ma_&_y_in_(FinS_(F,D))_"_{x}_)_or_(_l_<>_ma_&_y_in_(FinS_(F,D))_"_{x}_)_)
percases ( l = ma or l <> ma ) ;
case l = ma ; ::_thesis: y in (FinS (F,D)) " {x}
then o in {x} by A14, TARSKI:def_1;
hence y in (FinS (F,D)) " {x} by A21, FUNCT_1:def_7; ::_thesis: verum
end;
case l <> ma ; ::_thesis: y in (FinS (F,D)) " {x}
then l < ma by A20, XXREAL_0:1;
then A23: o >= r by A14, A21, RFINSEQ:19;
now__::_thesis:_(_(_l_=_mi_&_y_in_(FinS_(F,D))_"_{x}_)_or_(_l_<>_mi_&_y_in_(FinS_(F,D))_"_{x}_)_)
percases ( l = mi or l <> mi ) ;
case l = mi ; ::_thesis: y in (FinS (F,D)) " {x}
then o in {x} by A10, TARSKI:def_1;
hence y in (FinS (F,D)) " {x} by A21, FUNCT_1:def_7; ::_thesis: verum
end;
case l <> mi ; ::_thesis: y in (FinS (F,D)) " {x}
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 y in (FinS (F,D)) " {x} by A21, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence y in (FinS (F,D)) " {x} ; ::_thesis: verum
end;
end;
end;
hence y in (FinS (F,D)) " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (FinS (F,D)) " {x} or y in (Seg ma) \ (Seg m1) )
assume A24: y in (FinS (F,D)) " {x} ; ::_thesis: y in (Seg ma) \ (Seg m1)
then A25: y in dom (FinS (F,D)) by FUNCT_1:def_7;
reconsider l = y as Element of NAT by A24;
A26: 1 <= l by A25, FINSEQ_3:25;
(FinS (F,D)) . y in {x} by A24, FUNCT_1:def_7;
then A27: (FinS (F,D)) . 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 y in (Seg ma) \ (Seg m1) by A28, XBOOLE_0:def_5; ::_thesis: verum
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 ((FinS (F,D)) " {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 (FinS (F,D)) by A10, FINSEQ_3:25;
then 1 <= len (FinS (F,D)) by A11, XXREAL_0:2;
then A34: 1 in dom (FinS (F,D)) by FINSEQ_3:25;
now__::_thesis:_(_(_mi_=_1_&_card_(p_"_{x})_=_card_((FinS_(F,D))_"_{x})_)_or_(_mi_<>_1_&_card_(p_"_{x})_=_card_((FinS_(F,D))_"_{x})_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA35: mi = 1 ; ::_thesis: card (p " {x}) = card ((FinS (F,D)) " {x})
(Co_Gen B) . ma = p " {x}
proof
thus (Co_Gen B) . ma c= p " {x} :: according to XBOOLE_0:def_10 ::_thesis: p " {x} c= (Co_Gen B) . ma
proof
defpred S2[ Element of NAT ] means ( $1 in dom (Co_Gen B) & $1 <= ma implies for c being Element of C st c in (Co_Gen B) . $1 holds
c in p " {x} );
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (Co_Gen B) . ma or y in p " {x} )
assume A36: y in (Co_Gen B) . ma ; ::_thesis: y in p " {x}
(Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
then reconsider cy = y as Element of C by A36;
A37: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A38: S2[n] ; ::_thesis: S2[n + 1]
assume that
A39: n + 1 in dom (Co_Gen B) and
A40: n + 1 <= ma ; ::_thesis: for c being Element of C st c in (Co_Gen B) . (n + 1) holds
c in p " {x}
A41: n + 1 <= len (Co_Gen B) by A39, FINSEQ_3:25;
then A42: n <= (len (Co_Gen B)) - 1 by XREAL_1:19;
A43: n < len (Co_Gen B) by A41, NAT_1:13;
let c be Element of C; ::_thesis: ( c in (Co_Gen B) . (n + 1) implies c in p " {x} )
assume A44: c in (Co_Gen B) . (n + 1) ; ::_thesis: c in p " {x}
A45: n <= len (Co_Gen B) by A41, NAT_1:13;
now__::_thesis:_(_(_n_=_0_&_c_in_p_"_{x}_)_or_(_n_<>_0_&_c_in_p_"_{x}_)_)
percases ( n = 0 or n <> 0 ) ;
case n = 0 ; ::_thesis: c in p " {x}
then p . c = x by A2, A10, A35, A44, Th22;
then p . c in {x} by TARSKI:def_1;
hence c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
caseA46: n <> 0 ; ::_thesis: c in p " {x}
then A47: 0 + 1 < n + 1 by XREAL_1:6;
A48: 0 + 1 <= n by A46, NAT_1:13;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A42, Def2;
then A49: (Co_Gen B) . (n + 1) = ((Co_Gen B) . (n + 1)) \/ ((Co_Gen B) . n) by XBOOLE_1:12
.= (((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \/ ((Co_Gen B) . n) by XBOOLE_1:39 ;
now__::_thesis:_(_(_c_in_((Co_Gen_B)_._(n_+_1))_\_((Co_Gen_B)_._n)_&_c_in_p_"_{x}_)_or_(_c_in_(Co_Gen_B)_._n_&_c_in_p_"_{x}_)_)
percases ( c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) or c in (Co_Gen B) . n ) by A44, A49, XBOOLE_0:def_3;
case c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) ; ::_thesis: c in p " {x}
then A50: p . c = (FinS (F,D)) . (n + 1) by A2, A43, A48, Th22;
now__::_thesis:_(_(_n_+_1_=_ma_&_c_in_p_"_{x}_)_or_(_n_+_1_<>_ma_&_c_in_p_"_{x}_)_)
percases ( n + 1 = ma or n + 1 <> ma ) ;
case n + 1 = ma ; ::_thesis: c in p " {x}
then p . c in {x} by A14, A50, TARSKI:def_1;
hence c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
case n + 1 <> ma ; ::_thesis: c in p " {x}
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 c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
case c in (Co_Gen B) . n ; ::_thesis: c in p " {x}
hence c in p " {x} by A38, A40, A45, A48, FINSEQ_3:25, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
A52: S2[ 0 ] by FINSEQ_3:25;
A53: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A52, A37);
ma in dom (Co_Gen B) by A5, A1, A14, FINSEQ_3:29;
then cy in p " {x} by A36, A53;
hence y in p " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p " {x} or y in (Co_Gen B) . ma )
assume A54: y in p " {x} ; ::_thesis: y in (Co_Gen B) . ma
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 S2[ Nat] means ( $1 in dom (Co_Gen B) & ma < $1 & cy in (Co_Gen B) . $1 );
assume A56: not y in (Co_Gen B) . ma ; ::_thesis: contradiction
A57: ex n being Nat st S2[n]
proof
take n = len (Co_Gen B); ::_thesis: S2[n]
len (Co_Gen B) <> 0 by Th4;
then 0 + 1 <= len (Co_Gen B) by NAT_1:13;
hence n in dom (Co_Gen B) by FINSEQ_3:25; ::_thesis: ( ma < n & cy in (Co_Gen B) . n )
A58: (Co_Gen B) . n = C by Th3;
now__::_thesis:_not_n_<=_ma
assume n <= ma ; ::_thesis: contradiction
then ma = len (Co_Gen B) by A5, A1, A15, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A58;
hence contradiction by A56; ::_thesis: verum
end;
hence ( ma < n & cy in (Co_Gen B) . n ) by A58; ::_thesis: verum
end;
consider mm being Nat such that
A59: ( S2[mm] & ( for n being Nat st S2[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 (FinS (F,D)) by A5, A1, A59, FINSEQ_3:29;
A63: mm <= len (Co_Gen 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 (Co_Gen B) by A63, XXREAL_0:2;
1m <= mm by A64, XREAL_1:19;
then 1m <= len (Co_Gen B) by A63, XXREAL_0:2;
then A66: 1m in dom (Co_Gen B) by A61, FINSEQ_3:25;
now__::_thesis:_(_(_ma_=_1m_&_contradiction_)_or_(_ma_<>_1m_&_contradiction_)_)
percases ( ma = 1m or ma <> 1m ) ;
case ma = 1m ; ::_thesis: contradiction
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A56, A59, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A2, A61, A65, Th22;
hence contradiction by A14, A55, A59, A62; ::_thesis: verum
end;
case ma <> 1m ; ::_thesis: contradiction
then A67: ma < 1m by A60, XXREAL_0:1;
now__::_thesis:_not_cy_in_(Co_Gen_B)_._1m
assume cy in (Co_Gen B) . 1m ; ::_thesis: contradiction
then mm <= 1m by A59, A66, A67;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; ::_thesis: verum
end;
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A59, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A2, A61, A65, Th22;
hence contradiction by A14, A55, A59, A62; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence card (p " {x}) = card ((FinS (F,D)) " {x}) by A5, A1, A29, A15, A32, A35, Def1; ::_thesis: verum
end;
caseA68: mi <> 1 ; ::_thesis: card (p " {x}) = card ((FinS (F,D)) " {x})
then 1 < mi by A11, XXREAL_0:1;
then A69: 1 <= m1 by A12, NAT_1:13;
A70: m1 <= len (FinS (F,D)) by A33, A12, NAT_1:13;
then A71: m1 in dom (Co_Gen B) by A5, A1, A69, FINSEQ_3:25;
then A72: (Co_Gen B) . m1 c= (Co_Gen B) . ma by A5, A1, A6, A14, A31, Th2;
(Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
then reconsider bma = (Co_Gen B) . ma, bm1 = (Co_Gen B) . m1 as finite set by A72;
((Co_Gen B) . ma) \ ((Co_Gen B) . m1) = p " {x}
proof
thus ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) c= p " {x} :: according to XBOOLE_0:def_10 ::_thesis: p " {x} c= ((Co_Gen B) . ma) \ ((Co_Gen B) . m1)
proof
defpred S2[ Element of NAT ] means ( $1 in dom (Co_Gen B) & mi <= $1 & $1 <= ma implies for c being Element of C st c in ((Co_Gen B) . $1) \ ((Co_Gen B) . m1) holds
c in p " {x} );
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) or y in p " {x} )
A73: (Co_Gen B) . ma c= C by A5, A1, A6, A14, Lm5;
A74: for n being Element of NAT st S2[n] holds
S2[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S2[n] implies S2[n + 1] )
assume A75: S2[n] ; ::_thesis: S2[n + 1]
assume that
A76: n + 1 in dom (Co_Gen B) and
A77: mi <= n + 1 and
A78: n + 1 <= ma ; ::_thesis: for c being Element of C st c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) holds
c in p " {x}
let c be Element of C; ::_thesis: ( c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) implies c in p " {x} )
n + 1 <= len (Co_Gen B) by A76, FINSEQ_3:25;
then A79: n < len (Co_Gen B) by NAT_1:13;
assume A80: c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) ; ::_thesis: c in p " {x}
now__::_thesis:_(_(_n_+_1_=_mi_&_c_in_p_"_{x}_)_or_(_mi_<>_n_+_1_&_c_in_p_"_{x}_)_)
percases ( n + 1 = mi or mi <> n + 1 ) ;
caseA81: n + 1 = mi ; ::_thesis: c in p " {x}
then p . c = (FinS (F,D)) . (n + 1) by A2, A69, A79, A80, Th22;
then p . c in {x} by A10, A81, TARSKI:def_1;
hence c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
case mi <> n + 1 ; ::_thesis: c in p " {x}
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 (Co_Gen B) by A5, A1, A15, XXREAL_0:2;
then ( n <= n + 1 & n in dom (Co_Gen B) ) by A83, FINSEQ_3:25, NAT_1:11;
then (Co_Gen B) . n c= (Co_Gen B) . (n + 1) by A76, Th2;
then A85: ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . m1) = (((Co_Gen B) . (n + 1)) \/ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) by XBOOLE_1:12
.= ((((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \/ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) by XBOOLE_1:39
.= ((((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1)) \/ (((Co_Gen B) . n) \ ((Co_Gen B) . m1)) by XBOOLE_1:42 ;
now__::_thesis:_(_(_c_in_(((Co_Gen_B)_._(n_+_1))_\_((Co_Gen_B)_._n))_\_((Co_Gen_B)_._m1)_&_c_in_p_"_{x}_)_or_(_c_in_((Co_Gen_B)_._n)_\_((Co_Gen_B)_._m1)_&_c_in_p_"_{x}_)_)
percases ( c in (((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) or c in ((Co_Gen B) . n) \ ((Co_Gen B) . m1) ) by A80, A85, XBOOLE_0:def_3;
case c in (((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n)) \ ((Co_Gen B) . m1) ; ::_thesis: c in p " {x}
then c in ((Co_Gen B) . (n + 1)) \ ((Co_Gen B) . n) by XBOOLE_0:def_5;
then A86: p . c = (FinS (F,D)) . (n + 1) by A2, A79, A83, Th22;
now__::_thesis:_(_(_n_+_1_=_ma_&_c_in_p_"_{x}_)_or_(_n_+_1_<>_ma_&_c_in_p_"_{x}_)_)
percases ( n + 1 = ma or n + 1 <> ma ) ;
case n + 1 = ma ; ::_thesis: c in p " {x}
then p . c in {x} by A14, A86, TARSKI:def_1;
hence c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
case n + 1 <> ma ; ::_thesis: c in p " {x}
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 c in p " {x} by A4, FUNCT_1:def_7; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
case c in ((Co_Gen B) . n) \ ((Co_Gen B) . m1) ; ::_thesis: c in p " {x}
hence c in p " {x} by A75, A78, A82, A83, A84, FINSEQ_3:25, NAT_1:13; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
end;
end;
hence c in p " {x} ; ::_thesis: verum
end;
A88: S2[ 0 ] ;
A89: for n being Element of NAT holds S2[n] from NAT_1:sch_1(A88, A74);
assume A90: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; ::_thesis: y in p " {x}
then y in (Co_Gen B) . ma ;
then reconsider cy = y as Element of C by A73;
ma in dom (Co_Gen B) by A5, A1, A14, FINSEQ_3:29;
then cy in p " {x} by A30, A90, A89;
hence y in p " {x} ; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in p " {x} or y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) )
assume A91: y in p " {x} ; ::_thesis: y in ((Co_Gen B) . ma) \ ((Co_Gen B) . m1)
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 ((Co_Gen B) . ma) \ ((Co_Gen B) . m1) ; ::_thesis: contradiction
now__::_thesis:_(_(_not_y_in_(Co_Gen_B)_._ma_&_contradiction_)_or_(_y_in_(Co_Gen_B)_._m1_&_contradiction_)_)
percases ( not y in (Co_Gen B) . ma or y in (Co_Gen B) . m1 ) by A93, XBOOLE_0:def_5;
caseA94: not y in (Co_Gen B) . ma ; ::_thesis: contradiction
defpred S2[ Nat] means ( $1 in dom (Co_Gen B) & ma < $1 & cy in (Co_Gen B) . $1 );
A95: ex n being Nat st S2[n]
proof
take n = len (Co_Gen B); ::_thesis: S2[n]
len (Co_Gen B) <> 0 by Th4;
then 0 + 1 <= len (Co_Gen B) by NAT_1:13;
hence n in dom (Co_Gen B) by FINSEQ_3:25; ::_thesis: ( ma < n & cy in (Co_Gen B) . n )
A96: (Co_Gen B) . n = C by Th3;
now__::_thesis:_not_n_<=_ma
assume n <= ma ; ::_thesis: contradiction
then ma = len (Co_Gen B) by A5, A1, A15, XXREAL_0:1;
then cy in (Co_Gen B) . ma by A96;
hence contradiction by A94; ::_thesis: verum
end;
hence ( ma < n & cy in (Co_Gen B) . n ) by A96; ::_thesis: verum
end;
consider mm being Nat such that
A97: ( S2[mm] & ( for n being Nat st S2[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 (FinS (F,D)) by A5, A1, A97, FINSEQ_3:29;
A101: mm <= len (Co_Gen 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 (Co_Gen B) by A101, XXREAL_0:2;
1m <= mm by A102, XREAL_1:19;
then 1m <= len (Co_Gen B) by A101, XXREAL_0:2;
then A104: 1m in dom (Co_Gen B) by A99, FINSEQ_3:25;
now__::_thesis:_(_(_ma_=_1m_&_contradiction_)_or_(_ma_<>_1m_&_contradiction_)_)
percases ( ma = 1m or ma <> 1m ) ;
case ma = 1m ; ::_thesis: contradiction
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A94, A97, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A2, A99, A103, Th22;
hence contradiction by A14, A92, A97, A100; ::_thesis: verum
end;
case ma <> 1m ; ::_thesis: contradiction
then A105: ma < 1m by A98, XXREAL_0:1;
now__::_thesis:_not_cy_in_(Co_Gen_B)_._1m
assume cy in (Co_Gen B) . 1m ; ::_thesis: contradiction
then mm <= 1m by A97, A104, A105;
then mm - 1m <= 0 by XREAL_1:47;
hence contradiction ; ::_thesis: verum
end;
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A97, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . mm by A2, A99, A103, Th22;
hence contradiction by A14, A92, A97, A100; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
caseA106: y in (Co_Gen B) . m1 ; ::_thesis: contradiction
defpred S2[ Nat] means ( $1 in dom (Co_Gen B) & $1 <= m1 & cy in (Co_Gen B) . $1 );
A107: ex n being Nat st S2[n] by A71, A106;
consider mm being Nat such that
A108: ( S2[mm] & ( for n being Nat st S2[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 (Co_Gen B) by A108, FINSEQ_3:25;
A111: mm in dom (FinS (F,D)) by A5, A1, A108, FINSEQ_3:29;
now__::_thesis:_(_(_mm_=_1_&_contradiction_)_or_(_mm_<>_1_&_contradiction_)_)
percases ( mm = 1 or mm <> 1 ) ;
case mm = 1 ; ::_thesis: contradiction
then p . cy = (FinS (F,D)) . 1 by A2, A108, Th22;
then mi <= 1 by A10, A34, A92;
hence contradiction by A11, A68, XXREAL_0:1; ::_thesis: verum
end;
case mm <> 1 ; ::_thesis: contradiction
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 (Co_Gen B) by A110, XXREAL_0:2;
then A115: 1m in dom (Co_Gen B) by A112, FINSEQ_3:25;
A116: 1m < mm by A113, XREAL_1:19;
then A117: 1m < len (Co_Gen B) by A110, XXREAL_0:2;
1m <= m1 by A108, A114, XXREAL_0:2;
then not cy in (Co_Gen B) . 1m by A108, A116, A115;
then cy in ((Co_Gen B) . (1m + 1)) \ ((Co_Gen B) . 1m) by A108, XBOOLE_0:def_5;
then p . cy = (FinS (F,D)) . (1m + 1) by A2, A112, A117, Th22;
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 ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
hence card (p " {x}) = (card bma) - (card bm1) by A72, CARD_2:44
.= ma - (card bm1) by A5, A1, A29, A15, Def1
.= card ((FinS (F,D)) " {x}) by A5, A1, A32, A69, A70, Def1 ;
::_thesis: verum
end;
end;
end;
hence card ((FinS (F,D)) " {x}) = card (p " {x}) ; ::_thesis: verum
end;
end;
end;
hence card (Coim ((FinS (F,D)),x)) = card (Coim (p,x)) ; ::_thesis: verum
end;
hence Rlor (F,B), FinS (F,D) are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum
end;
theorem Th25: :: REARRAN1:25
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rlor (F,A)),C) = FinS (F,D)
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rlor (F,A)),C) = FinS (F,D)
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
FinS ((Rlor (F,A)),C) = FinS (F,D)
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies FinS ((Rlor (F,B)),C) = FinS (F,D) )
assume A1: ( F is total & card C = card D ) ; ::_thesis: FinS ((Rlor (F,B)),C) = FinS (F,D)
then A2: Rlor (F,B), FinS (F,D) are_fiberwise_equipotent by Th24;
A3: dom (Rlor (F,B)) = C by A1, Th21;
then (Rlor (F,B)) | C = Rlor (F,B) by RELAT_1:68;
hence FinS ((Rlor (F,B)),C) = FinS (F,D) by A2, A3, RFUNCT_3:def_13; ::_thesis: verum
end;
theorem Th26: :: REARRAN1:26
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rlor (F,A)),C) = Sum (F,D)
proof
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rlor (F,A)),C) = Sum (F,D)
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card C = card D holds
Sum ((Rlor (F,A)),C) = Sum (F,D)
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies Sum ((Rlor (F,B)),C) = Sum (F,D) )
assume ( F is total & card C = card D ) ; ::_thesis: Sum ((Rlor (F,B)),C) = Sum (F,D)
then FinS ((Rlor (F,B)),C) = FinS (F,D) by Th25;
hence Sum ((Rlor (F,B)),C) = Sum (FinS (F,D)) by RFUNCT_3:def_14
.= Sum (F,D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem :: REARRAN1:27
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( FinS (((Rlor (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( FinS (((Rlor (F,B)) - r),C) = FinS ((F - r),D) & Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),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, Th24;
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; ::_thesis: Sum (((Rlor (F,B)) - r),C) = Sum ((F - r),D)
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 ;
::_thesis: verum
end;
theorem :: REARRAN1:28
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) ) )
assume A1: ( F is total & card C = card D ) ; ::_thesis: ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) )
then A2: ( Sum ((Rland (F,B)),C) = Sum (F,D) & Rlor (F,B), FinS (F,D) are_fiberwise_equipotent ) by Th19, Th24;
( Rland (F,B), FinS (F,D) are_fiberwise_equipotent & FinS ((Rland (F,B)),C) = FinS (F,D) ) by A1, Th17, Th18;
hence ( Rlor (F,B), Rland (F,B) are_fiberwise_equipotent & FinS ((Rlor (F,B)),C) = FinS ((Rland (F,B)),C) & Sum ((Rlor (F,B)),C) = Sum ((Rland (F,B)),C) ) by A1, A2, Th25, Th26, CLASSES1:76; ::_thesis: verum
end;
theorem :: REARRAN1:29
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( max+ ((Rland (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rland (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rland (F,B)) - r)),C) = Sum ((max+ (F - r)),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( max+ ((Rland (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rland (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rland (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
set mp = max+ ((Rland (F,B)) - r);
set 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, Th17;
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: max+ ((Rland (F,B)) - r), max+ (F - r) are_fiberwise_equipotent by RFUNCT_3:41; ::_thesis: ( FinS ((max+ ((Rland (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rland (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
A6: dom (max+ ((Rland (F,B)) - r)) = dom ((Rland (F,B)) - r) by RFUNCT_3:def_10;
then (max+ ((Rland (F,B)) - r)) | C = max+ ((Rland (F,B)) - r) by RELAT_1:68;
then FinS ((max+ ((Rland (F,B)) - r)),C), max+ ((Rland (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def_13;
then A7: FinS ((max+ ((Rland (F,B)) - r)),C), max+ (F - r) are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (max+ (F - r)) = dom (F - r) by RFUNCT_3:def_10;
then (max+ (F - r)) | D = max+ (F - r) by RELAT_1:68;
hence FinS ((max+ ((Rland (F,B)) - r)),C) = FinS ((max+ (F - r)),D) by A8, A7, RFUNCT_3:def_13; ::_thesis: Sum ((max+ ((Rland (F,B)) - r)),C) = Sum ((max+ (F - r)),D)
hence Sum ((max+ ((Rland (F,B)) - r)),C) = Sum (FinS ((max+ (F - r)),D)) by RFUNCT_3:def_14
.= Sum ((max+ (F - r)),D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem :: REARRAN1:30
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( max- ((Rland (F,B)) - r), max- (F - r) are_fiberwise_equipotent & FinS ((max- ((Rland (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rland (F,B)) - r)),C) = Sum ((max- (F - r)),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( max- ((Rland (F,B)) - r), max- (F - r) are_fiberwise_equipotent & FinS ((max- ((Rland (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rland (F,B)) - r)),C) = Sum ((max- (F - r)),D) )
set mp = max- ((Rland (F,B)) - r);
set 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, Th17;
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: max- ((Rland (F,B)) - r), max- (F - r) are_fiberwise_equipotent by RFUNCT_3:42; ::_thesis: ( FinS ((max- ((Rland (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rland (F,B)) - r)),C) = Sum ((max- (F - r)),D) )
A6: dom (max- ((Rland (F,B)) - r)) = dom ((Rland (F,B)) - r) by RFUNCT_3:def_11;
then (max- ((Rland (F,B)) - r)) | C = max- ((Rland (F,B)) - r) by RELAT_1:68;
then FinS ((max- ((Rland (F,B)) - r)),C), max- ((Rland (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def_13;
then A7: FinS ((max- ((Rland (F,B)) - r)),C), max- (F - r) are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (max- (F - r)) = dom (F - r) by RFUNCT_3:def_11;
then (max- (F - r)) | D = max- (F - r) by RELAT_1:68;
hence FinS ((max- ((Rland (F,B)) - r)),C) = FinS ((max- (F - r)),D) by A8, A7, RFUNCT_3:def_13; ::_thesis: Sum ((max- ((Rland (F,B)) - r)),C) = Sum ((max- (F - r)),D)
hence Sum ((max- ((Rland (F,B)) - r)),C) = Sum (FinS ((max- (F - r)),D)) by RFUNCT_3:def_14
.= Sum ((max- (F - r)),D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem Th31: :: REARRAN1:31
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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)) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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)) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C implies ( len (FinS ((Rland (F,B)),C)) = card C & 1 <= len (FinS ((Rland (F,B)),C)) ) )
set p = Rland (F,B);
assume ( F is total & card D = card C ) ; ::_thesis: ( len (FinS ((Rland (F,B)),C)) = card C & 1 <= len (FinS ((Rland (F,B)),C)) )
then A1: dom (Rland (F,B)) = C by Th13;
then A2: (Rland (F,B)) | C = Rland (F,B) by RELAT_1:68;
hence len (FinS ((Rland (F,B)),C)) = card C by A1, RFUNCT_3:67; ::_thesis: 1 <= len (FinS ((Rland (F,B)),C))
0 + 1 <= card C by NAT_1:13;
hence 1 <= len (FinS ((Rland (F,B)),C)) by A1, A2, RFUNCT_3:67; ::_thesis: verum
end;
theorem :: REARRAN1:32
for n being Element of NAT
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 n be Element of NAT ; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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))
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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))
let F be PartFunc of D,REAL; ::_thesis: for A being 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))
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C & n in dom B implies (FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n)) )
assume that
A1: ( F is total & card D = card C ) and
A2: n in dom B ; ::_thesis: (FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n))
set p = Rland (F,B);
A3: len (FinS ((Rland (F,B)),C)) = card C by A1, Th31;
defpred S1[ Element of 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 ((Rland (F,B)),C)) = Seg (len (FinS ((Rland (F,B)),C))) ) by FINSEQ_1:def_3;
A6: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
set f = FinS ((Rland (F,B)),C);
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A7: S1[m] ; ::_thesis: S1[m + 1]
A8: m <= m + 1 by NAT_1:11;
assume A9: m + 1 in dom B ; ::_thesis: (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))
then 1 <= m + 1 by FINSEQ_3:25;
then A10: m + 1 in Seg (m + 1) by FINSEQ_1:1;
A11: dom (Rland (F,B)) = C by A1, Th13;
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 ((FinS ((Rland (F,B)),C)) | (m + 1)) = m + 1 by A4, A3, A12, FINSEQ_1:59;
now__::_thesis:_(_(_m_=_0_&_(FinS_((Rland_(F,B)),C))_|_(m_+_1)_=_FinS_((Rland_(F,B)),(B_._(m_+_1)))_)_or_(_m_<>_0_&_(FinS_((Rland_(F,B)),C))_|_(m_+_1)_=_FinS_((Rland_(F,B)),(B_._(m_+_1)))_)_)
percases ( m = 0 or m <> 0 ) ;
caseA17: m = 0 ; ::_thesis: (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))
consider d being 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 ((Rland (F,B)),C)) by A1, Th31;
then ( 1 in Seg 1 & 1 in dom (FinS ((Rland (F,B)),C)) ) by FINSEQ_1:1, FINSEQ_3:25;
then A21: ((FinS ((Rland (F,B)),C)) | (m + 1)) . 1 = (FinS ((Rland (F,B)),C)) . 1 by A17, RFINSEQ:6
.= (FinS (F,D)) . 1 by A1, Th18
.= (Rland (F,B)) . d by A1, A19, Th15 ;
dom (Rland (F,B)) = C by A1, Th13;
then A22: FinS ((Rland (F,B)),(B . (m + 1))) = <*((Rland (F,B)) . d)*> by A17, A18, RFUNCT_3:69;
len ((FinS ((Rland (F,B)),C)) | (m + 1)) = 1 by A17, A20, FINSEQ_1:59;
hence (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1))) by A22, A21, FINSEQ_1:40; ::_thesis: verum
end;
caseA23: m <> 0 ; ::_thesis: (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1)))
A24: Seg m c= Seg (m + 1) by A8, FINSEQ_1:5;
A25: ((FinS ((Rland (F,B)),C)) | (m + 1)) | m = ((FinS ((Rland (F,B)),C)) | (m + 1)) | (Seg m) by FINSEQ_1:def_15
.= ((FinS ((Rland (F,B)),C)) | (Seg (m + 1))) | (Seg m) by FINSEQ_1:def_15
.= (FinS ((Rland (F,B)),C)) | ((Seg (m + 1)) /\ (Seg m)) by RELAT_1:71
.= (FinS ((Rland (F,B)),C)) | (Seg m) by A24, XBOOLE_1:28
.= (FinS ((Rland (F,B)),C)) | m by FINSEQ_1:def_15 ;
A26: 0 + 1 <= m by A23, NAT_1:13;
then consider d being 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 (Rland (F,B)) . d = (FinS (F,D)) . (m + 1) by A1, A14, A26, A27, Th15
.= (FinS ((Rland (F,B)),C)) . (m + 1) by A1, Th18
.= ((FinS ((Rland (F,B)),C)) | (m + 1)) . (m + 1) by A5, A4, A3, A9, A10, RFINSEQ:6 ;
then A30: (FinS ((Rland (F,B)),C)) | (m + 1) = ((FinS ((Rland (F,B)),C)) | m) ^ <*((Rland (F,B)) . d)*> by A16, A25, RFINSEQ:7;
d in (dom (Rland (F,B))) /\ (B . (m + 1)) by A11, A27, A29, XBOOLE_0:def_4;
then A31: d in dom ((Rland (F,B)) | (B . (m + 1))) by RELAT_1:61;
A32: (FinS ((Rland (F,B)),C)) | (m + 1) is non-increasing by RFINSEQ:20;
A33: dom ((Rland (F,B)) | (B . (m + 1))) = (dom (Rland (F,B))) /\ (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 (FinS ((Rland (F,B)),C)) | (m + 1),(Rland (F,B)) | (B . (m + 1)) are_fiberwise_equipotent by A7, A13, A26, A28, A30, A31, FINSEQ_3:25, RFUNCT_3:65;
hence (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1))) by A33, A32, RFUNCT_3:def_13; ::_thesis: verum
end;
end;
end;
hence (FinS ((Rland (F,B)),C)) | (m + 1) = FinS ((Rland (F,B)),(B . (m + 1))) ; ::_thesis: verum
end;
A34: S1[ 0 ] by FINSEQ_3:25;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A34, A6);
hence (FinS ((Rland (F,B)),C)) | n = FinS ((Rland (F,B)),(B . n)) by A2; ::_thesis: verum
end;
theorem :: REARRAN1:33
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rland ((F - r),A) = (Rland (F,A)) - r
proof
let r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rland ((F - r),A) = (Rland (F,A)) - r
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rland ((F - r),A) = (Rland (F,A)) - r
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card D = card C holds
Rland ((F - r),A) = (Rland (F,A)) - r
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C implies Rland ((F - r),B) = (Rland (F,B)) - r )
assume that
A1: F is total and
A2: card D = card C ; ::_thesis: Rland ((F - r),B) = (Rland (F,B)) - r
A3: dom (Rland (F,B)) = C by A1, A2, Th13;
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;
F | D = F by A4, RELAT_1:68;
then A9: FinS ((F - r),D) = (FinS (F,D)) - ((card D) |-> r) by A4, RFUNCT_3:73;
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(Rland_((F_-_r),B))_holds_
(Rland_((F_-_r),B))_._c_=_((Rland_(F,B))_-_r)_._c
let c be Element of C; ::_thesis: ( c in dom (Rland ((F - r),B)) implies (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c )
assume c in dom (Rland ((F - r),B)) ; ::_thesis: (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c
defpred S1[ 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 being Nat st S1[n] by A11;
consider mi being Nat such that
A15: ( S1[mi] & ( for n being Nat st S1[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__::_thesis:_(_(_mi_=_1_&_(Rland_((F_-_r),B))_._c_=_((Rland_(F,B))_-_r)_._c_)_or_(_mi_<>_1_&_(Rland_((F_-_r),B))_._c_=_((Rland_(F,B))_-_r)_._c_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA21: mi = 1 ; ::_thesis: (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c
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, Th15;
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 ;
::_thesis: verum
end;
case mi <> 1 ; ::_thesis: (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c
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, Th15;
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 ;
::_thesis: verum
end;
end;
end;
hence (Rland ((F - r),B)) . c = ((Rland (F,B)) - r) . c ; ::_thesis: verum
end;
dom ((Rland (F,B)) - r) = C by A3, VALUED_1:3;
hence Rland ((F - r),B) = (Rland (F,B)) - r by A2, A6, A10, Th13, PARTFUN1:5; ::_thesis: verum
end;
theorem :: REARRAN1:34
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( max+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( max+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent & FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
set mp = max+ ((Rlor (F,B)) - r);
set 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, Th24;
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: max+ ((Rlor (F,B)) - r), max+ (F - r) are_fiberwise_equipotent by RFUNCT_3:41; ::_thesis: ( FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) & Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D) )
A6: dom (max+ ((Rlor (F,B)) - r)) = dom ((Rlor (F,B)) - r) by RFUNCT_3:def_10;
then (max+ ((Rlor (F,B)) - r)) | C = max+ ((Rlor (F,B)) - r) by RELAT_1:68;
then FinS ((max+ ((Rlor (F,B)) - r)),C), max+ ((Rlor (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def_13;
then A7: FinS ((max+ ((Rlor (F,B)) - r)),C), max+ (F - r) are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (max+ (F - r)) = dom (F - r) by RFUNCT_3:def_10;
then (max+ (F - r)) | D = max+ (F - r) by RELAT_1:68;
hence FinS ((max+ ((Rlor (F,B)) - r)),C) = FinS ((max+ (F - r)),D) by A8, A7, RFUNCT_3:def_13; ::_thesis: Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum ((max+ (F - r)),D)
hence Sum ((max+ ((Rlor (F,B)) - r)),C) = Sum (FinS ((max+ (F - r)),D)) by RFUNCT_3:def_14
.= Sum ((max+ (F - r)),D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem :: REARRAN1:35
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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) )
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card C = card D implies ( max- ((Rlor (F,B)) - r), max- (F - r) are_fiberwise_equipotent & FinS ((max- ((Rlor (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rlor (F,B)) - r)),C) = Sum ((max- (F - r)),D) ) )
assume that
A1: F is total and
A2: card C = card D ; ::_thesis: ( max- ((Rlor (F,B)) - r), max- (F - r) are_fiberwise_equipotent & FinS ((max- ((Rlor (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rlor (F,B)) - r)),C) = Sum ((max- (F - r)),D) )
set mp = max- ((Rlor (F,B)) - r);
set 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, Th24;
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: max- ((Rlor (F,B)) - r), max- (F - r) are_fiberwise_equipotent by RFUNCT_3:42; ::_thesis: ( FinS ((max- ((Rlor (F,B)) - r)),C) = FinS ((max- (F - r)),D) & Sum ((max- ((Rlor (F,B)) - r)),C) = Sum ((max- (F - r)),D) )
A6: dom (max- ((Rlor (F,B)) - r)) = dom ((Rlor (F,B)) - r) by RFUNCT_3:def_11;
then (max- ((Rlor (F,B)) - r)) | C = max- ((Rlor (F,B)) - r) by RELAT_1:68;
then FinS ((max- ((Rlor (F,B)) - r)),C), max- ((Rlor (F,B)) - r) are_fiberwise_equipotent by A6, RFUNCT_3:def_13;
then A7: FinS ((max- ((Rlor (F,B)) - r)),C), max- (F - r) are_fiberwise_equipotent by A5, CLASSES1:76;
A8: dom (max- (F - r)) = dom (F - r) by RFUNCT_3:def_11;
then (max- (F - r)) | D = max- (F - r) by RELAT_1:68;
hence FinS ((max- ((Rlor (F,B)) - r)),C) = FinS ((max- (F - r)),D) by A8, A7, RFUNCT_3:def_13; ::_thesis: Sum ((max- ((Rlor (F,B)) - r)),C) = Sum ((max- (F - r)),D)
hence Sum ((max- ((Rlor (F,B)) - r)),C) = Sum (FinS ((max- (F - r)),D)) by RFUNCT_3:def_14
.= Sum ((max- (F - r)),D) by RFUNCT_3:def_14 ;
::_thesis: verum
end;
theorem Th36: :: REARRAN1:36
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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)) )
let F be PartFunc of D,REAL; ::_thesis: for A being 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)) )
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C implies ( len (FinS ((Rlor (F,B)),C)) = card C & 1 <= len (FinS ((Rlor (F,B)),C)) ) )
set p = Rlor (F,B);
assume ( F is total & card D = card C ) ; ::_thesis: ( len (FinS ((Rlor (F,B)),C)) = card C & 1 <= len (FinS ((Rlor (F,B)),C)) )
then A1: dom (Rlor (F,B)) = C by Th21;
then A2: (Rlor (F,B)) | C = Rlor (F,B) by RELAT_1:68;
hence len (FinS ((Rlor (F,B)),C)) = card C by A1, RFUNCT_3:67; ::_thesis: 1 <= len (FinS ((Rlor (F,B)),C))
0 + 1 <= card C by NAT_1:13;
hence 1 <= len (FinS ((Rlor (F,B)),C)) by A1, A2, RFUNCT_3:67; ::_thesis: verum
end;
theorem :: REARRAN1:37
for n being Element of NAT
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 n be Element of NAT ; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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))
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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))
let F be PartFunc of D,REAL; ::_thesis: for A being 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))
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C & n in dom B implies (FinS ((Rlor (F,B)),C)) | n = FinS ((Rlor (F,B)),((Co_Gen B) . n)) )
assume that
A1: ( F is total & card D = card C ) and
A2: n in dom B ; ::_thesis: (FinS ((Rlor (F,B)),C)) | n = FinS ((Rlor (F,B)),((Co_Gen B) . n))
set p = Rlor (F,B);
set b = Co_Gen B;
A3: len (FinS ((Rlor (F,B)),C)) = card C by A1, Th36;
defpred S1[ Element of NAT ] means ( $1 in dom (Co_Gen B) implies (FinS ((Rlor (F,B)),C)) | $1 = FinS ((Rlor (F,B)),((Co_Gen B) . $1)) );
A4: dom (Co_Gen B) = Seg (len (Co_Gen B)) by FINSEQ_1:def_3;
A5: len (Co_Gen B) = card C by Th1;
A6: dom (FinS ((Rlor (F,B)),C)) = Seg (len (FinS ((Rlor (F,B)),C))) by FINSEQ_1:def_3;
A7: for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
set f = FinS ((Rlor (F,B)),C);
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A8: S1[m] ; ::_thesis: S1[m + 1]
A9: m <= m + 1 by NAT_1:11;
assume A10: m + 1 in dom (Co_Gen B) ; ::_thesis: (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1)))
then 1 <= m + 1 by FINSEQ_3:25;
then A11: m + 1 in Seg (m + 1) by FINSEQ_1:1;
A12: dom (Rlor (F,B)) = C by A1, Th21;
A13: m + 1 <= len (Co_Gen B) by A10, FINSEQ_3:25;
then A14: m <= len (Co_Gen B) by NAT_1:13;
A15: m < len (Co_Gen B) by A13, NAT_1:13;
A16: m <= (len (Co_Gen B)) - 1 by A13, XREAL_1:19;
A17: len ((FinS ((Rlor (F,B)),C)) | (m + 1)) = m + 1 by A5, A3, A13, FINSEQ_1:59;
now__::_thesis:_(_(_m_=_0_&_(FinS_((Rlor_(F,B)),C))_|_(m_+_1)_=_FinS_((Rlor_(F,B)),((Co_Gen_B)_._(m_+_1)))_)_or_(_m_<>_0_&_(FinS_((Rlor_(F,B)),C))_|_(m_+_1)_=_FinS_((Rlor_(F,B)),((Co_Gen_B)_._(m_+_1)))_)_)
percases ( m = 0 or m <> 0 ) ;
caseA18: m = 0 ; ::_thesis: (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1)))
consider d being Element of C such that
A19: (Co_Gen B) . 1 = {d} by Th9;
A20: d in (Co_Gen B) . 1 by A19, TARSKI:def_1;
A21: 1 <= len (FinS ((Rlor (F,B)),C)) by A1, Th36;
then ( 1 in Seg 1 & 1 in dom (FinS ((Rlor (F,B)),C)) ) by FINSEQ_1:1, FINSEQ_3:25;
then A22: ((FinS ((Rlor (F,B)),C)) | (m + 1)) . 1 = (FinS ((Rlor (F,B)),C)) . 1 by A18, RFINSEQ:6
.= (FinS (F,D)) . 1 by A1, Th25
.= (Rlor (F,B)) . d by A1, A20, Th22 ;
dom (Rlor (F,B)) = C by A1, Th21;
then A23: FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1))) = <*((Rlor (F,B)) . d)*> by A18, A19, RFUNCT_3:69;
len ((FinS ((Rlor (F,B)),C)) | (m + 1)) = 1 by A18, A21, FINSEQ_1:59;
hence (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1))) by A23, A22, FINSEQ_1:40; ::_thesis: verum
end;
caseA24: m <> 0 ; ::_thesis: (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1)))
A25: Seg m c= Seg (m + 1) by A9, FINSEQ_1:5;
A26: ((FinS ((Rlor (F,B)),C)) | (m + 1)) | m = ((FinS ((Rlor (F,B)),C)) | (m + 1)) | (Seg m) by FINSEQ_1:def_15
.= ((FinS ((Rlor (F,B)),C)) | (Seg (m + 1))) | (Seg m) by FINSEQ_1:def_15
.= (FinS ((Rlor (F,B)),C)) | ((Seg (m + 1)) /\ (Seg m)) by RELAT_1:71
.= (FinS ((Rlor (F,B)),C)) | (Seg m) by A25, XBOOLE_1:28
.= (FinS ((Rlor (F,B)),C)) | m by FINSEQ_1:def_15 ;
A27: 0 + 1 <= m by A24, NAT_1:13;
then consider d being Element of C such that
A28: ((Co_Gen B) . (m + 1)) \ ((Co_Gen B) . m) = {d} and
(Co_Gen B) . (m + 1) = ((Co_Gen B) . m) \/ {d} and
A29: ((Co_Gen B) . (m + 1)) \ {d} = (Co_Gen B) . m by A16, Th10;
A30: d in {d} by TARSKI:def_1;
then (Rlor (F,B)) . d = (FinS (F,D)) . (m + 1) by A1, A15, A27, A28, Th22
.= (FinS ((Rlor (F,B)),C)) . (m + 1) by A1, Th25
.= ((FinS ((Rlor (F,B)),C)) | (m + 1)) . (m + 1) by A4, A6, A5, A3, A10, A11, RFINSEQ:6 ;
then A31: (FinS ((Rlor (F,B)),C)) | (m + 1) = ((FinS ((Rlor (F,B)),C)) | m) ^ <*((Rlor (F,B)) . d)*> by A17, A26, RFINSEQ:7;
d in (dom (Rlor (F,B))) /\ ((Co_Gen B) . (m + 1)) by A12, A28, A30, XBOOLE_0:def_4;
then A32: d in dom ((Rlor (F,B)) | ((Co_Gen B) . (m + 1))) by RELAT_1:61;
A33: (FinS ((Rlor (F,B)),C)) | (m + 1) is non-increasing by RFINSEQ:20;
A34: dom ((Rlor (F,B)) | ((Co_Gen B) . (m + 1))) = (dom (Rlor (F,B))) /\ ((Co_Gen B) . (m + 1)) by RELAT_1:61
.= (Co_Gen B) . (m + 1) by A10, A12, Lm5, XBOOLE_1:28 ;
(Co_Gen B) . (m + 1) is finite by A10, Lm5, FINSET_1:1;
then (FinS ((Rlor (F,B)),C)) | (m + 1),(Rlor (F,B)) | ((Co_Gen B) . (m + 1)) are_fiberwise_equipotent by A8, A14, A27, A29, A31, A32, FINSEQ_3:25, RFUNCT_3:65;
hence (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1))) by A34, A33, RFUNCT_3:def_13; ::_thesis: verum
end;
end;
end;
hence (FinS ((Rlor (F,B)),C)) | (m + 1) = FinS ((Rlor (F,B)),((Co_Gen B) . (m + 1))) ; ::_thesis: verum
end;
A35: ( dom B = Seg (len B) & len B = card C ) by Th1, FINSEQ_1:def_3;
A36: S1[ 0 ] by FINSEQ_3:25;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A36, A7);
hence (FinS ((Rlor (F,B)),C)) | n = FinS ((Rlor (F,B)),((Co_Gen B) . n)) by A2, A4, A35, A5; ::_thesis: verum
end;
theorem :: REARRAN1:38
for r being Real
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r
proof
let r be Real; ::_thesis: for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r
let D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being RearrangmentGen of C st F is total & card D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r
let F be PartFunc of D,REAL; ::_thesis: for A being RearrangmentGen of C st F is total & card D = card C holds
Rlor ((F - r),A) = (Rlor (F,A)) - r
let B be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C implies Rlor ((F - r),B) = (Rlor (F,B)) - r )
assume that
A1: F is total and
A2: card D = card C ; ::_thesis: Rlor ((F - r),B) = (Rlor (F,B)) - r
A3: dom (Rlor (F,B)) = C by A1, A2, Th21;
set b = Co_Gen B;
A4: len (Co_Gen 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;
F | D = F by A5, RELAT_1:68;
then A9: FinS ((F - r),D) = (FinS (F,D)) - ((card D) |-> r) by A5, RFUNCT_3:73;
A10: now__::_thesis:_for_c_being_Element_of_C_st_c_in_dom_(Rlor_((F_-_r),B))_holds_
(Rlor_((F_-_r),B))_._c_=_((Rlor_(F,B))_-_r)_._c
let c be Element of C; ::_thesis: ( c in dom (Rlor ((F - r),B)) implies (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c )
assume c in dom (Rlor ((F - r),B)) ; ::_thesis: (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c
defpred S1[ set ] means ( $1 in dom (Co_Gen B) & c in (Co_Gen B) . $1 );
A11: C = (Co_Gen B) . (len (Co_Gen B)) by Th3;
len (Co_Gen B) <> 0 by Th4;
then A12: 0 + 1 <= len (Co_Gen B) by NAT_1:13;
then A13: 1 in dom (Co_Gen B) by FINSEQ_3:25;
len (Co_Gen B) in dom (Co_Gen B) by A12, FINSEQ_3:25;
then A14: ex n being Nat st S1[n] by A11;
consider mi being Nat such that
A15: ( S1[mi] & ( for n being Nat st S1[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 (Co_Gen 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 (Co_Gen B) by A17, XXREAL_0:2;
m1 <= mi by A18, XREAL_1:19;
then A20: m1 <= len (Co_Gen B) by A17, XXREAL_0:2;
now__::_thesis:_(_(_mi_=_1_&_(Rlor_((F_-_r),B))_._c_=_((Rlor_(F,B))_-_r)_._c_)_or_(_mi_<>_1_&_(Rlor_((F_-_r),B))_._c_=_((Rlor_(F,B))_-_r)_._c_)_)
percases ( mi = 1 or mi <> 1 ) ;
caseA21: mi = 1 ; ::_thesis: (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c
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, Th22;
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 ;
::_thesis: verum
end;
case mi <> 1 ; ::_thesis: (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c
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 (Co_Gen B) by A20, FINSEQ_3:25;
then not c in (Co_Gen B) . m1 by A15, XREAL_1:44;
then c in ((Co_Gen B) . (m1 + 1)) \ ((Co_Gen 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, Th22;
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 ;
::_thesis: verum
end;
end;
end;
hence (Rlor ((F - r),B)) . c = ((Rlor (F,B)) - r) . c ; ::_thesis: verum
end;
dom ((Rlor (F,B)) - r) = C by A3, VALUED_1:3;
hence Rlor ((F - r),B) = (Rlor (F,B)) - r by A2, A7, A10, Th21, PARTFUN1:5; ::_thesis: verum
end;
theorem :: REARRAN1:39
for D, C being non empty finite set
for F being PartFunc of D,REAL
for A being 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 D, C be non empty finite set ; ::_thesis: for F being PartFunc of D,REAL
for A being 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 )
let F be PartFunc of D,REAL; ::_thesis: for A being 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 )
let A be RearrangmentGen of C; ::_thesis: ( F is total & card D = card C implies ( 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 ) )
assume that
A1: F is total and
A2: card D = card C ; ::_thesis: ( 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 )
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, Th24;
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, Th17;
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; ::_thesis: ( rng (Rland (F,A)) = rng F & rng (Rlor (F,A)) = rng F )
hence ( rng (Rland (F,A)) = rng F & rng (Rlor (F,A)) = rng F ) by CLASSES1:75; ::_thesis: verum
end;