:: 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;