:: by Yuji Sakai and Jaros{\l}aw Kotowicz

::

:: Received May 22, 1993

:: Copyright (c) 1993-2017 Association of Mizar Users

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 func r (#) F -> Element of PFuncs (D,REAL);

coherence

r (#) F is Element of PFuncs (D,REAL)

end;
let E be real-membered set ;

let F be PartFunc of D,E;

let r be Real;

:: original: (#)

redefine func r (#) F -> Element of PFuncs (D,REAL);

coherence

r (#) F is Element of PFuncs (D,REAL)

proof end;

Lm1: for f being Function

for x being object st not x in rng f holds

f " {x} = {}

proof end;

definition

let IT be FinSequence;

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

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

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 Nat st 1 <= k & k <= len A holds

A . k is finite

proof 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 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 end;

definition

let X be set ;

let IT be FinSequence of X;

end;
let IT be FinSequence of X;

attr IT is lenght_equal_card_of_set means :: REARRAN1:def 3

ex B being finite set st

( B = union X & len IT = card B );

ex B being finite set st

( B = union X & len IT = card B );

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

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 ;

ex b_{1} being FinSequence of bool D st

( b_{1} is terms've_same_card_as_number & b_{1} is ascending & b_{1} is lenght_equal_card_of_set )

end;
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 b

( b

proof 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;
mode RearrangmentGen of D is terms've_same_card_as_number ascending lenght_equal_card_of_set FinSequence of bool D;

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 )

for a being FinSequence of bool D holds

( a is lenght_equal_card_of_set iff len a = card D )

proof end;

theorem Th2: :: REARRAN1:2

for a being FinSequence holds

( a is ascending iff for n, m being Nat st n <= m & n in dom a & m in dom a holds

a . n c= a . m )

( a is ascending iff for n, m being Nat st n <= m & n in dom a & m in dom a holds

a . n c= a . m )

proof 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

for a being terms've_same_card_as_number lenght_equal_card_of_set FinSequence of bool D holds a . (len a) = D

proof 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

for a being lenght_equal_card_of_set FinSequence of bool D holds len a <> 0

proof 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 Nat st n in dom a & m in dom a & n <> m holds

a . n <> a . m

for a being terms've_same_card_as_number ascending FinSequence of bool D

for n, m being Nat st n in dom a & m in dom a & n <> m holds

a . n <> a . m

proof 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 Nat st 1 <= n & n <= (len a) - 1 holds

a . n <> a . (n + 1)

for a being terms've_same_card_as_number ascending FinSequence of bool D

for n being Nat st 1 <= n & n <= (len a) - 1 holds

a . n <> a . (n + 1)

proof end;

Lm5: for n being 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 end;

theorem Th7: :: REARRAN1:7

for n being 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 <> {}

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

theorem Th8: :: REARRAN1:8

for n being 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) <> {}

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 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}

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

theorem Th10: :: REARRAN1:10

for n being 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 )

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

definition

let D be non empty finite set ;

let A be RearrangmentGen of D;

ex b_{1} being RearrangmentGen of D st

for m being Nat st 1 <= m & m <= (len b_{1}) - 1 holds

b_{1} . m = D \ (A . ((len A) - m))

for b_{1}, b_{2} being RearrangmentGen of D st ( for m being Nat st 1 <= m & m <= (len b_{1}) - 1 holds

b_{1} . m = D \ (A . ((len A) - m)) ) & ( for m being Nat st 1 <= m & m <= (len b_{2}) - 1 holds

b_{2} . m = D \ (A . ((len A) - m)) ) holds

b_{1} = b_{2}

for b_{1}, b_{2} being RearrangmentGen of D st ( for m being Nat st 1 <= m & m <= (len b_{1}) - 1 holds

b_{1} . m = D \ (b_{2} . ((len b_{2}) - m)) ) holds

for m being Nat st 1 <= m & m <= (len b_{2}) - 1 holds

b_{2} . m = D \ (b_{1} . ((len b_{1}) - m))

end;
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 for m being Nat st 1 <= m & m <= (len it) - 1 holds

it . m = D \ (A . ((len A) - m));

ex b

for m being Nat st 1 <= m & m <= (len b

b

proof end;

uniqueness for b

b

b

b

proof end;

involutiveness for b

b

for m being Nat st 1 <= m & m <= (len b

b

proof end;

:: deftheorem defines Co_Gen REARRAN1:def 4 :

for D being non empty finite set

for A, b_{3} being RearrangmentGen of D holds

( b_{3} = Co_Gen A iff for m being Nat st 1 <= m & m <= (len b_{3}) - 1 holds

b_{3} . m = D \ (A . ((len A) - m)) );

for D being non empty finite set

for A, b

( b

b

::$CT

theorem Th11: :: REARRAN1:12

for C, D 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))

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

definition

let D, C be non empty finite set ;

let A be RearrangmentGen of C;

let F be PartFunc of D,REAL;

coherence

Sum ((MIM (FinS (F,D))) (#) (CHI (A,C))) is PartFunc of C,REAL;

;

coherence

Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C))) is PartFunc of C,REAL;

;

end;
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 Sum ((MIM (FinS (F,D))) (#) (CHI (A,C)));

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 Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C)));

coherence

Sum ((MIM (FinS (F,D))) (#) (CHI ((Co_Gen A),C))) is PartFunc of C,REAL;

;

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

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

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 Th12: :: REARRAN1:13

for C, D 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

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

theorem Th13: :: 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 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)) ) )

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

theorem Th14: :: 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 Nat st 1 <= n & n < len A & c in (A . (n + 1)) \ (A . n) holds

(Rland (F,A)) . c = (FinS (F,D)) . (n + 1) ) )

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

theorem Th15: :: REARRAN1:16

for C, D 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))

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

theorem Th16: :: REARRAN1:17

for C, D 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

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

theorem Th17: :: REARRAN1:18

for C, D 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)

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

theorem Th18: :: REARRAN1:19

for C, D 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)

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

theorem :: REARRAN1:20

for r being Real

for C, D 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) )

for C, D 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 end;

theorem Th20: :: REARRAN1:21

for C, D 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

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

theorem Th21: :: 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 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) ) )

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

theorem Th22: :: REARRAN1:23

for C, D 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))

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

theorem Th23: :: REARRAN1:24

for C, D 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

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

theorem Th24: :: REARRAN1:25

for C, D 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)

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

theorem Th25: :: REARRAN1:26

for C, D 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)

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

theorem :: REARRAN1:27

for r being Real

for C, D 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) )

for C, D 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 end;

theorem :: REARRAN1:28

for C, D 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) )

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

theorem :: REARRAN1:29

for r being Real

for C, D 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) )

for C, D 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 end;

theorem :: REARRAN1:30

for r being Real

for C, D 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) )

for C, D 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 end;

theorem Th30: :: REARRAN1:31

for C, D 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)) )

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

theorem :: REARRAN1:32

for n being Nat

for C, D 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))

for C, D 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 end;

theorem :: REARRAN1:33

for r being Real

for C, D 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

for C, D 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 end;

theorem :: REARRAN1:34

for r being Real

for C, D 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) )

for C, D 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 end;

theorem :: REARRAN1:35

for r being Real

for C, D 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) )

for C, D 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 end;

theorem Th35: :: REARRAN1:36

for C, D 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)) )

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

theorem :: REARRAN1:37

for n being Nat

for C, D 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))

for C, D 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 end;

theorem :: REARRAN1:38

for r being Real

for C, D 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

for C, D 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 end;

theorem :: REARRAN1:39

for C, D 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 )

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