rearran1.miz



    begin

    reserve n,m,k for Nat,

x,y for set,

r for Real;

    definition

      let D be non empty set, E be real-membered set, F be PartFunc of D, E, r be Real;

      :: original: (#)

      redefine

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

      coherence

      proof

        reconsider F as PartFunc of D, E;

        (r (#) F) is PartFunc of D, REAL ;

        hence thesis by PARTFUN1: 45;

      end;

    end

    

     Lm1: for f be Function, x be object st not x in ( rng f) holds (f " {x}) = {}

    proof

      let f be Function, x be object;

      assume

       A1: not x in ( rng f);

      ( rng f) misses {x}

      proof

        set y = the Element of (( rng f) /\ {x});

        assume (( rng f) /\ {x}) <> {} ;

        then y in ( rng f) & y in {x} by XBOOLE_0:def 4;

        hence contradiction by A1, TARSKI:def 1;

      end;

      hence thesis by RELAT_1: 138;

    end;

    definition

      let IT be FinSequence;

      :: REARRAN1:def1

      attr IT is terms've_same_card_as_number means

      : Def1: for n be Nat st 1 <= n & n <= ( len IT) holds for B be finite set st B = (IT . n) holds ( card B) = n;

      :: REARRAN1:def2

      attr IT is ascending means

      : Def2: for n be Nat st 1 <= n & n <= (( len IT) - 1) holds (IT . n) c= (IT . (n + 1));

    end

    

     Lm2: for D be non empty finite set, A be FinSequence of ( bool D), k be Nat st 1 <= k & k <= ( len A) holds (A . k) is finite

    proof

      let D be non empty finite set, A be FinSequence of ( bool D), k be Nat;

      assume 1 <= k & k <= ( len A);

      then k in ( dom A) by FINSEQ_3: 25;

      then (A . k) in ( bool D) by FINSEQ_2: 11;

      hence thesis;

    end;

    

     Lm3: for D be non empty finite set, A be FinSequence of ( bool D) st ( len A) = ( card D) & A is terms've_same_card_as_number holds for B be finite set st B = (A . ( len A)) holds B = D

    proof

      let D be non empty finite set, A be FinSequence of ( bool D);

      assume that

       A1: ( len A) = ( card D) and

       A2: A is terms've_same_card_as_number;

      

       A3: ( 0 + 1) <= ( len A) by A1, NAT_1: 13;

      then ( len A) in ( dom A) by FINSEQ_3: 25;

      then

       A4: (A . ( len A)) in ( bool D) by FINSEQ_2: 11;

      let B be finite set such that

       A5: B = (A . ( len A));

      assume B <> D;

      then

       A6: B c< D by A5, A4;

      ( card B) = ( card D) by A1, A2, A5, A3;

      hence contradiction by A6, CARD_2: 48;

    end;

    

     Lm4: for D be non empty finite set holds ex B be FinSequence of ( bool D) st ( len B) = ( card D) & B is ascending & B is terms've_same_card_as_number

    proof

      let D be non empty finite set;

      defpred P[ Nat] means for D be non empty finite set st ( card D) = $1 holds ex B be FinSequence of ( bool D) st ( len B) = ( card D) & B is ascending & B is terms've_same_card_as_number;

      

       A1: for n st P[n] holds P[(n + 1)]

      proof

        let n;

        assume

         A2: P[n];

        let D be non empty finite set;

        assume

         A3: ( card D) = (n + 1);

        set x = the Element of D;

        set Y = (D \ {x});

         {x} c= D by ZFMISC_1: 31;

        

        then

         A4: ( card Y) = (( card D) - ( card {x})) by CARD_2: 44

        .= ((n + 1) - 1) by A3, CARD_1: 30

        .= n;

        now

          per cases ;

            case

             A5: n = 0 ;

            set f = <*D*>;

            

             A6: ( len f) = 1 by FINSEQ_1: 39;

            

             A7: ( rng f) = {D} by FINSEQ_1: 39;

            ( rng f) c= ( bool D)

            proof

              let z be object;

              assume z in ( rng f);

              then z = D by A7, TARSKI:def 1;

              hence thesis by ZFMISC_1:def 1;

            end;

            then

            reconsider f as FinSequence of ( bool D) by FINSEQ_1:def 4;

            take f;

            thus ( card D) = ( len f) by A3, A5, FINSEQ_1: 40;

            thus f is ascending by A6, XXREAL_0: 2;

            thus f is terms've_same_card_as_number

            proof

              let m be Nat;

              assume 1 <= m & m <= ( len f);

              then

               A8: m = 1 by A6, XXREAL_0: 1;

              let B be finite set;

              assume B = (f . m);

              hence thesis by A3, A5, A8, FINSEQ_1: 40;

            end;

          end;

            case n <> 0 ;

            then

            reconsider Y as non empty finite set by A4;

            D in ( bool D) by ZFMISC_1:def 1;

            then

             A9: {D} c= ( bool D) by ZFMISC_1: 31;

            consider f be FinSequence of ( bool Y) such that

             A10: ( len f) = ( card Y) and

             A11: f is ascending and

             A12: f is terms've_same_card_as_number by A2, A4;

            set g = (f ^ <*D*>);

            

             A13: ( rng <*D*>) = {D} & ( rng g) = (( rng f) \/ ( rng <*D*>)) by FINSEQ_1: 31, FINSEQ_1: 39;

            ( bool Y) c= ( bool D) by ZFMISC_1: 67;

            then ( rng f) c= ( bool D);

            then ( rng g) c= (( bool D) \/ ( bool D)) by A9, A13, XBOOLE_1: 13;

            then

            reconsider g as FinSequence of ( bool D) by FINSEQ_1:def 4;

            take g;

            

             A14: ( len <*D*>) = 1 by FINSEQ_1: 39;

            then

             A15: ( len g) = (( len f) + 1) by FINSEQ_1: 22;

            thus ( len g) = ( card D) by A3, A4, A10, A14, FINSEQ_1: 22;

            thus g is ascending

            proof

              let m be Nat;

              assume that

               A16: 1 <= m and

               A17: m <= (( len g) - 1);

              m in ( dom f) by A15, A16, A17, FINSEQ_3: 25;

              then

               A18: (g . m) = (f . m) by FINSEQ_1:def 7;

              per cases ;

                suppose

                 A19: m = ( len f);

                then

                reconsider gm = (g . m) as finite set by A16, A18, Lm2;

                gm = Y & (g . (m + 1)) = D by A10, A12, A18, A19, Lm3, FINSEQ_1: 42;

                hence thesis;

              end;

                suppose m <> ( len f);

                then m < ( len f) by A15, A17, XXREAL_0: 1;

                then

                 A20: (m + 1) <= ( len f) by NAT_1: 13;

                1 <= (m + 1) by A16, NAT_1: 13;

                then (m + 1) in ( dom f) by A20, FINSEQ_3: 25;

                then

                 A21: (g . (m + 1)) = (f . (m + 1)) by FINSEQ_1:def 7;

                m <= (( len f) - 1) by A20, XREAL_1: 19;

                hence thesis by A11, A16, A18, A21;

              end;

            end;

            thus g is terms've_same_card_as_number

            proof

              let m be Nat such that

               A22: 1 <= m and

               A23: m <= ( len g);

              let B be finite set such that

               A24: B = (g . m);

              per cases ;

                suppose m = ( len g);

                hence thesis by A3, A4, A10, A15, A24, FINSEQ_1: 42;

              end;

                suppose m <> ( len g);

                then m < ( len g) by A23, XXREAL_0: 1;

                then

                 A25: m <= ( len f) by A15, NAT_1: 13;

                then m in ( dom f) by A22, FINSEQ_3: 25;

                then (g . m) = (f . m) by FINSEQ_1:def 7;

                hence thesis by A12, A22, A24, A25;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A26: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A26, A1);

      hence thesis;

    end;

    definition

      let X be set;

      let IT be FinSequence of X;

      :: REARRAN1:def3

      attr IT is length_equal_card_of_set means ex B be finite set st B = ( union X) & ( len IT) = ( card B);

    end

    registration

      let D be non empty finite set;

      cluster terms've_same_card_as_number ascending length_equal_card_of_set for FinSequence of ( bool D);

      existence

      proof

        consider B be FinSequence of ( bool D) such that

         A1: ( len B) = ( card D) & B is ascending & B is terms've_same_card_as_number by Lm4;

        take B;

        ( union ( bool D)) = D by ZFMISC_1: 81;

        hence thesis by A1;

      end;

    end

    definition

      let D be non empty finite set;

      mode RearrangmentGen of D is terms've_same_card_as_number ascending length_equal_card_of_set FinSequence of ( bool D);

    end

    reserve C,D for non empty finite set,

a for FinSequence of ( bool D);

    theorem :: REARRAN1:1

    

     Th1: for a be FinSequence of ( bool D) holds a is length_equal_card_of_set iff ( len a) = ( card D)

    proof

      let A be FinSequence of ( bool D);

      thus A is length_equal_card_of_set implies ( len A) = ( card D) by ZFMISC_1: 81;

      assume

       A1: ( len A) = ( card D);

      take D;

      thus thesis by A1, ZFMISC_1: 81;

    end;

    theorem :: REARRAN1:2

    

     Th2: for a be FinSequence holds a is ascending iff for n, m st n <= m & n in ( dom a) & m in ( dom a) holds (a . n) c= (a . m)

    proof

      let A be FinSequence;

      thus A is ascending implies for n, m st n <= m & n in ( dom A) & m in ( dom A) holds (A . n) c= (A . m)

      proof

        defpred P[ Nat] means for n st n <= $1 & n in ( dom A) & $1 in ( dom A) holds (A . n) c= (A . $1);

        assume

         A1: A is ascending;

        

         A2: for m st P[m] holds P[(m + 1)]

        proof

          let m;

          assume

           A3: P[m];

          let n;

          assume that

           A4: n <= (m + 1) and

           A5: n in ( dom A) and

           A6: (m + 1) in ( dom A);

          now

            per cases ;

              case n = (m + 1);

              hence thesis;

            end;

              case n <> (m + 1);

              then n < (m + 1) by A4, XXREAL_0: 1;

              then

               A7: n <= m by NAT_1: 13;

              1 <= n by A5, FINSEQ_3: 25;

              then

               A8: 1 <= m by A7, XXREAL_0: 2;

              

               A9: (m + 1) <= ( len A) by A6, FINSEQ_3: 25;

              m <= (m + 1) by NAT_1: 11;

              then m <= ( len A) by A9, XXREAL_0: 2;

              then m in ( dom A) by A8, FINSEQ_3: 25;

              then

               A10: (A . n) c= (A . m) by A3, A5, A7;

              m <= (( len A) - 1) by A9, XREAL_1: 19;

              then (A . m) c= (A . (m + 1)) by A1, A8;

              hence thesis by A10;

            end;

          end;

          hence thesis;

        end;

        let n, m;

        assume

         A11: n <= m & n in ( dom A) & m in ( dom A);

        

         A12: P[ 0 ];

        for m holds P[m] from NAT_1:sch 2( A12, A2);

        hence thesis by A11;

      end;

      assume

       A13: for n, m st n <= m & n in ( dom A) & m in ( dom A) holds (A . n) c= (A . m);

      let n be Nat;

      assume that

       A14: 1 <= n and

       A15: n <= (( len A) - 1);

      

       A16: (n + 1) <= ( len A) by A15, XREAL_1: 19;

      n <= (n + 1) by NAT_1: 11;

      then n <= ( len A) by A16, XXREAL_0: 2;

      then

       A17: n in ( dom A) by A14, FINSEQ_3: 25;

      1 <= (n + 1) by NAT_1: 11;

      then (n + 1) in ( dom A) by A16, FINSEQ_3: 25;

      hence thesis by A13, A17, NAT_1: 11;

    end;

    theorem :: REARRAN1:3

    

     Th3: for a be terms've_same_card_as_number length_equal_card_of_set FinSequence of ( bool D) holds (a . ( len a)) = D

    proof

      let A be terms've_same_card_as_number length_equal_card_of_set FinSequence of ( bool D);

      

       A1: ( len A) = ( card D) by Th1;

      then 1 <= ( len A) by NAT_1: 14;

      then (A . ( len A)) is finite set by Lm2;

      hence thesis by A1, Lm3;

    end;

    theorem :: REARRAN1:4

    

     Th4: for a be length_equal_card_of_set FinSequence of ( bool D) holds ( len a) <> 0

    proof

      let A be length_equal_card_of_set FinSequence of ( bool D);

      assume ( len A) = 0 ;

      then ( card D) = 0 by Th1;

      hence contradiction;

    end;

    theorem :: REARRAN1:5

    

     Th5: for a be ascending terms've_same_card_as_number FinSequence of ( bool D) holds for n, m holds n in ( dom a) & m in ( dom a) & n <> m implies (a . n) <> (a . m)

    proof

      let A be ascending terms've_same_card_as_number FinSequence of ( bool D);

      let n, m;

      assume that

       A1: n in ( dom A) and

       A2: m in ( dom A) and

       A3: n <> m & (A . n) = (A . m);

      

       A4: 1 <= m & m <= ( len A) by A2, FINSEQ_3: 25;

      

       A5: 1 <= n & n <= ( len A) by A1, FINSEQ_3: 25;

      reconsider Am = (A . m) as finite set by A4, Lm2;

      ( card Am) = m by A4, Def1;

      hence contradiction by A3, A5, Def1;

    end;

    theorem :: REARRAN1:6

    for a be ascending terms've_same_card_as_number FinSequence of ( bool D) holds for n holds 1 <= n & n <= (( len a) - 1) implies (a . n) <> (a . (n + 1))

    proof

      let A be ascending terms've_same_card_as_number FinSequence of ( bool D);

      let n;

      assume that

       A1: 1 <= n and

       A2: n <= (( len A) - 1);

      

       A3: (n + 1) <= ( len A) by A2, XREAL_1: 19;

      n <= (n + 1) by NAT_1: 11;

      then n <= ( len A) by A3, XXREAL_0: 2;

      then

       A4: n in ( dom A) by A1, FINSEQ_3: 25;

      1 <= (n + 1) by NAT_1: 11;

      then

       A5: (n + 1) in ( dom A) by A3, FINSEQ_3: 25;

      n <> (n + 1);

      hence thesis by A4, A5, Th5;

    end;

    

     Lm5: n in ( dom a) implies (a . n) c= D

    proof

      assume n in ( dom a);

      then (a . n) in ( bool D) by FINSEQ_2: 11;

      hence thesis;

    end;

    theorem :: REARRAN1:7

    

     Th7: for a be terms've_same_card_as_number FinSequence of ( bool D) st n in ( dom a) holds (a . n) <> {}

    proof

      let A be terms've_same_card_as_number FinSequence of ( bool D);

      assume n in ( dom A);

      then

       A1: 1 <= n & n <= ( len A) by FINSEQ_3: 25;

      assume (A . n) = {} ;

      hence contradiction by A1, Def1, CARD_1: 27;

    end;

    theorem :: REARRAN1:8

    

     Th8: for a be terms've_same_card_as_number FinSequence of ( bool D) st 1 <= n & n <= (( len a) - 1) holds ((a . (n + 1)) \ (a . n)) <> {}

    proof

      let A be terms've_same_card_as_number FinSequence of ( bool D);

      assume that

       A1: 1 <= n and

       A2: n <= (( len A) - 1);

      

       A3: (n + 1) <= ( len A) by A2, XREAL_1: 19;

      n <= (n + 1) by NAT_1: 11;

      then

       A4: n <= ( len A) by A3, XXREAL_0: 2;

      then

      reconsider An1 = (A . (n + 1)), An = (A . n) as finite set by A1, A3, Lm2, NAT_1: 11;

      1 <= (n + 1) by NAT_1: 11;

      then

       A5: ( card An1) = (n + 1) by A3, Def1;

      assume ((A . (n + 1)) \ (A . n)) = {} ;

      then

       A6: (A . (n + 1)) c= (A . n) by XBOOLE_1: 37;

      ( card An) = n by A1, A4, Def1;

      then (n + 1) <= n by A5, A6, NAT_1: 43;

      then 1 <= (n - n) by XREAL_1: 19;

      then 1 <= 0 ;

      hence contradiction;

    end;

    theorem :: REARRAN1:9

    

     Th9: for a be terms've_same_card_as_number length_equal_card_of_set FinSequence of ( bool D) holds ex d be Element of D st (a . 1) = {d}

    proof

      let A be terms've_same_card_as_number length_equal_card_of_set FinSequence of ( bool D);

      ( len A) <> 0 by Th4;

      then

       A1: ( 0 + 1) <= ( len A) by NAT_1: 13;

      then

      reconsider A1 = (A . 1) as finite set by Lm2;

      ( card A1) = 1 by A1, Def1;

      then

      consider x be object such that

       A2: {x} = (A . 1) by CARD_2: 42;

      1 in ( dom A) by A1, FINSEQ_3: 25;

      then (A . 1) c= D by Lm5;

      then

      reconsider x as Element of D by A2, ZFMISC_1: 31;

      take x;

      thus thesis by A2;

    end;

    theorem :: REARRAN1:10

    

     Th10: for a be terms've_same_card_as_number ascending FinSequence of ( bool D) st 1 <= n & n <= (( len a) - 1) holds ex d be Element of D st ((a . (n + 1)) \ (a . n)) = {d} & (a . (n + 1)) = ((a . n) \/ {d}) & ((a . (n + 1)) \ {d}) = (a . n)

    proof

      let A be terms've_same_card_as_number ascending FinSequence of ( bool D);

      assume that

       A1: 1 <= n and

       A2: n <= (( len A) - 1);

      

       A3: (n + 1) <= ( len A) by A2, XREAL_1: 19;

      

       A4: (A . n) c= (A . (n + 1)) by A1, A2, Def2;

      n <= (n + 1) by NAT_1: 11;

      then

       A5: n <= ( len A) by A3, XXREAL_0: 2;

      then

      reconsider An1 = (A . (n + 1)), An = (A . n) as finite set by A1, A3, Lm2, NAT_1: 11;

      

       A6: ( card An) = n by A1, A5, Def1;

      

       A7: 1 <= (n + 1) by NAT_1: 11;

      then ( card An1) = (n + 1) by A3, Def1;

      

      then ( card (An1 \ An)) = ((n + 1) - n) by A4, A6, CARD_2: 44

      .= 1;

      then

      consider x be object such that

       A8: {x} = ((A . (n + 1)) \ (A . n)) by CARD_2: 42;

      x in ((A . (n + 1)) \ (A . n)) by A8, ZFMISC_1: 31;

      then

       A9: not x in (A . n) by XBOOLE_0:def 5;

      

       A10: x in (A . (n + 1)) by A8, ZFMISC_1: 31;

      (n + 1) in ( dom A) by A3, A7, FINSEQ_3: 25;

      then (A . (n + 1)) c= D by Lm5;

      then

      reconsider x as Element of D by A10;

      take x;

      thus {x} = ((A . (n + 1)) \ (A . n)) by A8;

      

      thus ((A . n) \/ {x}) = ((A . (n + 1)) \/ (A . n)) by A8, XBOOLE_1: 39

      .= (A . (n + 1)) by A4, XBOOLE_1: 12;

      

      hence ((A . (n + 1)) \ {x}) = (((A . n) \ {x}) \/ ( {x} \ {x})) by XBOOLE_1: 42

      .= (((A . n) \ {x}) \/ {} ) by XBOOLE_1: 37

      .= (A . n) by A9, ZFMISC_1: 57;

    end;

    definition

      let D be non empty finite set, A be RearrangmentGen of D;

      :: REARRAN1:def4

      func Co_Gen A -> RearrangmentGen of D means for m be Nat st 1 <= m & m <= (( len it ) - 1) holds (it . m) = (D \ (A . (( len A) - m)));

      existence

      proof

        deffunc F( Nat) = (D \ (A . (( len A) - $1)));

        set c = ( card D);

        D c= D;

        then

        reconsider y = D as Subset of D;

        ( 0 + 1) <= c by NAT_1: 13;

        then ( max ( 0 ,(c - 1))) = (c - 1) by FINSEQ_2: 4;

        then

        reconsider c1 = (c - 1) as Element of NAT by FINSEQ_2: 5;

        consider f be FinSequence such that

         A1: ( len f) = c1 and

         A2: for m be Nat st m in ( dom f) holds (f . m) = F(m) from FINSEQ_1:sch 2;

        

         A3: ( dom f) = ( Seg c1) by A1, FINSEQ_1:def 3;

        ( rng f) c= ( bool D)

        proof

          let x be object;

          assume x in ( rng f);

          then

          consider m be Nat such that

           A4: m in ( dom f) & (f . m) = x by FINSEQ_2: 10;

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

          then x is Subset of D by A2, A4;

          hence thesis;

        end;

        then

        reconsider f as FinSequence of ( bool D) by FINSEQ_1:def 4;

        set C = (f ^ <*y*>);

        

         A5: ( len C) = (( len f) + ( len <*y*>)) by FINSEQ_1: 22

        .= (( len f) + 1) by FINSEQ_1: 39;

        

         A6: ( card D) = ( len A) by Th1;

        

         A7: C is terms've_same_card_as_number

        proof

          let m be Nat;

          assume that

           A8: 1 <= m and

           A9: m <= ( len C);

          ( max ( 0 ,(( len C) - m))) = (( len C) - m) by A9, FINSEQ_2: 4;

          then

          reconsider l = (( len C) - m) as Element of NAT by FINSEQ_2: 5;

          let B be finite set such that

           A10: B = (C . m);

          now

            per cases ;

              case m = ( len C);

              hence thesis by A1, A5, A10, FINSEQ_1: 42;

            end;

              case m <> ( len C);

              then m < ( len C) by A9, XXREAL_0: 1;

              then

               A11: (m + 1) <= ( len C) by NAT_1: 13;

              then

               A12: 1 <= l by XREAL_1: 19;

              

               A13: l <= ( len A) by A6, A1, A5, XREAL_1: 43;

              then

               A14: l in ( dom A) by A12, FINSEQ_3: 25;

              then

              reconsider Al = (A . l) as finite set by Lm5, FINSET_1: 1;

              m <= (( len C) - 1) by A11, XREAL_1: 19;

              then

               A15: m in ( dom f) by A5, A8, FINSEQ_3: 25;

              

              then (C . m) = (f . m) by FINSEQ_1:def 7

              .= (D \ (A . l)) by A6, A1, A2, A5, A15;

              

              hence ( card B) = (( card D) - ( card Al)) by A10, A14, Lm5, CARD_2: 44

              .= (( len A) - l) by A6, A12, A13, Def1

              .= m by A6, A1, A5;

            end;

          end;

          hence thesis;

        end;

        for m be Nat st 1 <= m & m <= (( len C) - 1) holds (C . m) c= (C . (m + 1))

        proof

          let m be Nat;

          assume that

           A16: 1 <= m and

           A17: m <= (( len C) - 1);

          

           A18: m in ( dom f) by A5, A16, A17, FINSEQ_3: 25;

          

          then

           A19: (C . m) = (f . m) by FINSEQ_1:def 7

          .= (D \ (A . (( len A) - m))) by A2, A18;

          per cases ;

            suppose m = (( len C) - 1);

            then (C . (m + 1)) = D by A5, FINSEQ_1: 42;

            hence thesis by A19;

          end;

            suppose m <> (( len C) - 1);

            then

             A20: m < (( len C) - 1) by A17, XXREAL_0: 1;

            then

             A21: (m + 1) < ( len A) by A6, A1, A5, XREAL_1: 20;

            then ( max ( 0 ,(( len A) - (m + 1)))) = (( len A) - (m + 1)) by FINSEQ_2: 4;

            then

            reconsider l = (( len A) - (m + 1)) as Element of NAT by FINSEQ_2: 5;

            

             A22: 1 <= (m + 1) by NAT_1: 11;

            (m + 1) <= (( len C) - 1) by A5, A20, NAT_1: 13;

            then

             A23: (m + 1) in ( dom f) by A5, A22, FINSEQ_3: 25;

            

            then

             A24: (C . (m + 1)) = (f . (m + 1)) by FINSEQ_1:def 7

            .= (D \ (A . l)) by A2, A23;

            ((m + 1) + 1) <= ( len A) by A21, NAT_1: 13;

            then

             A25: 1 <= (( len A) - (m + 1)) by XREAL_1: 19;

            l <= (( len A) - 1) by A22, XREAL_1: 13;

            then (A . l) c= (A . (l + 1)) by A25, Def2;

            hence thesis by A19, A24, XBOOLE_1: 34;

          end;

        end;

        then

        reconsider C as RearrangmentGen of D by A1, A5, A7, Def2, Th1;

        take C;

        let m be Nat;

        assume 1 <= m & m <= (( len C) - 1);

        then

         A26: m in ( Seg c1) by A1, A5, FINSEQ_1: 1;

        then m in ( dom f) by A1, FINSEQ_1:def 3;

        

        hence (C . m) = (f . m) by FINSEQ_1:def 7

        .= (D \ (A . (( len A) - m))) by A2, A3, A26;

      end;

      uniqueness

      proof

        let f1,f2 be RearrangmentGen of D such that

         A27: for m be Nat st 1 <= m & m <= (( len f1) - 1) holds (f1 . m) = (D \ (A . (( len A) - m))) and

         A28: for m be Nat st 1 <= m & m <= (( len f2) - 1) holds (f2 . m) = (D \ (A . (( len A) - m)));

        

         A29: ( len f2) = ( card D) by Th1;

        

         A30: ( len A) = ( card D) by Th1;

        

         A31: ( len f1) = ( card D) by Th1;

        then

         A32: ( dom f1) = ( Seg ( len A)) by A30, FINSEQ_1:def 3;

        now

          let m be Nat;

          reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

          assume

           A33: m in ( dom f1);

          then

           A34: 1 <= m by A32, FINSEQ_1: 1;

          

           A35: m <= ( len A) by A32, A33, FINSEQ_1: 1;

          per cases ;

            suppose

             A36: m = ( len A);

            then (f1 . m) = D by A31, A30, Th3;

            hence (f1 . m) = (f2 . m) by A29, A30, A36, Th3;

          end;

            suppose m <> ( len A);

            then m < ( len A) by A35, XXREAL_0: 1;

            then (m + 1) <= ( len A) by NAT_1: 13;

            then

             A37: m <= (( len A) - 1) by XREAL_1: 19;

            then (f1 . m1) = (D \ (A . (( len A) - m1))) by A27, A31, A30, A34;

            hence (f1 . m) = (f2 . m) by A28, A29, A30, A34, A37;

          end;

        end;

        hence thesis by A31, A29, FINSEQ_2: 9;

      end;

      involutiveness

      proof

        let B,A be RearrangmentGen of D such that

         A38: for m be Nat st 1 <= m & m <= (( len B) - 1) holds (B . m) = (D \ (A . (( len A) - m)));

        let m be Nat such that

         A39: 1 <= m & m <= (( len A) - 1);

        

         A40: ( len A) = ( card D) by Th1;

        

         A41: ( len B) = ( card D) by Th1;

        (( len A) - 1) < ( len A) by XREAL_1: 44;

        then

         A42: m < ( len A) by A39, XXREAL_0: 2;

        then (( len A) - m) in NAT by INT_1: 5;

        then

        reconsider n = (( len B) - m) as Nat by A40, A41;

        

         A43: (( len A) - n) = m by A40, A41;

        (m + 1) <= ( len A) by A39, XREAL_1: 19;

        then

         A44: 1 <= n by A40, A41, XREAL_1: 19;

        

         A45: n <= (( len B) - 1) by A39, XREAL_1: 10;

        (( len A) - n) in ( dom A) by A43, A39, A42, FINSEQ_3: 25;

        then

         A46: (A . (( len A) - n)) c= D by Lm5;

        

        thus (A . m) = (A . (( len A) - n)) by A40, A41

        .= (D /\ (A . (( len A) - n))) by A46, XBOOLE_1: 28

        .= (D \ (D \ (A . (( len A) - n)))) by XBOOLE_1: 48

        .= (D \ (B . (( len B) - m))) by A44, A45, A38;

      end;

    end

    ::$Canceled

    theorem :: REARRAN1:12

    

     Th11: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( len ( MIM ( FinS (F,D)))) = ( len ( CHI (A,C)))

    proof

      let F be PartFunc of D, REAL , A be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set a = ( FinS (F,D));

      reconsider a9 = a as finite Function;

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then

      reconsider F9 = F as finite Function by FINSET_1: 10;

      reconsider da9 = ( dom a9), dF9 = ( dom F9) as finite set;

      

       A4: (F | D) = F by A3, RELAT_1: 68;

      D = (( dom F) /\ D) by A3

      .= ( dom (F | D)) by RELAT_1: 61;

      then (F,( FinS (F,D))) are_fiberwise_equipotent by A4, RFUNCT_3:def 13;

      then

       A5: ( dom a) = ( Seg ( len a)) & ( card da9) = ( card dF9) by CLASSES1: 81, FINSEQ_1:def 3;

      

      thus ( len ( CHI (A,C))) = ( len A) by RFUNCT_3:def 6

      .= ( card C) by Th1

      .= ( len a) by A2, A3, A5, FINSEQ_1: 57

      .= ( len ( MIM a)) by RFINSEQ:def 2;

    end;

    definition

      let D,C be non empty finite set, A be RearrangmentGen of C, F be PartFunc of D, REAL ;

      :: REARRAN1:def5

      func Rland (F,A) -> PartFunc of C, REAL equals ( Sum (( MIM ( FinS (F,D))) (#) ( CHI (A,C))));

      correctness ;

      :: REARRAN1:def6

      func Rlor (F,A) -> PartFunc of C, REAL equals ( Sum (( MIM ( FinS (F,D))) (#) ( CHI (( Co_Gen A),C))));

      correctness ;

    end

    theorem :: REARRAN1:13

    

     Th12: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( dom ( Rland (F,A))) = C

    proof

      let F be PartFunc of D, REAL , A be RearrangmentGen of C;

      

       A1: ( len ( CHI (A,C))) = ( len A) & ( len A) <> 0 by Th4, RFUNCT_3:def 6;

      assume F is total & ( card C) = ( card D);

      then

       A2: ( len ( MIM ( FinS (F,D)))) = ( len ( CHI (A,C))) by Th11;

      thus ( dom ( Rland (F,A))) c= C;

      let x be object;

      assume x in C;

      then

      reconsider c = x as Element of C;

      ( len (( MIM ( FinS (F,D))) (#) ( CHI (A,C)))) = ( min (( len ( MIM ( FinS (F,D)))),( len ( CHI (A,C))))) & c is_common_for_dom (( MIM ( FinS (F,D))) (#) ( CHI (A,C))) by RFUNCT_3: 32, RFUNCT_3:def 7;

      hence thesis by A2, A1, RFUNCT_3: 28;

    end;

    theorem :: REARRAN1:14

    

     Th13: for c be Element of C, F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (c in (A . 1) implies ((( MIM ( FinS (F,D))) (#) ( CHI (A,C))) # c) = ( MIM ( FinS (F,D)))) & for n st 1 <= n & n < ( len A) & c in ((A . (n + 1)) \ (A . n)) holds ((( MIM ( FinS (F,D))) (#) ( CHI (A,C))) # c) = ((n |-> 0 qua Real) ^ ( MIM (( FinS (F,D)) /^ n)))

    proof

      let c be Element of C, F be PartFunc of D, REAL , A be RearrangmentGen of C;

      set fd = ( FinS (F,D)), mf = ( MIM fd), h = ( CHI (A,C)), fh = ((mf (#) h) # c);

      

       A1: ( dom A) = ( Seg ( len A)) by FINSEQ_1:def 3;

      

       A2: ( dom (mf (#) h)) = ( Seg ( len (mf (#) h))) by FINSEQ_1:def 3;

      

       A3: ( len h) = ( len A) by RFUNCT_3:def 6;

      

       A4: ( len mf) = ( len fd) by RFINSEQ:def 2;

      

       A5: ( dom fh) = ( Seg ( len fh)) by FINSEQ_1:def 3;

      

       A6: ( min (( len mf),( len h))) = ( len (mf (#) h)) by RFUNCT_3:def 7;

      assume F is total & ( card C) = ( card D);

      then

       A7: ( len mf) = ( len h) by Th11;

      

       A8: ( len fh) = ( len (mf (#) h)) by RFUNCT_3:def 8;

      

       A9: ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3;

      thus c in (A . 1) implies ((mf (#) h) # c) = mf

      proof

        assume

         A10: c in (A . 1);

        

         A11: for n st n in ( dom A) holds c in (A . n)

        proof

          let n;

          assume

           A12: n in ( dom A);

          then

           A13: 1 <= n by FINSEQ_3: 25;

          n <= ( len A) by A12, FINSEQ_3: 25;

          then 1 <= ( len A) by A13, XXREAL_0: 2;

          then 1 in ( dom A) by FINSEQ_3: 25;

          then (A . 1) c= (A . n) by A12, A13, Th2;

          hence thesis by A10;

        end;

        

         A14: ( dom ((mf (#) h) # c)) = ( Seg ( len mf)) by A7, A6, A8, FINSEQ_1:def 3;

        now

          let m be Nat;

          reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

          reconsider r1 = (fd . m) as Real;

          assume

           A15: m in ( dom ((mf (#) h) # c));

          then

           A16: 1 <= m by FINSEQ_3: 25;

          

           A17: (h . m) = ( chi ((A . m),C)) by A9, A5, A7, A6, A8, A15, RFUNCT_3:def 6;

          

           A18: c in (A . m) by A1, A5, A7, A3, A6, A8, A11, A15;

          m in ( dom mf) by A14, A15, FINSEQ_1:def 3;

          then

           A19: m <= ( len mf) by FINSEQ_3: 25;

          now

            per cases ;

              case

               A20: m = ( len mf);

              then (mf . m) = r1 by A4, RFINSEQ:def 2;

              then ((mf (#) h) . m) = (r1 (#) ( chi ((A . m),C))) by A2, A5, A8, A15, A17, RFUNCT_3:def 7;

              then

               A21: (((mf (#) h) # c) . m) = ((r1 (#) ( chi ((A . m),C))) . c) by A15, RFUNCT_3:def 8;

              ( dom (r1 (#) ( chi ((A . m),C)))) = ( dom ( chi ((A . m),C))) by VALUED_1:def 5

              .= C by RFUNCT_1: 61;

              

              hence (((mf (#) h) # c) . m) = (r1 * (( chi ((A . m),C)) . c)) by A21, VALUED_1:def 5

              .= (r1 * 1) by A18, RFUNCT_1: 63

              .= (mf . m) by A4, A20, RFINSEQ:def 2;

            end;

              case

               A22: m <> ( len mf);

              reconsider r2 = (fd . (m + 1)) as Real;

              m < ( len mf) by A19, A22, XXREAL_0: 1;

              then (m + 1) <= ( len mf) by NAT_1: 13;

              then

               A23: m <= (( len mf) - 1) by XREAL_1: 19;

              then (mf . m1) = (r1 - r2) by A16, RFINSEQ:def 2;

              then ((mf (#) h) . m) = ((r1 - r2) (#) ( chi ((A . m),C))) by A2, A5, A8, A15, A17, RFUNCT_3:def 7;

              then

               A24: (((mf (#) h) # c) . m) = (((r1 - r2) (#) ( chi ((A . m),C))) . c) by A15, RFUNCT_3:def 8;

              ( dom ((r1 - r2) (#) ( chi ((A . m),C)))) = ( dom ( chi ((A . m),C))) by VALUED_1:def 5

              .= C by RFUNCT_1: 61;

              

              hence (((mf (#) h) # c) . m) = ((r1 - r2) * (( chi ((A . m),C)) . c)) by A24, VALUED_1:def 5

              .= ((r1 - r2) * 1) by A18, RFUNCT_1: 63

              .= (mf . m1) by A16, A23, RFINSEQ:def 2;

            end;

          end;

          hence (((mf (#) h) # c) . m) = (mf . m);

        end;

        hence thesis by A7, A6, A8, FINSEQ_2: 9;

      end;

      let n;

      assume that

       A25: 1 <= n and

       A26: n < ( len A) and

       A27: c in ((A . (n + 1)) \ (A . n));

      

       A28: ( len (mf /^ n)) = (( len mf) - n) by A7, A3, A26, RFINSEQ:def 1;

      

       A29: for k st k in ( dom A) & k <= n holds not c in (A . k)

      proof

        let k;

        assume

         A30: k in ( dom A) & k <= n;

        assume

         A31: c in (A . k);

        n in ( dom A) by A25, A26, FINSEQ_3: 25;

        then (A . k) c= (A . n) by A30, Th2;

        hence contradiction by A27, A31, XBOOLE_0:def 5;

      end;

      

       A32: c in (A . (n + 1)) by A27;

      

       A33: (n + 1) <= ( len A) by A26, NAT_1: 13;

      

       A34: 1 <= (n + 1) by A25, NAT_1: 13;

      

       A35: for k st k in ( dom A) & (n + 1) <= k holds c in (A . k)

      proof

        let k;

        assume

         A36: k in ( dom A) & (n + 1) <= k;

        (n + 1) in ( dom A) by A33, A34, FINSEQ_3: 25;

        then (A . (n + 1)) c= (A . k) by A36, Th2;

        hence thesis by A32;

      end;

      set fdn = (( FinS (F,D)) /^ n), mfn = ( MIM fdn), n0 = (n |-> 0 qua Real);

      

       A37: ( len mfn) = ( len fdn) by RFINSEQ:def 2;

      

       A38: ( len n0) = n by CARD_1:def 7;

      ( len fdn) = (( len fd) - n) by A7, A3, A4, A26, RFINSEQ:def 1;

      

      then

       A39: ( len (n0 ^ mfn)) = (n + (( len fd) - n)) by A37, A38, FINSEQ_1: 22

      .= ( len mf) by RFINSEQ:def 2;

      then

       A40: ( dom (n0 ^ mfn)) = ( Seg ( len mf)) by FINSEQ_1:def 3;

      

       A41: ( dom n0) = ( Seg ( len n0)) by FINSEQ_1:def 3;

      now

        let m be Nat;

        reconsider m1 = m as Element of NAT by ORDINAL1:def 12;

        reconsider r1 = (fd . m) as Real;

        assume

         A42: m in ( dom (n0 ^ mfn));

        then

         A43: 1 <= m by FINSEQ_3: 25;

        m in ( dom mf) by A40, A42, FINSEQ_1:def 3;

        then

         A44: m <= ( len mf) by FINSEQ_3: 25;

        

         A45: (h . m) = ( chi ((A . m),C)) by A9, A7, A40, A42, RFUNCT_3:def 6;

        now

          per cases ;

            case

             A46: m <= n;

            reconsider r2 = (fd . (m + 1)) as Real;

            m < (n + 1) by A46, NAT_1: 13;

            then m < ( len A) by A33, XXREAL_0: 2;

            then (m + 1) <= ( len A) by NAT_1: 13;

            then m <= (( len mf) - 1) by A7, A3, XREAL_1: 19;

            then (mf . m1) = (r1 - r2) by A43, RFINSEQ:def 2;

            then ((mf (#) h) . m) = ((r1 - r2) (#) ( chi ((A . m),C))) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;

            then

             A47: (((mf (#) h) # c) . m) = (((r1 - r2) (#) ( chi ((A . m),C))) . c) by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;

             not c in (A . m) by A1, A7, A3, A29, A40, A42, A46;

            then

             A48: (( chi ((A . m),C)) . c) = 0 by RFUNCT_1: 64;

            

             A49: m in ( Seg n) by A43, A46, FINSEQ_1: 1;

            

             A50: (n0 . m) = 0 ;

            ( dom ((r1 - r2) (#) ( chi ((A . m),C)))) = ( dom ( chi ((A . m),C))) by VALUED_1:def 5

            .= C by RFUNCT_1: 61;

            

            hence (((mf (#) h) # c) . m) = ((r1 - r2) * (( chi ((A . m),C)) . c)) by A47, VALUED_1:def 5

            .= ((n0 ^ mfn) . m) by A38, A41, A48, A49, A50, FINSEQ_1:def 7;

          end;

            case

             A51: n < m;

            then ( max ( 0 ,(m - n))) = (m - n) by FINSEQ_2: 4;

            then

            reconsider mn = (m - n) as Element of NAT by FINSEQ_2: 5;

            

             A52: (n + 1) <= m by A51, NAT_1: 13;

            then c in (A . m) by A1, A7, A3, A35, A40, A42;

            then

             A53: (( chi ((A . m),C)) . c) = 1 by RFUNCT_1: 63;

            

             A54: 1 <= mn by A52, XREAL_1: 19;

            now

              per cases ;

                case

                 A55: m = ( len mf);

                then (mf . m) = r1 by A4, RFINSEQ:def 2;

                then ((mf (#) h) . m) = (r1 (#) ( chi ((A . m),C))) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;

                then

                 A56: (((mf (#) h) # c) . m) = ((r1 (#) ( chi ((A . m),C))) . c) by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;

                

                 A57: mn in ( dom (mf /^ n)) by A28, A54, A55, FINSEQ_3: 25;

                

                 A58: ((n0 ^ mfn) . m) = (mfn . (m - n)) by A38, A39, A44, A51, FINSEQ_1: 24

                .= ((mf /^ n) . mn) by RFINSEQ: 15

                .= (mf . (mn + n)) by A7, A3, A26, A57, RFINSEQ:def 1

                .= r1 by A4, A55, RFINSEQ:def 2;

                ( dom (r1 (#) ( chi ((A . m),C)))) = ( dom ( chi ((A . m),C))) by VALUED_1:def 5

                .= C by RFUNCT_1: 61;

                

                hence (((mf (#) h) # c) . m) = (r1 * (( chi ((A . m),C)) . c)) by A56, VALUED_1:def 5

                .= ((n0 ^ mfn) . m) by A53, A58;

              end;

                case

                 A59: m <> ( len mf);

                reconsider r2 = (fd . (m + 1)) as Real;

                m < ( len mf) by A44, A59, XXREAL_0: 1;

                then (m + 1) <= ( len mf) by NAT_1: 13;

                then

                 A60: m <= (( len mf) - 1) by XREAL_1: 19;

                then (mf . m1) = (r1 - r2) by A43, RFINSEQ:def 2;

                then ((mf (#) h) . m) = ((r1 - r2) (#) ( chi ((A . m),C))) by A2, A7, A6, A40, A42, A45, RFUNCT_3:def 7;

                then

                 A61: (((mf (#) h) # c) . m) = (((r1 - r2) (#) ( chi ((A . m),C))) . c) by A5, A7, A6, A8, A40, A42, RFUNCT_3:def 8;

                mn <= ( len (mf /^ n)) by A28, A44, XREAL_1: 9;

                then

                 A62: mn in ( dom (mf /^ n)) by A54, FINSEQ_3: 25;

                

                 A63: ((n0 ^ mfn) . m) = (mfn . (m - n)) by A38, A39, A44, A51, FINSEQ_1: 24

                .= ((mf /^ n) . mn) by RFINSEQ: 15

                .= (mf . (mn + n)) by A7, A3, A26, A62, RFINSEQ:def 1

                .= (r1 - r2) by A43, A60, RFINSEQ:def 2;

                ( dom ((r1 - r2) (#) ( chi ((A . m),C)))) = ( dom ( chi ((A . m),C))) by VALUED_1:def 5

                .= C by RFUNCT_1: 61;

                

                hence (((mf (#) h) # c) . m) = ((r1 - r2) * (( chi ((A . m),C)) . c)) by A61, VALUED_1:def 5

                .= ((n0 ^ mfn) . m) by A53, A63;

              end;

            end;

            hence (((mf (#) h) # c) . m) = ((n0 ^ mfn) . m);

          end;

        end;

        hence (((mf (#) h) # c) . m) = ((n0 ^ mfn) . m);

      end;

      hence thesis by A7, A6, A8, A39, FINSEQ_2: 9;

    end;

    theorem :: REARRAN1:15

    

     Th14: for c be Element of C, F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (c in (A . 1) implies (( Rland (F,A)) . c) = (( FinS (F,D)) . 1)) & for n st 1 <= n & n < ( len A) & c in ((A . (n + 1)) \ (A . n)) holds (( Rland (F,A)) . c) = (( FinS (F,D)) . (n + 1))

    proof

      let c be Element of C, F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set fd = ( FinS (F,D)), mf = ( MIM fd), h = ( CHI (B,C));

      

       A1: (( Rland (F,B)) . c) = ( Sum ((mf (#) h) # c)) by RFUNCT_3: 32, RFUNCT_3: 33;

      

       A2: ( len h) = ( len B) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      assume

       A3: F is total & ( card C) = ( card D);

      then

       A4: ( len mf) = ( len h) by Th11;

      thus c in (B . 1) implies (( Rland (F,B)) . c) = (( FinS (F,D)) . 1)

      proof

        assume c in (B . 1);

        

        hence (( Rland (F,B)) . c) = ( Sum mf) by A3, A1, Th13

        .= (( FinS (F,D)) . 1) by A4, A2, Th4, RFINSEQ: 16;

      end;

      let n;

      set mfn = ( MIM (( FinS (F,D)) /^ n));

      assume that

       A5: 1 <= n and

       A6: n < ( len B) and

       A7: c in ((B . (n + 1)) \ (B . n));

      ((mf (#) h) # c) = ((n |-> 0 qua Real) ^ mfn) by A3, A5, A6, A7, Th13;

      

      hence (( Rland (F,B)) . c) = (( Sum (n |-> ( In ( 0 , REAL )))) + ( Sum mfn)) by A1, RVSUM_1: 75

      .= ( 0 + ( Sum mfn)) by RVSUM_1: 81

      .= (( FinS (F,D)) . (n + 1)) by A4, A2, A6, RFINSEQ: 17;

    end;

    theorem :: REARRAN1:16

    

     Th15: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( rng ( Rland (F,A))) = ( rng ( FinS (F,D)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set fd = ( FinS (F,D)), p = ( Rland (F,B)), mf = ( MIM fd), h = ( CHI (B,C));

      

       A3: ( len mf) = ( len h) by A1, A2, Th11;

      

       A4: ( dom F) = D by A1, PARTFUN1:def 2;

      then

      reconsider fd9 = fd, F9 = F as finite Function by FINSET_1: 10;

      reconsider dfd = ( dom fd9), dF = ( dom F9) as finite set;

      

       A5: ( len h) = ( len B) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      

       A6: ( dom p) = C by A1, A2, Th12;

      

       A7: ( dom fd) = ( Seg ( len fd)) by FINSEQ_1:def 3;

      

       A8: ( dom B) = ( Seg ( len B)) by FINSEQ_1:def 3;

      (F | D) = F by A4, RELAT_1: 68;

      then (fd,F) are_fiberwise_equipotent by A4, RFUNCT_3:def 13;

      then ( card dfd) = ( card dF) by CLASSES1: 81;

      then ( len fd) <> 0 by A4, A7;

      then

       A9: ( 0 + 1) <= ( len fd) by NAT_1: 13;

      then

       A10: 1 in ( dom fd) by FINSEQ_3: 25;

      thus ( rng p) c= ( rng fd)

      proof

        let x be object;

        assume x in ( rng p);

        then

        consider c be Element of C such that c in ( dom p) and

         A11: (p . c) = x by PARTFUN1: 3;

        defpred P[ set] means $1 in ( dom B) & c in (B . $1);

        

         A12: ex n be Nat st P[n]

        proof

          take n = ( len B);

          (B . n) = C by Th3;

          hence thesis by A3, A5, A9, FINSEQ_3: 25;

        end;

        consider mi be Nat such that

         A13: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A12);

        

         A14: 1 <= mi by A13, FINSEQ_3: 25;

        then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

        

         A15: mi <= ( len B) by A13, FINSEQ_3: 25;

        now

          per cases ;

            case mi = 1;

            then (p . c) = (fd . 1) by A1, A2, A13, Th14;

            hence thesis by A10, A11, FUNCT_1:def 3;

          end;

            case mi <> 1;

            then 1 < mi by A14, XXREAL_0: 1;

            then (1 + 1) <= mi by NAT_1: 13;

            then

             A16: 1 <= m1 by XREAL_1: 19;

            

             A17: m1 < mi by XREAL_1: 44;

            then m1 <= ( len B) by A15, XXREAL_0: 2;

            then m1 in ( dom B) by A16, FINSEQ_3: 25;

            then not c in (B . m1) by A13, XREAL_1: 44;

            then

             A18: c in ((B . (m1 + 1)) \ (B . m1)) by A13, XBOOLE_0:def 5;

            m1 < ( len B) by A15, A17, XXREAL_0: 2;

            then (p . c) = (fd . (m1 + 1)) by A1, A2, A16, A18, Th14;

            hence thesis by A3, A5, A7, A8, A11, A13, FUNCT_1:def 3;

          end;

        end;

        hence thesis;

      end;

      let x be object;

      defpred P[ Nat] means $1 in ( dom fd) & (fd . $1) = x;

      assume x in ( rng fd);

      then

       A19: ex n be Nat st P[n] by FINSEQ_2: 10;

      consider mi be Nat such that

       A20: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A19);

      

       A21: 1 <= mi by A20, FINSEQ_3: 25;

      then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

      then

      reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

      

       A22: mi <= ( len fd) by A20, FINSEQ_3: 25;

      now

        per cases ;

          case

           A23: mi = 1;

          set y = the Element of (B . 1);

          

           A24: (B . 1) <> {} by A3, A5, A7, A8, A10, Th7;

          (B . 1) c= C by A3, A5, A7, A8, A10, Lm5;

          then

          reconsider y as Element of C by A24;

          (p . y) = (fd . 1) by A1, A2, A24, Th14;

          hence thesis by A6, A20, A23, FUNCT_1:def 3;

        end;

          case

           A25: mi <> 1;

          set y = the Element of ((B . (m1 + 1)) \ (B . m1));

          1 < mi by A21, A25, XXREAL_0: 1;

          then (1 + 1) <= mi by NAT_1: 13;

          then

           A26: 1 <= m1 by XREAL_1: 19;

          (m1 + 1) <= ( len fd) by A20, FINSEQ_3: 25;

          then m1 <= (( len fd) - 1) by XREAL_1: 19;

          then

           A27: ((B . (m1 + 1)) \ (B . m1)) <> {} by A3, A5, A26, Th8;

          then

           A28: y in (B . (m1 + 1)) by XBOOLE_0:def 5;

          (B . mi) c= C by A3, A5, A7, A8, A20, Lm5;

          then

          reconsider y as Element of C by A28;

          m1 < mi by XREAL_1: 44;

          then m1 < ( len fd) by A22, XXREAL_0: 2;

          then (p . y) = (fd . (m1 + 1)) by A1, A2, A3, A5, A26, A27, Th14;

          hence thesis by A6, A20, FUNCT_1:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: REARRAN1:17

    

     Th16: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( Rland (F,A)),( FinS (F,D))) are_fiberwise_equipotent

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set fd = ( FinS (F,D)), p = ( Rland (F,B)), mf = ( MIM fd), h = ( CHI (B,C));

      ( dom p) is finite;

      then

      reconsider p as finite PartFunc of C, REAL by FINSET_1: 10;

      

       A1: ( len h) = ( len B) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      

       A2: ( dom fd) = ( Seg ( len fd)) & ( dom B) = ( Seg ( len B)) by FINSEQ_1:def 3;

      assume

       A3: F is total & ( card C) = ( card D);

      then

       A4: ( len mf) = ( len h) by Th11;

      

       A5: ( dom p) = C by A3, Th12;

      

       A6: ( rng p) = ( rng fd) by A3, Th15;

      now

        let x be object;

        now

          per cases ;

            case

             A7: not x in ( rng fd);

            then (fd " {x}) = {} by Lm1;

            hence ( card (fd " {x})) = ( card (p " {x})) by A6, A7, Lm1;

          end;

            case

             A8: x in ( rng fd);

            defpred P[ Nat] means $1 in ( dom fd) & (fd . $1) = x;

            

             A9: for n be Nat st P[n] holds n <= ( len fd) by FINSEQ_3: 25;

            

             A10: ex n be Nat st P[n] by A8, FINSEQ_2: 10;

            consider ma be Nat such that

             A11: P[ma] & for n be Nat st P[n] holds n <= ma from NAT_1:sch 6( A9, A10);

            

             A12: ex n be Nat st P[n] by A8, FINSEQ_2: 10;

            consider mi be Nat such that

             A13: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A12);

            reconsider r = x as Real by A13;

            

             A14: 1 <= mi by A13, FINSEQ_3: 25;

            then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

            then

            reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

            

             A15: (m1 + 1) = mi;

            

             A16: ma <= ( len fd) by A11, FINSEQ_3: 25;

            

             A17: (( Seg ma) \ ( Seg m1)) = (fd " {x})

            proof

              thus (( Seg ma) \ ( Seg m1)) c= (fd " {x})

              proof

                let y be object;

                assume

                 A18: y in (( Seg ma) \ ( Seg m1));

                then

                reconsider l = y as Element of NAT ;

                reconsider o = (fd . l) as Real;

                

                 A19: y in ( Seg ma) by A18, XBOOLE_0:def 5;

                then

                 A20: 1 <= l by FINSEQ_1: 1;

                

                 A21: l <= ma by A19, FINSEQ_1: 1;

                then l <= ( len fd) by A16, XXREAL_0: 2;

                then

                 A22: l in ( dom fd) by A20, FINSEQ_3: 25;

                 not y in ( Seg m1) by A18, XBOOLE_0:def 5;

                then l < 1 or m1 < l by FINSEQ_1: 1;

                then mi < (l + 1) by A19, FINSEQ_1: 1, XREAL_1: 19;

                then

                 A23: mi <= l by NAT_1: 13;

                now

                  per cases ;

                    case l = ma;

                    then o in {x} by A11, TARSKI:def 1;

                    hence thesis by A22, FUNCT_1:def 7;

                  end;

                    case l <> ma;

                    then l < ma by A21, XXREAL_0: 1;

                    then

                     A24: o >= r by A11, A22, RFINSEQ: 19;

                    now

                      per cases ;

                        case l = mi;

                        then o in {x} by A13, TARSKI:def 1;

                        hence thesis by A22, FUNCT_1:def 7;

                      end;

                        case l <> mi;

                        then mi < l by A23, XXREAL_0: 1;

                        then r >= o by A13, A22, RFINSEQ: 19;

                        then r = o by A24, XXREAL_0: 1;

                        then o in {x} by TARSKI:def 1;

                        hence thesis by A22, FUNCT_1:def 7;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              let y be object;

              assume

               A25: y in (fd " {x});

              then

               A26: y in ( dom fd) by FUNCT_1:def 7;

              reconsider l = y as Element of NAT by A25;

              

               A27: 1 <= l by A26, FINSEQ_3: 25;

              (fd . y) in {x} by A25, FUNCT_1:def 7;

              then

               A28: (fd . l) = x by TARSKI:def 1;

              then mi <= l by A13, A26;

              then mi < (l + 1) by NAT_1: 13;

              then m1 < l or l < 1 by XREAL_1: 19;

              then

               A29: not l in ( Seg m1) by FINSEQ_1: 1;

              l <= ma by A11, A26, A28;

              then l in ( Seg ma) by A27, FINSEQ_1: 1;

              hence thesis by A29, XBOOLE_0:def 5;

            end;

            

             A30: 1 <= ma by A11, FINSEQ_3: 25;

            

             A31: mi <= ma by A13, A11;

            m1 <= mi by XREAL_1: 43;

            then

             A32: m1 <= ma by A31, XXREAL_0: 2;

            then ( Seg m1) c= ( Seg ma) by FINSEQ_1: 5;

            

            then

             A33: ( card (fd " {x})) = (( card ( Seg ma)) - ( card ( Seg m1))) by A17, CARD_2: 44

            .= (ma - ( card ( Seg m1))) by FINSEQ_1: 57

            .= (ma - m1) by FINSEQ_1: 57;

            

             A34: mi <= ( len fd) by A13, FINSEQ_3: 25;

            then 1 <= ( len fd) by A14, XXREAL_0: 2;

            then

             A35: 1 in ( dom fd) by FINSEQ_3: 25;

            now

              per cases ;

                case

                 A36: mi = 1;

                (B . ma) = (p " {x})

                proof

                  thus (B . ma) c= (p " {x})

                  proof

                    defpred P[ Nat] means $1 in ( dom B) & $1 <= ma implies for c be Element of C st c in (B . $1) holds c in (p " {x});

                    let y be object;

                    assume

                     A37: y in (B . ma);

                    (B . ma) c= C by A4, A1, A2, A11, Lm5;

                    then

                    reconsider cy = y as Element of C by A37;

                    

                     A38: for n st P[n] holds P[(n + 1)]

                    proof

                      let n;

                      assume

                       A39: P[n];

                      assume that

                       A40: (n + 1) in ( dom B) and

                       A41: (n + 1) <= ma;

                      

                       A42: (n + 1) <= ( len B) by A40, FINSEQ_3: 25;

                      then

                       A43: n <= (( len B) - 1) by XREAL_1: 19;

                      

                       A44: n < ( len B) by A42, NAT_1: 13;

                      let c be Element of C;

                      assume

                       A45: c in (B . (n + 1));

                      

                       A46: n <= ( len B) by A42, NAT_1: 13;

                      now

                        per cases ;

                          case n = 0 ;

                          then (p . c) = x by A3, A13, A36, A45, Th14;

                          then (p . c) in {x} by TARSKI:def 1;

                          hence thesis by A5, FUNCT_1:def 7;

                        end;

                          case

                           A47: n <> 0 ;

                          then

                           A48: ( 0 + 1) < (n + 1) by XREAL_1: 6;

                          

                           A49: ( 0 + 1) <= n by A47, NAT_1: 13;

                          then (B . n) c= (B . (n + 1)) by A43, Def2;

                          

                          then

                           A50: (B . (n + 1)) = ((B . (n + 1)) \/ (B . n)) by XBOOLE_1: 12

                          .= (((B . (n + 1)) \ (B . n)) \/ (B . n)) by XBOOLE_1: 39;

                          now

                            per cases by A45, A50, XBOOLE_0:def 3;

                              case c in ((B . (n + 1)) \ (B . n));

                              then

                               A51: (p . c) = (fd . (n + 1)) by A3, A44, A49, Th14;

                              now

                                per cases ;

                                  case (n + 1) = ma;

                                  then (p . c) in {x} by A11, A51, TARSKI:def 1;

                                  hence thesis by A5, FUNCT_1:def 7;

                                end;

                                  case (n + 1) <> ma;

                                  then (n + 1) < ma by A41, XXREAL_0: 1;

                                  then

                                   A52: (p . c) >= r by A4, A1, A2, A11, A40, A51, RFINSEQ: 19;

                                  r >= (p . c) by A4, A1, A2, A13, A36, A40, A48, A51, RFINSEQ: 19;

                                  then r = (p . c) by A52, XXREAL_0: 1;

                                  then (p . c) in {x} by TARSKI:def 1;

                                  hence thesis by A5, FUNCT_1:def 7;

                                end;

                              end;

                              hence thesis;

                            end;

                              case c in (B . n);

                              hence thesis by A39, A41, A46, A49, FINSEQ_3: 25, NAT_1: 13;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    

                     A53: P[ 0 ] by FINSEQ_3: 25;

                    

                     A54: for n holds P[n] from NAT_1:sch 2( A53, A38);

                    ma in ( dom B) by A4, A1, A11, FINSEQ_3: 29;

                    then cy in (p " {x}) by A37, A54;

                    hence thesis;

                  end;

                  let y be object;

                  assume

                   A55: y in (p " {x});

                  then

                  reconsider cy = y as Element of C;

                  (p . cy) in {x} by A55, FUNCT_1:def 7;

                  then

                   A56: (p . cy) = x by TARSKI:def 1;

                  defpred Q[ Nat] means $1 in ( dom B) & ma < $1 & cy in (B . $1);

                  assume

                   A57: not y in (B . ma);

                  

                   A58: ex n be Nat st Q[n]

                  proof

                    take n = ( len B);

                    ( len B) <> 0 by Th4;

                    then ( 0 + 1) <= ( len B) by NAT_1: 13;

                    hence n in ( dom B) by FINSEQ_3: 25;

                    

                     A59: (B . n) = C by Th3;

                    now

                      assume n <= ma;

                      then ma = ( len B) by A4, A1, A16, XXREAL_0: 1;

                      then cy in (B . ma) by A59;

                      hence contradiction by A57;

                    end;

                    hence thesis by A59;

                  end;

                  consider mm be Nat such that

                   A60: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A58);

                  1 <= mm by A60, FINSEQ_3: 25;

                  then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                  then

                  reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                  (ma + 1) <= mm by A60, NAT_1: 13;

                  then

                   A61: ma <= 1m by XREAL_1: 19;

                  then

                   A62: 1 <= 1m by A30, XXREAL_0: 2;

                  

                   A63: mm in ( dom fd) by A4, A1, A60, FINSEQ_3: 29;

                  

                   A64: mm <= ( len B) by A60, FINSEQ_3: 25;

                  

                   A65: mm < (mm + 1) by NAT_1: 13;

                  then 1m < mm by XREAL_1: 19;

                  then

                   A66: 1m < ( len B) by A64, XXREAL_0: 2;

                  1m <= mm by A65, XREAL_1: 19;

                  then 1m <= ( len B) by A64, XXREAL_0: 2;

                  then

                   A67: 1m in ( dom B) by A62, FINSEQ_3: 25;

                  now

                    per cases ;

                      case ma = 1m;

                      then cy in ((B . (1m + 1)) \ (B . 1m)) by A57, A60, XBOOLE_0:def 5;

                      then (p . cy) = (fd . mm) by A3, A62, A66, Th14;

                      hence contradiction by A11, A56, A60, A63;

                    end;

                      case ma <> 1m;

                      then

                       A68: ma < 1m by A61, XXREAL_0: 1;

                      now

                        assume cy in (B . 1m);

                        then mm <= 1m by A60, A67, A68;

                        then (mm - 1m) <= 0 by XREAL_1: 47;

                        hence contradiction;

                      end;

                      then cy in ((B . (1m + 1)) \ (B . 1m)) by A60, XBOOLE_0:def 5;

                      then (p . cy) = (fd . mm) by A3, A62, A66, Th14;

                      hence contradiction by A11, A56, A60, A63;

                    end;

                  end;

                  hence contradiction;

                end;

                hence ( card (p " {x})) = ( card (fd " {x})) by A4, A1, A30, A16, A33, A36, Def1;

              end;

                case

                 A69: mi <> 1;

                then 1 < mi by A14, XXREAL_0: 1;

                then

                 A70: 1 <= m1 by A15, NAT_1: 13;

                

                 A71: m1 <= ( len fd) by A34, A15, NAT_1: 13;

                then

                 A72: m1 in ( dom B) by A4, A1, A70, FINSEQ_3: 25;

                then

                 A73: (B . m1) c= (B . ma) by A4, A1, A2, A11, A32, Th2;

                (B . ma) c= C by A4, A1, A2, A11, Lm5;

                then

                reconsider Bma = (B . ma), Bm1 = (B . m1) as finite set by A73;

                ((B . ma) \ (B . m1)) = (p " {x})

                proof

                  thus ((B . ma) \ (B . m1)) c= (p " {x})

                  proof

                    defpred P[ Nat] means $1 in ( dom B) & mi <= $1 & $1 <= ma implies for c be Element of C st c in ((B . $1) \ (B . m1)) holds c in (p " {x});

                    let y be object;

                    

                     A74: (B . ma) c= C by A4, A1, A2, A11, Lm5;

                    

                     A75: for n st P[n] holds P[(n + 1)]

                    proof

                      let n;

                      assume

                       A76: P[n];

                      assume that

                       A77: (n + 1) in ( dom B) and

                       A78: mi <= (n + 1) and

                       A79: (n + 1) <= ma;

                      let c be Element of C;

                      (n + 1) <= ( len B) by A77, FINSEQ_3: 25;

                      then

                       A80: n < ( len B) by NAT_1: 13;

                      assume

                       A81: c in ((B . (n + 1)) \ (B . m1));

                      now

                        per cases ;

                          case

                           A82: (n + 1) = mi;

                          then (p . c) = (fd . (n + 1)) by A3, A70, A80, A81, Th14;

                          then (p . c) in {x} by A13, A82, TARSKI:def 1;

                          hence thesis by A5, FUNCT_1:def 7;

                        end;

                          case mi <> (n + 1);

                          then

                           A83: mi < (n + 1) by A78, XXREAL_0: 1;

                          then mi <= n by NAT_1: 13;

                          then

                           A84: 1 <= n by A14, XXREAL_0: 2;

                          n <= ma by A79, NAT_1: 13;

                          then

                           A85: n <= ( len B) by A4, A1, A16, XXREAL_0: 2;

                          then n <= (n + 1) & n in ( dom B) by A84, FINSEQ_3: 25, NAT_1: 11;

                          then (B . n) c= (B . (n + 1)) by A77, Th2;

                          

                          then

                           A86: ((B . (n + 1)) \ (B . m1)) = (((B . (n + 1)) \/ (B . n)) \ (B . m1)) by XBOOLE_1: 12

                          .= ((((B . (n + 1)) \ (B . n)) \/ (B . n)) \ (B . m1)) by XBOOLE_1: 39

                          .= ((((B . (n + 1)) \ (B . n)) \ (B . m1)) \/ ((B . n) \ (B . m1))) by XBOOLE_1: 42;

                          now

                            per cases by A81, A86, XBOOLE_0:def 3;

                              case c in (((B . (n + 1)) \ (B . n)) \ (B . m1));

                              then c in ((B . (n + 1)) \ (B . n)) by XBOOLE_0:def 5;

                              then

                               A87: (p . c) = (fd . (n + 1)) by A3, A80, A84, Th14;

                              now

                                per cases ;

                                  case (n + 1) = ma;

                                  then (p . c) in {x} by A11, A87, TARSKI:def 1;

                                  hence thesis by A5, FUNCT_1:def 7;

                                end;

                                  case (n + 1) <> ma;

                                  then (n + 1) < ma by A79, XXREAL_0: 1;

                                  then

                                   A88: (p . c) >= r by A4, A1, A2, A11, A77, A87, RFINSEQ: 19;

                                  r >= (p . c) by A4, A1, A2, A13, A77, A83, A87, RFINSEQ: 19;

                                  then r = (p . c) by A88, XXREAL_0: 1;

                                  then (p . c) in {x} by TARSKI:def 1;

                                  hence thesis by A5, FUNCT_1:def 7;

                                end;

                              end;

                              hence thesis;

                            end;

                              case c in ((B . n) \ (B . m1));

                              hence thesis by A76, A79, A83, A84, A85, FINSEQ_3: 25, NAT_1: 13;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    

                     A89: P[ 0 ];

                    

                     A90: for n holds P[n] from NAT_1:sch 2( A89, A75);

                    assume

                     A91: y in ((B . ma) \ (B . m1));

                    then y in (B . ma);

                    then

                    reconsider cy = y as Element of C by A74;

                    ma in ( dom B) by A4, A1, A11, FINSEQ_3: 29;

                    then cy in (p " {x}) by A31, A91, A90;

                    hence thesis;

                  end;

                  let y be object;

                  assume

                   A92: y in (p " {x});

                  then

                  reconsider cy = y as Element of C;

                  (p . cy) in {x} by A92, FUNCT_1:def 7;

                  then

                   A93: (p . cy) = x by TARSKI:def 1;

                  assume

                   A94: not y in ((B . ma) \ (B . m1));

                  now

                    per cases by A94, XBOOLE_0:def 5;

                      case

                       A95: not y in (B . ma);

                      defpred Q[ Nat] means $1 in ( dom B) & ma < $1 & cy in (B . $1);

                      

                       A96: ex n be Nat st Q[n]

                      proof

                        take n = ( len B);

                        ( len B) <> 0 by Th4;

                        then ( 0 + 1) <= ( len B) by NAT_1: 13;

                        hence n in ( dom B) by FINSEQ_3: 25;

                        

                         A97: (B . n) = C by Th3;

                        now

                          assume n <= ma;

                          then ma = ( len B) by A4, A1, A16, XXREAL_0: 1;

                          then cy in (B . ma) by A97;

                          hence contradiction by A95;

                        end;

                        hence thesis by A97;

                      end;

                      consider mm be Nat such that

                       A98: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A96);

                      1 <= mm by A98, FINSEQ_3: 25;

                      then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                      then

                      reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                      (ma + 1) <= mm by A98, NAT_1: 13;

                      then

                       A99: ma <= 1m by XREAL_1: 19;

                      then

                       A100: 1 <= 1m by A30, XXREAL_0: 2;

                      

                       A101: mm in ( dom fd) by A4, A1, A98, FINSEQ_3: 29;

                      

                       A102: mm <= ( len B) by A98, FINSEQ_3: 25;

                      

                       A103: mm < (mm + 1) by NAT_1: 13;

                      then 1m < mm by XREAL_1: 19;

                      then

                       A104: 1m < ( len B) by A102, XXREAL_0: 2;

                      1m <= mm by A103, XREAL_1: 19;

                      then 1m <= ( len B) by A102, XXREAL_0: 2;

                      then

                       A105: 1m in ( dom B) by A100, FINSEQ_3: 25;

                      now

                        per cases ;

                          case ma = 1m;

                          then cy in ((B . (1m + 1)) \ (B . 1m)) by A95, A98, XBOOLE_0:def 5;

                          then (p . cy) = (fd . mm) by A3, A100, A104, Th14;

                          hence contradiction by A11, A93, A98, A101;

                        end;

                          case ma <> 1m;

                          then

                           A106: ma < 1m by A99, XXREAL_0: 1;

                          now

                            assume cy in (B . 1m);

                            then mm <= 1m by A98, A105, A106;

                            then (mm - 1m) <= 0 by XREAL_1: 47;

                            hence contradiction;

                          end;

                          then cy in ((B . (1m + 1)) \ (B . 1m)) by A98, XBOOLE_0:def 5;

                          then (p . cy) = (fd . mm) by A3, A100, A104, Th14;

                          hence contradiction by A11, A93, A98, A101;

                        end;

                      end;

                      hence contradiction;

                    end;

                      case

                       A107: y in (B . m1);

                      defpred Q[ Nat] means $1 in ( dom B) & $1 <= m1 & cy in (B . $1);

                      

                       A108: ex n be Nat st Q[n] by A72, A107;

                      consider mm be Nat such that

                       A109: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A108);

                      

                       A110: 1 <= mm by A109, FINSEQ_3: 25;

                      then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                      then

                      reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                      

                       A111: mm <= ( len B) by A109, FINSEQ_3: 25;

                      

                       A112: mm in ( dom fd) by A4, A1, A109, FINSEQ_3: 29;

                      now

                        per cases ;

                          case mm = 1;

                          then (p . cy) = (fd . 1) by A3, A109, Th14;

                          then mi <= 1 by A13, A35, A93;

                          hence contradiction by A14, A69, XXREAL_0: 1;

                        end;

                          case mm <> 1;

                          then 1 < mm by A110, XXREAL_0: 1;

                          then (1 + 1) <= mm by NAT_1: 13;

                          then

                           A113: 1 <= 1m by XREAL_1: 19;

                          

                           A114: mm < (mm + 1) by NAT_1: 13;

                          then

                           A115: 1m <= mm by XREAL_1: 19;

                          then 1m <= ( len B) by A111, XXREAL_0: 2;

                          then

                           A116: 1m in ( dom B) by A113, FINSEQ_3: 25;

                          

                           A117: 1m < mm by A114, XREAL_1: 19;

                          then

                           A118: 1m < ( len B) by A111, XXREAL_0: 2;

                          1m <= m1 by A109, A115, XXREAL_0: 2;

                          then not cy in (B . 1m) by A109, A117, A116;

                          then cy in ((B . (1m + 1)) \ (B . 1m)) by A109, XBOOLE_0:def 5;

                          then (p . cy) = (fd . (1m + 1)) by A3, A113, A118, Th14;

                          then mi <= mm by A13, A93, A112;

                          then (m1 + 1) <= m1 by A109, XXREAL_0: 2;

                          then 1 <= (m1 - m1) by XREAL_1: 19;

                          then 1 <= 0 ;

                          hence contradiction;

                        end;

                      end;

                      hence contradiction;

                    end;

                  end;

                  hence contradiction;

                end;

                

                hence ( card (p " {x})) = (( card Bma) - ( card Bm1)) by A73, CARD_2: 44

                .= (ma - ( card Bm1)) by A4, A1, A30, A16, Def1

                .= ( card (fd " {x})) by A4, A1, A33, A70, A71, Def1;

              end;

            end;

            hence ( card (fd " {x})) = ( card (p " {x}));

          end;

        end;

        hence ( card ( Coim (fd,x))) = ( card ( Coim (p,x)));

      end;

      hence thesis by CLASSES1:def 10;

    end;

    theorem :: REARRAN1:18

    

     Th17: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( FinS (( Rland (F,A)),C)) = ( FinS (F,D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume

       A1: F is total & ( card C) = ( card D);

      then

       A2: (( Rland (F,B)),( FinS (F,D))) are_fiberwise_equipotent by Th16;

      

       A3: ( dom ( Rland (F,B))) = C by A1, Th12;

      then (( Rland (F,B)) | C) = ( Rland (F,B)) by RELAT_1: 68;

      hence thesis by A2, A3, RFUNCT_3:def 13;

    end;

    theorem :: REARRAN1:19

    

     Th18: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( Sum (( Rland (F,A)),C)) = ( Sum (F,D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume F is total & ( card C) = ( card D);

      then ( FinS (( Rland (F,B)),C)) = ( FinS (F,D)) by Th17;

      

      hence ( Sum (( Rland (F,B)),C)) = ( Sum ( FinS (F,D))) by RFUNCT_3:def 14

      .= ( Sum (F,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:20

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( FinS ((( Rland (F,A)) - r),C)) = ( FinS ((F - r),D)) & ( Sum ((( Rland (F,A)) - r),C)) = ( Sum ((F - r),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rland (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th16;

      then (( Rland (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then

       A5: ((( Rland (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      

       A6: ( dom (( Rland (F,B)) - r)) = ( dom ( Rland (F,B))) by VALUED_1: 3;

      then ((( Rland (F,B)) - r) | C) = (( Rland (F,B)) - r) by RELAT_1: 68;

      then (( FinS ((( Rland (F,B)) - r),C)),(( Rland (F,B)) - r)) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS ((( Rland (F,B)) - r),C)),(F - r)) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom (F - r)) = ( dom F) by VALUED_1: 3;

      then ((F - r) | D) = (F - r) by RELAT_1: 68;

      hence ( FinS ((( Rland (F,B)) - r),C)) = ( FinS ((F - r),D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum ((( Rland (F,B)) - r),C)) = ( Sum ( FinS ((F - r),D))) by RFUNCT_3:def 14

      .= ( Sum ((F - r),D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:21

    

     Th20: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( dom ( Rlor (F,A))) = C

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set b = ( Co_Gen B);

      

       A1: ( len ( CHI (b,C))) = ( len b) & ( len (( MIM ( FinS (F,D))) (#) ( CHI (b,C)))) = ( min (( len ( MIM ( FinS (F,D)))),( len ( CHI (b,C))))) by RFUNCT_3:def 6, RFUNCT_3:def 7;

      assume F is total & ( card C) = ( card D);

      then

       A2: ( len ( MIM ( FinS (F,D)))) = ( len ( CHI (b,C))) & ( len b) = ( card D) by Th1, Th11;

      thus ( dom ( Rlor (F,B))) c= C;

      let x be object;

      assume x in C;

      then

      reconsider c = x as Element of C;

      c is_common_for_dom (( MIM ( FinS (F,D))) (#) ( CHI (b,C))) by RFUNCT_3: 32;

      hence thesis by A1, A2, RFUNCT_3: 28;

    end;

    theorem :: REARRAN1:22

    

     Th21: for c be Element of C, F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (c in (( Co_Gen A) . 1) implies (( Rlor (F,A)) . c) = (( FinS (F,D)) . 1)) & for n st 1 <= n & n < ( len ( Co_Gen A)) & c in ((( Co_Gen A) . (n + 1)) \ (( Co_Gen A) . n)) holds (( Rlor (F,A)) . c) = (( FinS (F,D)) . (n + 1))

    proof

      let c be Element of C, F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set fd = ( FinS (F,D)), mf = ( MIM fd), b = ( Co_Gen B), h = ( CHI (b,C));

      

       A1: (( Rlor (F,B)) . c) = ( Sum ((mf (#) h) # c)) by RFUNCT_3: 32, RFUNCT_3: 33;

      

       A2: ( len h) = ( len b) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      assume

       A3: F is total & ( card C) = ( card D);

      then

       A4: ( len mf) = ( len h) by Th11;

      thus c in (b . 1) implies (( Rlor (F,B)) . c) = (( FinS (F,D)) . 1)

      proof

        assume c in (b . 1);

        

        hence (( Rlor (F,B)) . c) = ( Sum mf) by A3, A1, Th13

        .= (( FinS (F,D)) . 1) by A4, A2, Th4, RFINSEQ: 16;

      end;

      let n;

      set mfn = ( MIM (( FinS (F,D)) /^ n));

      assume that

       A5: 1 <= n and

       A6: n < ( len b) and

       A7: c in ((b . (n + 1)) \ (b . n));

      ((mf (#) h) # c) = ((n |-> 0 qua Real) ^ mfn) by A3, A5, A6, A7, Th13;

      

      hence (( Rlor (F,B)) . c) = (( Sum (n |-> ( In ( 0 , REAL )))) + ( Sum mfn)) by A1, RVSUM_1: 75

      .= ( 0 + ( Sum mfn)) by RVSUM_1: 81

      .= (( FinS (F,D)) . (n + 1)) by A4, A2, A6, RFINSEQ: 17;

    end;

    theorem :: REARRAN1:23

    

     Th22: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( rng ( Rlor (F,A))) = ( rng ( FinS (F,D)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set fd = ( FinS (F,D)), p = ( Rlor (F,B)), mf = ( MIM fd), b = ( Co_Gen B), h = ( CHI (b,C));

      

       A3: ( len mf) = ( len h) by A1, A2, Th11;

      ( dom F) is finite;

      then

      reconsider F9 = F as finite Function by FINSET_1: 10;

      

       A4: ( dom fd) = ( Seg ( len fd)) by FINSEQ_1:def 3;

      

       A5: ( dom p) = C by A1, A2, Th20;

      

       A6: ( dom b) = ( Seg ( len b)) by FINSEQ_1:def 3;

      reconsider dfd = ( dom fd), dF = ( dom F9) as finite set;

      

       A7: ( len h) = ( len b) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      

       A8: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then (fd,F) are_fiberwise_equipotent by A8, RFUNCT_3:def 13;

      then ( card dfd) = ( card dF) by CLASSES1: 81;

      then ( len fd) <> 0 by A8, A4;

      then

       A9: ( 0 + 1) <= ( len fd) by NAT_1: 13;

      then

       A10: 1 in ( dom fd) by FINSEQ_3: 25;

      thus ( rng p) c= ( rng fd)

      proof

        let x be object;

        assume x in ( rng p);

        then

        consider c be Element of C such that c in ( dom p) and

         A11: (p . c) = x by PARTFUN1: 3;

        defpred P[ set] means $1 in ( dom b) & c in (b . $1);

        

         A12: ex n be Nat st P[n]

        proof

          take n = ( len b);

          (b . n) = C by Th3;

          hence thesis by A3, A7, A9, FINSEQ_3: 25;

        end;

        consider mi be Nat such that

         A13: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A12);

        

         A14: 1 <= mi by A13, FINSEQ_3: 25;

        then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

        

         A15: mi <= ( len b) by A13, FINSEQ_3: 25;

        now

          per cases ;

            case mi = 1;

            then (p . c) = (fd . 1) by A1, A2, A13, Th21;

            hence thesis by A10, A11, FUNCT_1:def 3;

          end;

            case mi <> 1;

            then 1 < mi by A14, XXREAL_0: 1;

            then (1 + 1) <= mi by NAT_1: 13;

            then

             A16: 1 <= m1 by XREAL_1: 19;

            

             A17: m1 < mi by XREAL_1: 44;

            then m1 <= ( len b) by A15, XXREAL_0: 2;

            then m1 in ( dom b) by A16, FINSEQ_3: 25;

            then not c in (b . m1) by A13, XREAL_1: 44;

            then

             A18: c in ((b . (m1 + 1)) \ (b . m1)) by A13, XBOOLE_0:def 5;

            m1 < ( len b) by A15, A17, XXREAL_0: 2;

            then (p . c) = (fd . (m1 + 1)) by A1, A2, A16, A18, Th21;

            hence thesis by A3, A7, A4, A6, A11, A13, FUNCT_1:def 3;

          end;

        end;

        hence thesis;

      end;

      let x be object;

      defpred P[ Nat] means $1 in ( dom fd) & (fd . $1) = x;

      assume x in ( rng fd);

      then

       A19: ex n be Nat st P[n] by FINSEQ_2: 10;

      consider mi be Nat such that

       A20: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A19);

      

       A21: 1 <= mi by A20, FINSEQ_3: 25;

      then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

      then

      reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

      

       A22: mi <= ( len fd) by A20, FINSEQ_3: 25;

      now

        per cases ;

          case

           A23: mi = 1;

          set y = the Element of (b . 1);

          

           A24: (b . 1) <> {} by A3, A7, A4, A6, A10, Th7;

          (b . 1) c= C by A3, A7, A4, A6, A10, Lm5;

          then

          reconsider y as Element of C by A24;

          (p . y) = (fd . 1) by A1, A2, A24, Th21;

          hence thesis by A5, A20, A23, FUNCT_1:def 3;

        end;

          case

           A25: mi <> 1;

          set y = the Element of ((b . (m1 + 1)) \ (b . m1));

          1 < mi by A21, A25, XXREAL_0: 1;

          then (1 + 1) <= mi by NAT_1: 13;

          then

           A26: 1 <= m1 by XREAL_1: 19;

          (m1 + 1) <= ( len fd) by A20, FINSEQ_3: 25;

          then m1 <= (( len fd) - 1) by XREAL_1: 19;

          then

           A27: ((b . (m1 + 1)) \ (b . m1)) <> {} by A3, A7, A26, Th8;

          then

           A28: y in (b . (m1 + 1)) by XBOOLE_0:def 5;

          (b . mi) c= C by A3, A7, A4, A6, A20, Lm5;

          then

          reconsider y as Element of C by A28;

          m1 < mi by XREAL_1: 44;

          then m1 < ( len fd) by A22, XXREAL_0: 2;

          then (p . y) = (fd . (m1 + 1)) by A1, A2, A3, A7, A26, A27, Th21;

          hence thesis by A5, A20, FUNCT_1:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: REARRAN1:24

    

     Th23: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( Rlor (F,A)),( FinS (F,D))) are_fiberwise_equipotent

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set fd = ( FinS (F,D)), p = ( Rlor (F,B)), mf = ( MIM fd), b = ( Co_Gen B), h = ( CHI (b,C));

      

       A1: ( len h) = ( len b) & ( len mf) = ( len fd) by RFINSEQ:def 2, RFUNCT_3:def 6;

      assume

       A2: F is total & ( card C) = ( card D);

      then

       A3: ( rng p) = ( rng fd) by Th22;

      

       A4: ( dom p) = C by A2, Th20;

      then

      reconsider p as finite PartFunc of C, REAL by FINSET_1: 10;

      

       A5: ( len mf) = ( len h) by A2, Th11;

      

       A6: ( dom fd) = ( Seg ( len fd)) & ( dom b) = ( Seg ( len b)) by FINSEQ_1:def 3;

      now

        let x be object;

        now

          per cases ;

            case

             A7: not x in ( rng fd);

            then (fd " {x}) = {} by Lm1;

            hence ( card (fd " {x})) = ( card (p " {x})) by A3, A7, Lm1;

          end;

            case

             A8: x in ( rng fd);

            defpred P[ Nat] means $1 in ( dom fd) & (fd . $1) = x;

            

             A9: ex n be Nat st P[n] by A8, FINSEQ_2: 10;

            consider mi be Nat such that

             A10: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A9);

            reconsider r = x as Real by A10;

            

             A11: 1 <= mi by A10, FINSEQ_3: 25;

            then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

            then

            reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

            

             A12: (m1 + 1) = mi;

            

             A13: for n be Nat st P[n] holds n <= ( len fd) by FINSEQ_3: 25;

            consider ma be Nat such that

             A14: P[ma] & for n be Nat st P[n] holds n <= ma from NAT_1:sch 6( A13, A9);

            

             A15: ma <= ( len fd) by A14, FINSEQ_3: 25;

            

             A16: (( Seg ma) \ ( Seg m1)) = (fd " {x})

            proof

              thus (( Seg ma) \ ( Seg m1)) c= (fd " {x})

              proof

                let y be object;

                assume

                 A17: y in (( Seg ma) \ ( Seg m1));

                then

                reconsider l = y as Element of NAT ;

                reconsider o = (fd . l) as Real;

                

                 A18: y in ( Seg ma) by A17, XBOOLE_0:def 5;

                then

                 A19: 1 <= l by FINSEQ_1: 1;

                

                 A20: l <= ma by A18, FINSEQ_1: 1;

                then l <= ( len fd) by A15, XXREAL_0: 2;

                then

                 A21: l in ( dom fd) by A19, FINSEQ_3: 25;

                 not y in ( Seg m1) by A17, XBOOLE_0:def 5;

                then l < 1 or m1 < l by FINSEQ_1: 1;

                then mi < (l + 1) by A18, FINSEQ_1: 1, XREAL_1: 19;

                then

                 A22: mi <= l by NAT_1: 13;

                now

                  per cases ;

                    case l = ma;

                    then o in {x} by A14, TARSKI:def 1;

                    hence thesis by A21, FUNCT_1:def 7;

                  end;

                    case l <> ma;

                    then l < ma by A20, XXREAL_0: 1;

                    then

                     A23: o >= r by A14, A21, RFINSEQ: 19;

                    now

                      per cases ;

                        case l = mi;

                        then o in {x} by A10, TARSKI:def 1;

                        hence thesis by A21, FUNCT_1:def 7;

                      end;

                        case l <> mi;

                        then mi < l by A22, XXREAL_0: 1;

                        then r >= o by A10, A21, RFINSEQ: 19;

                        then r = o by A23, XXREAL_0: 1;

                        then o in {x} by TARSKI:def 1;

                        hence thesis by A21, FUNCT_1:def 7;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

              let y be object;

              assume

               A24: y in (fd " {x});

              then

               A25: y in ( dom fd) by FUNCT_1:def 7;

              reconsider l = y as Element of NAT by A24;

              

               A26: 1 <= l by A25, FINSEQ_3: 25;

              (fd . y) in {x} by A24, FUNCT_1:def 7;

              then

               A27: (fd . l) = x by TARSKI:def 1;

              then mi <= l by A10, A25;

              then mi < (l + 1) by NAT_1: 13;

              then m1 < l or l < 1 by XREAL_1: 19;

              then

               A28: not l in ( Seg m1) by FINSEQ_1: 1;

              l <= ma by A14, A25, A27;

              then l in ( Seg ma) by A26, FINSEQ_1: 1;

              hence thesis by A28, XBOOLE_0:def 5;

            end;

            

             A29: 1 <= ma by A14, FINSEQ_3: 25;

            

             A30: mi <= ma by A10, A14;

            m1 <= mi by XREAL_1: 43;

            then

             A31: m1 <= ma by A30, XXREAL_0: 2;

            then ( Seg m1) c= ( Seg ma) by FINSEQ_1: 5;

            

            then

             A32: ( card (fd " {x})) = (( card ( Seg ma)) - ( card ( Seg m1))) by A16, CARD_2: 44

            .= (ma - ( card ( Seg m1))) by FINSEQ_1: 57

            .= (ma - m1) by FINSEQ_1: 57;

            

             A33: mi <= ( len fd) by A10, FINSEQ_3: 25;

            then 1 <= ( len fd) by A11, XXREAL_0: 2;

            then

             A34: 1 in ( dom fd) by FINSEQ_3: 25;

            now

              per cases ;

                case

                 A35: mi = 1;

                (b . ma) = (p " {x})

                proof

                  thus (b . ma) c= (p " {x})

                  proof

                    defpred P[ Nat] means $1 in ( dom b) & $1 <= ma implies for c be Element of C st c in (b . $1) holds c in (p " {x});

                    let y be object;

                    assume

                     A36: y in (b . ma);

                    (b . ma) c= C by A5, A1, A6, A14, Lm5;

                    then

                    reconsider cy = y as Element of C by A36;

                    

                     A37: for n st P[n] holds P[(n + 1)]

                    proof

                      let n;

                      assume

                       A38: P[n];

                      assume that

                       A39: (n + 1) in ( dom b) and

                       A40: (n + 1) <= ma;

                      

                       A41: (n + 1) <= ( len b) by A39, FINSEQ_3: 25;

                      then

                       A42: n <= (( len b) - 1) by XREAL_1: 19;

                      

                       A43: n < ( len b) by A41, NAT_1: 13;

                      let c be Element of C;

                      assume

                       A44: c in (b . (n + 1));

                      

                       A45: n <= ( len b) by A41, NAT_1: 13;

                      now

                        per cases ;

                          case n = 0 ;

                          then (p . c) = x by A2, A10, A35, A44, Th21;

                          then (p . c) in {x} by TARSKI:def 1;

                          hence thesis by A4, FUNCT_1:def 7;

                        end;

                          case

                           A46: n <> 0 ;

                          then

                           A47: ( 0 + 1) < (n + 1) by XREAL_1: 6;

                          

                           A48: ( 0 + 1) <= n by A46, NAT_1: 13;

                          then (b . n) c= (b . (n + 1)) by A42, Def2;

                          

                          then

                           A49: (b . (n + 1)) = ((b . (n + 1)) \/ (b . n)) by XBOOLE_1: 12

                          .= (((b . (n + 1)) \ (b . n)) \/ (b . n)) by XBOOLE_1: 39;

                          now

                            per cases by A44, A49, XBOOLE_0:def 3;

                              case c in ((b . (n + 1)) \ (b . n));

                              then

                               A50: (p . c) = (fd . (n + 1)) by A2, A43, A48, Th21;

                              now

                                per cases ;

                                  case (n + 1) = ma;

                                  then (p . c) in {x} by A14, A50, TARSKI:def 1;

                                  hence thesis by A4, FUNCT_1:def 7;

                                end;

                                  case (n + 1) <> ma;

                                  then (n + 1) < ma by A40, XXREAL_0: 1;

                                  then

                                   A51: (p . c) >= r by A5, A1, A6, A14, A39, A50, RFINSEQ: 19;

                                  r >= (p . c) by A5, A1, A6, A10, A35, A39, A47, A50, RFINSEQ: 19;

                                  then r = (p . c) by A51, XXREAL_0: 1;

                                  then (p . c) in {x} by TARSKI:def 1;

                                  hence thesis by A4, FUNCT_1:def 7;

                                end;

                              end;

                              hence thesis;

                            end;

                              case c in (b . n);

                              hence thesis by A38, A40, A45, A48, FINSEQ_3: 25, NAT_1: 13;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    

                     A52: P[ 0 ] by FINSEQ_3: 25;

                    

                     A53: for n holds P[n] from NAT_1:sch 2( A52, A37);

                    ma in ( dom b) by A5, A1, A14, FINSEQ_3: 29;

                    then cy in (p " {x}) by A36, A53;

                    hence thesis;

                  end;

                  let y be object;

                  assume

                   A54: y in (p " {x});

                  then

                  reconsider cy = y as Element of C;

                  (p . cy) in {x} by A54, FUNCT_1:def 7;

                  then

                   A55: (p . cy) = x by TARSKI:def 1;

                  defpred Q[ Nat] means $1 in ( dom b) & ma < $1 & cy in (b . $1);

                  assume

                   A56: not y in (b . ma);

                  

                   A57: ex n be Nat st Q[n]

                  proof

                    take n = ( len b);

                    ( len b) <> 0 by Th4;

                    then ( 0 + 1) <= ( len b) by NAT_1: 13;

                    hence n in ( dom b) by FINSEQ_3: 25;

                    

                     A58: (b . n) = C by Th3;

                    now

                      assume n <= ma;

                      then ma = ( len b) by A5, A1, A15, XXREAL_0: 1;

                      then cy in (b . ma) by A58;

                      hence contradiction by A56;

                    end;

                    hence thesis by A58;

                  end;

                  consider mm be Nat such that

                   A59: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A57);

                  1 <= mm by A59, FINSEQ_3: 25;

                  then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                  then

                  reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                  (ma + 1) <= mm by A59, NAT_1: 13;

                  then

                   A60: ma <= 1m by XREAL_1: 19;

                  then

                   A61: 1 <= 1m by A29, XXREAL_0: 2;

                  

                   A62: mm in ( dom fd) by A5, A1, A59, FINSEQ_3: 29;

                  

                   A63: mm <= ( len b) by A59, FINSEQ_3: 25;

                  

                   A64: mm < (mm + 1) by NAT_1: 13;

                  then 1m < mm by XREAL_1: 19;

                  then

                   A65: 1m < ( len b) by A63, XXREAL_0: 2;

                  1m <= mm by A64, XREAL_1: 19;

                  then 1m <= ( len b) by A63, XXREAL_0: 2;

                  then

                   A66: 1m in ( dom b) by A61, FINSEQ_3: 25;

                  now

                    per cases ;

                      case ma = 1m;

                      then cy in ((b . (1m + 1)) \ (b . 1m)) by A56, A59, XBOOLE_0:def 5;

                      then (p . cy) = (fd . mm) by A2, A61, A65, Th21;

                      hence contradiction by A14, A55, A59, A62;

                    end;

                      case ma <> 1m;

                      then

                       A67: ma < 1m by A60, XXREAL_0: 1;

                      now

                        assume cy in (b . 1m);

                        then mm <= 1m by A59, A66, A67;

                        then (mm - 1m) <= 0 by XREAL_1: 47;

                        hence contradiction;

                      end;

                      then cy in ((b . (1m + 1)) \ (b . 1m)) by A59, XBOOLE_0:def 5;

                      then (p . cy) = (fd . mm) by A2, A61, A65, Th21;

                      hence contradiction by A14, A55, A59, A62;

                    end;

                  end;

                  hence contradiction;

                end;

                hence ( card (p " {x})) = ( card (fd " {x})) by A5, A1, A29, A15, A32, A35, Def1;

              end;

                case

                 A68: mi <> 1;

                then 1 < mi by A11, XXREAL_0: 1;

                then

                 A69: 1 <= m1 by A12, NAT_1: 13;

                

                 A70: m1 <= ( len fd) by A33, A12, NAT_1: 13;

                then

                 A71: m1 in ( dom b) by A5, A1, A69, FINSEQ_3: 25;

                then

                 A72: (b . m1) c= (b . ma) by A5, A1, A6, A14, A31, Th2;

                (b . ma) c= C by A5, A1, A6, A14, Lm5;

                then

                reconsider bma = (b . ma), bm1 = (b . m1) as finite set by A72;

                ((b . ma) \ (b . m1)) = (p " {x})

                proof

                  thus ((b . ma) \ (b . m1)) c= (p " {x})

                  proof

                    defpred P[ Nat] means $1 in ( dom b) & mi <= $1 & $1 <= ma implies for c be Element of C st c in ((b . $1) \ (b . m1)) holds c in (p " {x});

                    let y be object;

                    

                     A73: (b . ma) c= C by A5, A1, A6, A14, Lm5;

                    

                     A74: for n st P[n] holds P[(n + 1)]

                    proof

                      let n;

                      assume

                       A75: P[n];

                      assume that

                       A76: (n + 1) in ( dom b) and

                       A77: mi <= (n + 1) and

                       A78: (n + 1) <= ma;

                      let c be Element of C;

                      (n + 1) <= ( len b) by A76, FINSEQ_3: 25;

                      then

                       A79: n < ( len b) by NAT_1: 13;

                      assume

                       A80: c in ((b . (n + 1)) \ (b . m1));

                      now

                        per cases ;

                          case

                           A81: (n + 1) = mi;

                          then (p . c) = (fd . (n + 1)) by A2, A69, A79, A80, Th21;

                          then (p . c) in {x} by A10, A81, TARSKI:def 1;

                          hence thesis by A4, FUNCT_1:def 7;

                        end;

                          case mi <> (n + 1);

                          then

                           A82: mi < (n + 1) by A77, XXREAL_0: 1;

                          then mi <= n by NAT_1: 13;

                          then

                           A83: 1 <= n by A11, XXREAL_0: 2;

                          n <= ma by A78, NAT_1: 13;

                          then

                           A84: n <= ( len b) by A5, A1, A15, XXREAL_0: 2;

                          then n <= (n + 1) & n in ( dom b) by A83, FINSEQ_3: 25, NAT_1: 11;

                          then (b . n) c= (b . (n + 1)) by A76, Th2;

                          

                          then

                           A85: ((b . (n + 1)) \ (b . m1)) = (((b . (n + 1)) \/ (b . n)) \ (b . m1)) by XBOOLE_1: 12

                          .= ((((b . (n + 1)) \ (b . n)) \/ (b . n)) \ (b . m1)) by XBOOLE_1: 39

                          .= ((((b . (n + 1)) \ (b . n)) \ (b . m1)) \/ ((b . n) \ (b . m1))) by XBOOLE_1: 42;

                          now

                            per cases by A80, A85, XBOOLE_0:def 3;

                              case c in (((b . (n + 1)) \ (b . n)) \ (b . m1));

                              then c in ((b . (n + 1)) \ (b . n)) by XBOOLE_0:def 5;

                              then

                               A86: (p . c) = (fd . (n + 1)) by A2, A79, A83, Th21;

                              now

                                per cases ;

                                  case (n + 1) = ma;

                                  then (p . c) in {x} by A14, A86, TARSKI:def 1;

                                  hence thesis by A4, FUNCT_1:def 7;

                                end;

                                  case (n + 1) <> ma;

                                  then (n + 1) < ma by A78, XXREAL_0: 1;

                                  then

                                   A87: (p . c) >= r by A5, A1, A6, A14, A76, A86, RFINSEQ: 19;

                                  r >= (p . c) by A5, A1, A6, A10, A76, A82, A86, RFINSEQ: 19;

                                  then r = (p . c) by A87, XXREAL_0: 1;

                                  then (p . c) in {x} by TARSKI:def 1;

                                  hence thesis by A4, FUNCT_1:def 7;

                                end;

                              end;

                              hence thesis;

                            end;

                              case c in ((b . n) \ (b . m1));

                              hence thesis by A75, A78, A82, A83, A84, FINSEQ_3: 25, NAT_1: 13;

                            end;

                          end;

                          hence thesis;

                        end;

                      end;

                      hence thesis;

                    end;

                    

                     A88: P[ 0 ];

                    

                     A89: for n holds P[n] from NAT_1:sch 2( A88, A74);

                    assume

                     A90: y in ((b . ma) \ (b . m1));

                    then y in (b . ma);

                    then

                    reconsider cy = y as Element of C by A73;

                    ma in ( dom b) by A5, A1, A14, FINSEQ_3: 29;

                    then cy in (p " {x}) by A30, A90, A89;

                    hence thesis;

                  end;

                  let y be object;

                  assume

                   A91: y in (p " {x});

                  then

                  reconsider cy = y as Element of C;

                  (p . cy) in {x} by A91, FUNCT_1:def 7;

                  then

                   A92: (p . cy) = x by TARSKI:def 1;

                  assume

                   A93: not y in ((b . ma) \ (b . m1));

                  now

                    per cases by A93, XBOOLE_0:def 5;

                      case

                       A94: not y in (b . ma);

                      defpred Q[ Nat] means $1 in ( dom b) & ma < $1 & cy in (b . $1);

                      

                       A95: ex n be Nat st Q[n]

                      proof

                        take n = ( len b);

                        ( len b) <> 0 by Th4;

                        then ( 0 + 1) <= ( len b) by NAT_1: 13;

                        hence n in ( dom b) by FINSEQ_3: 25;

                        

                         A96: (b . n) = C by Th3;

                        now

                          assume n <= ma;

                          then ma = ( len b) by A5, A1, A15, XXREAL_0: 1;

                          then cy in (b . ma) by A96;

                          hence contradiction by A94;

                        end;

                        hence thesis by A96;

                      end;

                      consider mm be Nat such that

                       A97: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A95);

                      1 <= mm by A97, FINSEQ_3: 25;

                      then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                      then

                      reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                      (ma + 1) <= mm by A97, NAT_1: 13;

                      then

                       A98: ma <= 1m by XREAL_1: 19;

                      then

                       A99: 1 <= 1m by A29, XXREAL_0: 2;

                      

                       A100: mm in ( dom fd) by A5, A1, A97, FINSEQ_3: 29;

                      

                       A101: mm <= ( len b) by A97, FINSEQ_3: 25;

                      

                       A102: mm < (mm + 1) by NAT_1: 13;

                      then 1m < mm by XREAL_1: 19;

                      then

                       A103: 1m < ( len b) by A101, XXREAL_0: 2;

                      1m <= mm by A102, XREAL_1: 19;

                      then 1m <= ( len b) by A101, XXREAL_0: 2;

                      then

                       A104: 1m in ( dom b) by A99, FINSEQ_3: 25;

                      now

                        per cases ;

                          case ma = 1m;

                          then cy in ((b . (1m + 1)) \ (b . 1m)) by A94, A97, XBOOLE_0:def 5;

                          then (p . cy) = (fd . mm) by A2, A99, A103, Th21;

                          hence contradiction by A14, A92, A97, A100;

                        end;

                          case ma <> 1m;

                          then

                           A105: ma < 1m by A98, XXREAL_0: 1;

                          now

                            assume cy in (b . 1m);

                            then mm <= 1m by A97, A104, A105;

                            then (mm - 1m) <= 0 by XREAL_1: 47;

                            hence contradiction;

                          end;

                          then cy in ((b . (1m + 1)) \ (b . 1m)) by A97, XBOOLE_0:def 5;

                          then (p . cy) = (fd . mm) by A2, A99, A103, Th21;

                          hence contradiction by A14, A92, A97, A100;

                        end;

                      end;

                      hence contradiction;

                    end;

                      case

                       A106: y in (b . m1);

                      defpred Q[ Nat] means $1 in ( dom b) & $1 <= m1 & cy in (b . $1);

                      

                       A107: ex n be Nat st Q[n] by A71, A106;

                      consider mm be Nat such that

                       A108: Q[mm] & for n be Nat st Q[n] holds mm <= n from NAT_1:sch 5( A107);

                      

                       A109: 1 <= mm by A108, FINSEQ_3: 25;

                      then ( max ( 0 ,(mm - 1))) = (mm - 1) by FINSEQ_2: 4;

                      then

                      reconsider 1m = (mm - 1) as Element of NAT by FINSEQ_2: 5;

                      

                       A110: mm <= ( len b) by A108, FINSEQ_3: 25;

                      

                       A111: mm in ( dom fd) by A5, A1, A108, FINSEQ_3: 29;

                      now

                        per cases ;

                          case mm = 1;

                          then (p . cy) = (fd . 1) by A2, A108, Th21;

                          then mi <= 1 by A10, A34, A92;

                          hence contradiction by A11, A68, XXREAL_0: 1;

                        end;

                          case mm <> 1;

                          then 1 < mm by A109, XXREAL_0: 1;

                          then (1 + 1) <= mm by NAT_1: 13;

                          then

                           A112: 1 <= 1m by XREAL_1: 19;

                          

                           A113: mm < (mm + 1) by NAT_1: 13;

                          then

                           A114: 1m <= mm by XREAL_1: 19;

                          then 1m <= ( len b) by A110, XXREAL_0: 2;

                          then

                           A115: 1m in ( dom b) by A112, FINSEQ_3: 25;

                          

                           A116: 1m < mm by A113, XREAL_1: 19;

                          then

                           A117: 1m < ( len b) by A110, XXREAL_0: 2;

                          1m <= m1 by A108, A114, XXREAL_0: 2;

                          then not cy in (b . 1m) by A108, A116, A115;

                          then cy in ((b . (1m + 1)) \ (b . 1m)) by A108, XBOOLE_0:def 5;

                          then (p . cy) = (fd . (1m + 1)) by A2, A112, A117, Th21;

                          then mi <= mm by A10, A92, A111;

                          then (m1 + 1) <= m1 by A108, XXREAL_0: 2;

                          then 1 <= (m1 - m1) by XREAL_1: 19;

                          then 1 <= 0 ;

                          hence contradiction;

                        end;

                      end;

                      hence contradiction;

                    end;

                  end;

                  hence contradiction;

                end;

                

                hence ( card (p " {x})) = (( card bma) - ( card bm1)) by A72, CARD_2: 44

                .= (ma - ( card bm1)) by A5, A1, A29, A15, Def1

                .= ( card (fd " {x})) by A5, A1, A32, A69, A70, Def1;

              end;

            end;

            hence ( card (fd " {x})) = ( card (p " {x}));

          end;

        end;

        hence ( card ( Coim (fd,x))) = ( card ( Coim (p,x)));

      end;

      hence thesis by CLASSES1:def 10;

    end;

    theorem :: REARRAN1:25

    

     Th24: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( FinS (( Rlor (F,A)),C)) = ( FinS (F,D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume

       A1: F is total & ( card C) = ( card D);

      then

       A2: (( Rlor (F,B)),( FinS (F,D))) are_fiberwise_equipotent by Th23;

      

       A3: ( dom ( Rlor (F,B))) = C by A1, Th20;

      then (( Rlor (F,B)) | C) = ( Rlor (F,B)) by RELAT_1: 68;

      hence thesis by A2, A3, RFUNCT_3:def 13;

    end;

    theorem :: REARRAN1:26

    

     Th25: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( Sum (( Rlor (F,A)),C)) = ( Sum (F,D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume F is total & ( card C) = ( card D);

      then ( FinS (( Rlor (F,B)),C)) = ( FinS (F,D)) by Th24;

      

      hence ( Sum (( Rlor (F,B)),C)) = ( Sum ( FinS (F,D))) by RFUNCT_3:def 14

      .= ( Sum (F,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:27

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds ( FinS ((( Rlor (F,A)) - r),C)) = ( FinS ((F - r),D)) & ( Sum ((( Rlor (F,A)) - r),C)) = ( Sum ((F - r),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rlor (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th23;

      then (( Rlor (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then

       A5: ((( Rlor (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      

       A6: ( dom (( Rlor (F,B)) - r)) = ( dom ( Rlor (F,B))) by VALUED_1: 3;

      then ((( Rlor (F,B)) - r) | C) = (( Rlor (F,B)) - r) by RELAT_1: 68;

      then (( FinS ((( Rlor (F,B)) - r),C)),(( Rlor (F,B)) - r)) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS ((( Rlor (F,B)) - r),C)),(F - r)) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom (F - r)) = ( dom F) by VALUED_1: 3;

      then ((F - r) | D) = (F - r) by RELAT_1: 68;

      hence ( FinS ((( Rlor (F,B)) - r),C)) = ( FinS ((F - r),D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum ((( Rlor (F,B)) - r),C)) = ( Sum ( FinS ((F - r),D))) by RFUNCT_3:def 14

      .= ( Sum ((F - r),D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:28

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( Rlor (F,A)),( Rland (F,A))) are_fiberwise_equipotent & ( FinS (( Rlor (F,A)),C)) = ( FinS (( Rland (F,A)),C)) & ( Sum (( Rlor (F,A)),C)) = ( Sum (( Rland (F,A)),C))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume

       A1: F is total & ( card C) = ( card D);

      then

       A2: ( Sum (( Rland (F,B)),C)) = ( Sum (F,D)) & (( Rlor (F,B)),( FinS (F,D))) are_fiberwise_equipotent by Th18, Th23;

      (( Rland (F,B)),( FinS (F,D))) are_fiberwise_equipotent & ( FinS (( Rland (F,B)),C)) = ( FinS (F,D)) by A1, Th16, Th17;

      hence thesis by A1, A2, Th24, Th25, CLASSES1: 76;

    end;

    theorem :: REARRAN1:29

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( max+ (( Rland (F,A)) - r)),( max+ (F - r))) are_fiberwise_equipotent & ( FinS (( max+ (( Rland (F,A)) - r)),C)) = ( FinS (( max+ (F - r)),D)) & ( Sum (( max+ (( Rland (F,A)) - r)),C)) = ( Sum (( max+ (F - r)),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set mp = ( max+ (( Rland (F,B)) - r)), mf = ( max+ (F - r));

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rland (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th16;

      then (( Rland (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then ((( Rland (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      hence

       A5: (mp,mf) are_fiberwise_equipotent by RFUNCT_3: 41;

      

       A6: ( dom mp) = ( dom (( Rland (F,B)) - r)) by RFUNCT_3:def 10;

      then (mp | C) = mp by RELAT_1: 68;

      then (( FinS (mp,C)),mp) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS (mp,C)),mf) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom mf) = ( dom (F - r)) by RFUNCT_3:def 10;

      then (mf | D) = mf by RELAT_1: 68;

      hence ( FinS (mp,C)) = ( FinS (mf,D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum (mp,C)) = ( Sum ( FinS (mf,D))) by RFUNCT_3:def 14

      .= ( Sum (mf,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:30

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( max- (( Rland (F,A)) - r)),( max- (F - r))) are_fiberwise_equipotent & ( FinS (( max- (( Rland (F,A)) - r)),C)) = ( FinS (( max- (F - r)),D)) & ( Sum (( max- (( Rland (F,A)) - r)),C)) = ( Sum (( max- (F - r)),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set mp = ( max- (( Rland (F,B)) - r)), mf = ( max- (F - r));

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rland (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th16;

      then (( Rland (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then ((( Rland (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      hence

       A5: (mp,mf) are_fiberwise_equipotent by RFUNCT_3: 42;

      

       A6: ( dom mp) = ( dom (( Rland (F,B)) - r)) by RFUNCT_3:def 11;

      then (mp | C) = mp by RELAT_1: 68;

      then (( FinS (mp,C)),mp) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS (mp,C)),mf) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom mf) = ( dom (F - r)) by RFUNCT_3:def 11;

      then (mf | D) = mf by RELAT_1: 68;

      hence ( FinS (mp,C)) = ( FinS (mf,D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum (mp,C)) = ( Sum ( FinS (mf,D))) by RFUNCT_3:def 14

      .= ( Sum (mf,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:31

    

     Th30: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) holds ( len ( FinS (( Rland (F,A)),C))) = ( card C) & 1 <= ( len ( FinS (( Rland (F,A)),C)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set p = ( Rland (F,B));

      assume F is total & ( card D) = ( card C);

      then

       A1: ( dom p) = C by Th12;

      then

       A2: (p | C) = p by RELAT_1: 68;

      hence ( len ( FinS (p,C))) = ( card C) by A1, RFUNCT_3: 67;

      ( 0 + 1) <= ( card C) by NAT_1: 13;

      hence thesis by A1, A2, RFUNCT_3: 67;

    end;

    theorem :: REARRAN1:32

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) & n in ( dom A) holds (( FinS (( Rland (F,A)),C)) | n) = ( FinS (( Rland (F,A)),(A . n)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total & ( card D) = ( card C) and

       A2: n in ( dom B);

      set p = ( Rland (F,B));

      

       A3: ( len ( FinS (p,C))) = ( card C) by A1, Th30;

      defpred P[ Nat] means $1 in ( dom B) implies (( FinS (( Rland (F,B)),C)) | $1) = ( FinS (( Rland (F,B)),(B . $1)));

      

       A4: ( len B) = ( card C) by Th1;

      

       A5: ( dom B) = ( Seg ( len B)) & ( dom ( FinS (p,C))) = ( Seg ( len ( FinS (p,C)))) by FINSEQ_1:def 3;

      

       A6: for m st P[m] holds P[(m + 1)]

      proof

        set f = ( FinS (p,C));

        let m;

        assume

         A7: P[m];

        

         A8: m <= (m + 1) by NAT_1: 11;

        assume

         A9: (m + 1) in ( dom B);

        then 1 <= (m + 1) by FINSEQ_3: 25;

        then

         A10: (m + 1) in ( Seg (m + 1)) by FINSEQ_1: 1;

        

         A11: ( dom p) = C by A1, Th12;

        

         A12: (m + 1) <= ( len B) by A9, FINSEQ_3: 25;

        then

         A13: m <= ( len B) by NAT_1: 13;

        

         A14: m < ( len B) by A12, NAT_1: 13;

        

         A15: m <= (( len B) - 1) by A12, XREAL_1: 19;

        

         A16: ( len (f | (m + 1))) = (m + 1) by A4, A3, A12, FINSEQ_1: 59;

        now

          per cases ;

            case

             A17: m = 0 ;

            consider d be Element of C such that

             A18: (B . 1) = {d} by Th9;

            

             A19: d in (B . 1) by A18, TARSKI:def 1;

            

             A20: 1 <= ( len ( FinS (p,C))) by A1, Th30;

            then 1 in ( Seg 1) & 1 in ( dom ( FinS (p,C))) by FINSEQ_1: 1, FINSEQ_3: 25;

            

            then

             A21: ((( FinS (p,C)) | (m + 1)) . 1) = (( FinS (p,C)) . 1) by A17, RFINSEQ: 6

            .= (( FinS (F,D)) . 1) by A1, Th17

            .= (p . d) by A1, A19, Th14;

            ( dom p) = C by A1, Th12;

            then

             A22: ( FinS (p,(B . (m + 1)))) = <*(p . d)*> by A17, A18, RFUNCT_3: 69;

            ( len (( FinS (p,C)) | (m + 1))) = 1 by A17, A20, FINSEQ_1: 59;

            hence thesis by A22, A21, FINSEQ_1: 40;

          end;

            case

             A23: m <> 0 ;

            

             A24: ( Seg m) c= ( Seg (m + 1)) by A8, FINSEQ_1: 5;

            

             A25: ((f | (m + 1)) | m) = ((f | (m + 1)) | ( Seg m)) by FINSEQ_1:def 15

            .= ((f | ( Seg (m + 1))) | ( Seg m)) by FINSEQ_1:def 15

            .= (f | (( Seg (m + 1)) /\ ( Seg m))) by RELAT_1: 71

            .= (f | ( Seg m)) by A24, XBOOLE_1: 28

            .= (f | m) by FINSEQ_1:def 15;

            

             A26: ( 0 + 1) <= m by A23, NAT_1: 13;

            then

            consider d be Element of C such that

             A27: ((B . (m + 1)) \ (B . m)) = {d} and (B . (m + 1)) = ((B . m) \/ {d}) and

             A28: ((B . (m + 1)) \ {d}) = (B . m) by A15, Th10;

            

             A29: d in {d} by TARSKI:def 1;

            

            then (p . d) = (( FinS (F,D)) . (m + 1)) by A1, A14, A26, A27, Th14

            .= (( FinS (p,C)) . (m + 1)) by A1, Th17

            .= ((f | (m + 1)) . (m + 1)) by A5, A4, A3, A9, A10, RFINSEQ: 6;

            then

             A30: (f | (m + 1)) = ((f | m) ^ <*(p . d)*>) by A16, A25, RFINSEQ: 7;

            d in (( dom p) /\ (B . (m + 1))) by A11, A27, A29, XBOOLE_0:def 4;

            then

             A31: d in ( dom (p | (B . (m + 1)))) by RELAT_1: 61;

            

             A32: (f | (m + 1)) is non-increasing by RFINSEQ: 20;

            

             A33: ( dom (p | (B . (m + 1)))) = (( dom p) /\ (B . (m + 1))) by RELAT_1: 61

            .= (B . (m + 1)) by A9, A11, Lm5, XBOOLE_1: 28;

            (B . (m + 1)) is finite by A9, Lm5, FINSET_1: 1;

            then ((f | (m + 1)),(p | (B . (m + 1)))) are_fiberwise_equipotent by A7, A13, A26, A28, A30, A31, FINSEQ_3: 25, RFUNCT_3: 65;

            hence thesis by A33, A32, RFUNCT_3:def 13;

          end;

        end;

        hence thesis;

      end;

      

       A34: P[ 0 ] by FINSEQ_3: 25;

      for m holds P[m] from NAT_1:sch 2( A34, A6);

      hence thesis by A2;

    end;

    theorem :: REARRAN1:33

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) holds ( Rland ((F - r),A)) = (( Rland (F,A)) - r)

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card D) = ( card C);

      

       A3: ( dom ( Rland (F,B))) = C by A1, A2, Th12;

      

       A4: ( dom F) = D by A1, PARTFUN1:def 2;

      then

       A5: ( dom (F - r)) = D by VALUED_1: 3;

      then

       A6: (F - r) is total by PARTFUN1:def 2;

      ((F - r) | D) = (F - r) by A5, RELAT_1: 68;

      then

       A7: ( len ( FinS ((F - r),D))) = ( card D) by A5, RFUNCT_3: 67;

      

       A8: ( len B) = ( card C) by Th1;

      reconsider rr = r as Element of REAL by XREAL_0:def 1;

      (F | D) = F by A4, RELAT_1: 68;

      then

       A9: ( FinS ((F - r),D)) = (( FinS (F,D)) - (( card D) |-> rr)) by A4, RFUNCT_3: 73;

       A10:

      now

        let c be Element of C;

        assume c in ( dom ( Rland ((F - r),B)));

        defpred P[ set] means $1 in ( dom B) & c in (B . $1);

        

         A11: C = (B . ( len B)) by Th3;

        ( len B) <> 0 by Th4;

        then

         A12: ( 0 + 1) <= ( len B) by NAT_1: 13;

        then

         A13: 1 in ( dom B) by FINSEQ_3: 25;

        ( len B) in ( dom B) by A12, FINSEQ_3: 25;

        then

         A14: ex n be Nat st P[n] by A11;

        consider mi be Nat such that

         A15: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A14);

        

         A16: 1 <= mi by A15, FINSEQ_3: 25;

        then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

        

         A17: mi <= ( len B) by A15, FINSEQ_3: 25;

        

         A18: mi < (mi + 1) by NAT_1: 13;

        then m1 < mi by XREAL_1: 19;

        then

         A19: m1 < ( len B) by A17, XXREAL_0: 2;

        m1 <= mi by A18, XREAL_1: 19;

        then

         A20: m1 <= ( len B) by A17, XXREAL_0: 2;

        now

          per cases ;

            case

             A21: mi = 1;

            

             A22: 1 in ( dom ( FinS ((F - r),D))) by A2, A7, A8, A12, FINSEQ_3: 25;

            1 in ( Seg ( card D)) by A2, A8, A13, FINSEQ_1:def 3;

            then

             A23: ((( card D) |-> r) . 1) = r by FUNCOP_1: 7;

            (( Rland ((F - r),B)) . c) = (( FinS ((F - r),D)) . 1) & (( Rland (F,B)) . c) = (( FinS (F,D)) . 1) by A1, A2, A6, A15, A21, Th14;

            

            hence (( Rland ((F - r),B)) . c) = ((( Rland (F,B)) . c) - r) by A9, A22, A23, VALUED_1: 13

            .= ((( Rland (F,B)) - r) . c) by A3, VALUED_1: 3;

          end;

            case mi <> 1;

            then 1 < mi by A16, XXREAL_0: 1;

            then (1 + 1) <= mi by NAT_1: 13;

            then

             A24: 1 <= m1 by XREAL_1: 19;

            then m1 in ( dom B) by A20, FINSEQ_3: 25;

            then not c in (B . m1) by A15, XREAL_1: 44;

            then c in ((B . (m1 + 1)) \ (B . m1)) by A15, XBOOLE_0:def 5;

            then

             A25: (( Rland ((F - r),B)) . c) = (( FinS ((F - r),D)) . (m1 + 1)) & (( Rland (F,B)) . c) = (( FinS (F,D)) . (m1 + 1)) by A1, A2, A6, A19, A24, Th14;

            (m1 + 1) in ( Seg ( card D)) by A2, A8, A15, FINSEQ_1:def 3;

            then

             A26: ((( card D) |-> r) . (m1 + 1)) = r by FUNCOP_1: 7;

            (m1 + 1) in ( dom ( FinS ((F - r),D))) by A2, A7, A8, A15, FINSEQ_3: 29;

            

            hence (( Rland ((F - r),B)) . c) = ((( Rland (F,B)) . c) - r) by A9, A25, A26, VALUED_1: 13

            .= ((( Rland (F,B)) - r) . c) by A3, VALUED_1: 3;

          end;

        end;

        hence (( Rland ((F - r),B)) . c) = ((( Rland (F,B)) - r) . c);

      end;

      ( dom (( Rland (F,B)) - r)) = C by A3, VALUED_1: 3;

      hence thesis by A2, A6, A10, Th12, PARTFUN1: 5;

    end;

    theorem :: REARRAN1:34

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( max+ (( Rlor (F,A)) - r)),( max+ (F - r))) are_fiberwise_equipotent & ( FinS (( max+ (( Rlor (F,A)) - r)),C)) = ( FinS (( max+ (F - r)),D)) & ( Sum (( max+ (( Rlor (F,A)) - r)),C)) = ( Sum (( max+ (F - r)),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set mp = ( max+ (( Rlor (F,B)) - r)), mf = ( max+ (F - r));

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rlor (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th23;

      then (( Rlor (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then ((( Rlor (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      hence

       A5: (mp,mf) are_fiberwise_equipotent by RFUNCT_3: 41;

      

       A6: ( dom mp) = ( dom (( Rlor (F,B)) - r)) by RFUNCT_3:def 10;

      then (mp | C) = mp by RELAT_1: 68;

      then (( FinS (mp,C)),mp) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS (mp,C)),mf) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom mf) = ( dom (F - r)) by RFUNCT_3:def 10;

      then (mf | D) = mf by RELAT_1: 68;

      hence ( FinS (mp,C)) = ( FinS (mf,D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum (mp,C)) = ( Sum ( FinS (mf,D))) by RFUNCT_3:def 14

      .= ( Sum (mf,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:35

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card C) = ( card D) holds (( max- (( Rlor (F,A)) - r)),( max- (F - r))) are_fiberwise_equipotent & ( FinS (( max- (( Rlor (F,A)) - r)),C)) = ( FinS (( max- (F - r)),D)) & ( Sum (( max- (( Rlor (F,A)) - r)),C)) = ( Sum (( max- (F - r)),D))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card C) = ( card D);

      set mp = ( max- (( Rlor (F,B)) - r)), mf = ( max- (F - r));

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      then (F | D) = F by RELAT_1: 68;

      then

       A4: (( FinS (F,D)),F) are_fiberwise_equipotent by A3, RFUNCT_3:def 13;

      (( Rlor (F,B)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th23;

      then (( Rlor (F,B)),F) are_fiberwise_equipotent by A4, CLASSES1: 76;

      then ((( Rlor (F,B)) - r),(F - r)) are_fiberwise_equipotent by RFUNCT_3: 51;

      hence

       A5: (mp,mf) are_fiberwise_equipotent by RFUNCT_3: 42;

      

       A6: ( dom mp) = ( dom (( Rlor (F,B)) - r)) by RFUNCT_3:def 11;

      then (mp | C) = mp by RELAT_1: 68;

      then (( FinS (mp,C)),mp) are_fiberwise_equipotent by A6, RFUNCT_3:def 13;

      then

       A7: (( FinS (mp,C)),mf) are_fiberwise_equipotent by A5, CLASSES1: 76;

      

       A8: ( dom mf) = ( dom (F - r)) by RFUNCT_3:def 11;

      then (mf | D) = mf by RELAT_1: 68;

      hence ( FinS (mp,C)) = ( FinS (mf,D)) by A8, A7, RFUNCT_3:def 13;

      

      hence ( Sum (mp,C)) = ( Sum ( FinS (mf,D))) by RFUNCT_3:def 14

      .= ( Sum (mf,D)) by RFUNCT_3:def 14;

    end;

    theorem :: REARRAN1:36

    

     Th35: for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) holds ( len ( FinS (( Rlor (F,A)),C))) = ( card C) & 1 <= ( len ( FinS (( Rlor (F,A)),C)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      set p = ( Rlor (F,B));

      assume F is total & ( card D) = ( card C);

      then

       A1: ( dom p) = C by Th20;

      then

       A2: (p | C) = p by RELAT_1: 68;

      hence ( len ( FinS (p,C))) = ( card C) by A1, RFUNCT_3: 67;

      ( 0 + 1) <= ( card C) by NAT_1: 13;

      hence thesis by A1, A2, RFUNCT_3: 67;

    end;

    theorem :: REARRAN1:37

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) & n in ( dom A) holds (( FinS (( Rlor (F,A)),C)) | n) = ( FinS (( Rlor (F,A)),(( Co_Gen A) . n)))

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total & ( card D) = ( card C) and

       A2: n in ( dom B);

      set p = ( Rlor (F,B)), b = ( Co_Gen B);

      

       A3: ( len ( FinS (p,C))) = ( card C) by A1, Th35;

      defpred P[ Nat] means $1 in ( dom b) implies (( FinS (( Rlor (F,B)),C)) | $1) = ( FinS (( Rlor (F,B)),(b . $1)));

      

       A4: ( dom b) = ( Seg ( len b)) by FINSEQ_1:def 3;

      

       A5: ( len b) = ( card C) by Th1;

      

       A6: ( dom ( FinS (p,C))) = ( Seg ( len ( FinS (p,C)))) by FINSEQ_1:def 3;

      

       A7: for m st P[m] holds P[(m + 1)]

      proof

        set f = ( FinS (p,C));

        let m;

        assume

         A8: P[m];

        

         A9: m <= (m + 1) by NAT_1: 11;

        assume

         A10: (m + 1) in ( dom b);

        then 1 <= (m + 1) by FINSEQ_3: 25;

        then

         A11: (m + 1) in ( Seg (m + 1)) by FINSEQ_1: 1;

        

         A12: ( dom p) = C by A1, Th20;

        

         A13: (m + 1) <= ( len b) by A10, FINSEQ_3: 25;

        then

         A14: m <= ( len b) by NAT_1: 13;

        

         A15: m < ( len b) by A13, NAT_1: 13;

        

         A16: m <= (( len b) - 1) by A13, XREAL_1: 19;

        

         A17: ( len (f | (m + 1))) = (m + 1) by A5, A3, A13, FINSEQ_1: 59;

        now

          per cases ;

            case

             A18: m = 0 ;

            consider d be Element of C such that

             A19: (b . 1) = {d} by Th9;

            

             A20: d in (b . 1) by A19, TARSKI:def 1;

            

             A21: 1 <= ( len ( FinS (p,C))) by A1, Th35;

            then 1 in ( Seg 1) & 1 in ( dom ( FinS (p,C))) by FINSEQ_1: 1, FINSEQ_3: 25;

            

            then

             A22: ((( FinS (p,C)) | (m + 1)) . 1) = (( FinS (p,C)) . 1) by A18, RFINSEQ: 6

            .= (( FinS (F,D)) . 1) by A1, Th24

            .= (p . d) by A1, A20, Th21;

            ( dom p) = C by A1, Th20;

            then

             A23: ( FinS (p,(b . (m + 1)))) = <*(p . d)*> by A18, A19, RFUNCT_3: 69;

            ( len (( FinS (p,C)) | (m + 1))) = 1 by A18, A21, FINSEQ_1: 59;

            hence thesis by A23, A22, FINSEQ_1: 40;

          end;

            case

             A24: m <> 0 ;

            

             A25: ( Seg m) c= ( Seg (m + 1)) by A9, FINSEQ_1: 5;

            

             A26: ((f | (m + 1)) | m) = ((f | (m + 1)) | ( Seg m)) by FINSEQ_1:def 15

            .= ((f | ( Seg (m + 1))) | ( Seg m)) by FINSEQ_1:def 15

            .= (f | (( Seg (m + 1)) /\ ( Seg m))) by RELAT_1: 71

            .= (f | ( Seg m)) by A25, XBOOLE_1: 28

            .= (f | m) by FINSEQ_1:def 15;

            

             A27: ( 0 + 1) <= m by A24, NAT_1: 13;

            then

            consider d be Element of C such that

             A28: ((b . (m + 1)) \ (b . m)) = {d} and (b . (m + 1)) = ((b . m) \/ {d}) and

             A29: ((b . (m + 1)) \ {d}) = (b . m) by A16, Th10;

            

             A30: d in {d} by TARSKI:def 1;

            

            then (p . d) = (( FinS (F,D)) . (m + 1)) by A1, A15, A27, A28, Th21

            .= (( FinS (p,C)) . (m + 1)) by A1, Th24

            .= ((f | (m + 1)) . (m + 1)) by A4, A6, A5, A3, A10, A11, RFINSEQ: 6;

            then

             A31: (f | (m + 1)) = ((f | m) ^ <*(p . d)*>) by A17, A26, RFINSEQ: 7;

            d in (( dom p) /\ (b . (m + 1))) by A12, A28, A30, XBOOLE_0:def 4;

            then

             A32: d in ( dom (p | (b . (m + 1)))) by RELAT_1: 61;

            

             A33: (f | (m + 1)) is non-increasing by RFINSEQ: 20;

            

             A34: ( dom (p | (b . (m + 1)))) = (( dom p) /\ (b . (m + 1))) by RELAT_1: 61

            .= (b . (m + 1)) by A10, A12, Lm5, XBOOLE_1: 28;

            (b . (m + 1)) is finite by A10, Lm5, FINSET_1: 1;

            then ((f | (m + 1)),(p | (b . (m + 1)))) are_fiberwise_equipotent by A8, A14, A27, A29, A31, A32, FINSEQ_3: 25, RFUNCT_3: 65;

            hence thesis by A34, A33, RFUNCT_3:def 13;

          end;

        end;

        hence thesis;

      end;

      

       A35: ( dom B) = ( Seg ( len B)) & ( len B) = ( card C) by Th1, FINSEQ_1:def 3;

      

       A36: P[ 0 ] by FINSEQ_3: 25;

      for m holds P[m] from NAT_1:sch 2( A36, A7);

      hence thesis by A2, A4, A35, A5;

    end;

    theorem :: REARRAN1:38

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) holds ( Rlor ((F - r),A)) = (( Rlor (F,A)) - r)

    proof

      let F be PartFunc of D, REAL , B be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card D) = ( card C);

      

       A3: ( dom ( Rlor (F,B))) = C by A1, A2, Th20;

      set b = ( Co_Gen B);

      

       A4: ( len b) = ( card C) by Th1;

      

       A5: ( dom F) = D by A1, PARTFUN1:def 2;

      then

       A6: ( dom (F - r)) = D by VALUED_1: 3;

      then

       A7: (F - r) is total by PARTFUN1:def 2;

      ((F - r) | D) = (F - r) by A6, RELAT_1: 68;

      then

       A8: ( len ( FinS ((F - r),D))) = ( card D) by A6, RFUNCT_3: 67;

      reconsider rr = r as Element of REAL by XREAL_0:def 1;

      (F | D) = F by A5, RELAT_1: 68;

      then

       A9: ( FinS ((F - r),D)) = (( FinS (F,D)) - (( card D) |-> rr)) by A5, RFUNCT_3: 73;

       A10:

      now

        let c be Element of C;

        assume c in ( dom ( Rlor ((F - r),B)));

        defpred P[ set] means $1 in ( dom b) & c in (b . $1);

        

         A11: C = (b . ( len b)) by Th3;

        ( len b) <> 0 by Th4;

        then

         A12: ( 0 + 1) <= ( len b) by NAT_1: 13;

        then

         A13: 1 in ( dom b) by FINSEQ_3: 25;

        ( len b) in ( dom b) by A12, FINSEQ_3: 25;

        then

         A14: ex n be Nat st P[n] by A11;

        consider mi be Nat such that

         A15: P[mi] & for n be Nat st P[n] holds mi <= n from NAT_1:sch 5( A14);

        

         A16: 1 <= mi by A15, FINSEQ_3: 25;

        then ( max ( 0 ,(mi - 1))) = (mi - 1) by FINSEQ_2: 4;

        then

        reconsider m1 = (mi - 1) as Element of NAT by FINSEQ_2: 5;

        

         A17: mi <= ( len b) by A15, FINSEQ_3: 25;

        

         A18: mi < (mi + 1) by NAT_1: 13;

        then m1 < mi by XREAL_1: 19;

        then

         A19: m1 < ( len b) by A17, XXREAL_0: 2;

        m1 <= mi by A18, XREAL_1: 19;

        then

         A20: m1 <= ( len b) by A17, XXREAL_0: 2;

        now

          per cases ;

            case

             A21: mi = 1;

            

             A22: 1 in ( dom ( FinS ((F - r),D))) by A2, A8, A4, A12, FINSEQ_3: 25;

            1 in ( Seg ( card D)) by A2, A4, A13, FINSEQ_1:def 3;

            then

             A23: ((( card D) |-> r) . 1) = r by FUNCOP_1: 7;

            (( Rlor ((F - r),B)) . c) = (( FinS ((F - r),D)) . 1) & (( Rlor (F,B)) . c) = (( FinS (F,D)) . 1) by A1, A2, A7, A15, A21, Th21;

            

            hence (( Rlor ((F - r),B)) . c) = ((( Rlor (F,B)) . c) - r) by A9, A22, A23, VALUED_1: 13

            .= ((( Rlor (F,B)) - r) . c) by A3, VALUED_1: 3;

          end;

            case mi <> 1;

            then 1 < mi by A16, XXREAL_0: 1;

            then (1 + 1) <= mi by NAT_1: 13;

            then

             A24: 1 <= m1 by XREAL_1: 19;

            then m1 in ( dom b) by A20, FINSEQ_3: 25;

            then not c in (b . m1) by A15, XREAL_1: 44;

            then c in ((b . (m1 + 1)) \ (b . m1)) by A15, XBOOLE_0:def 5;

            then

             A25: (( Rlor ((F - r),B)) . c) = (( FinS ((F - r),D)) . (m1 + 1)) & (( Rlor (F,B)) . c) = (( FinS (F,D)) . (m1 + 1)) by A1, A2, A7, A19, A24, Th21;

            (m1 + 1) in ( Seg ( card D)) by A2, A4, A15, FINSEQ_1:def 3;

            then

             A26: ((( card D) |-> r) . (m1 + 1)) = r by FUNCOP_1: 7;

            (m1 + 1) in ( dom ( FinS ((F - r),D))) by A2, A8, A4, A15, FINSEQ_3: 29;

            

            hence (( Rlor ((F - r),B)) . c) = ((( Rlor (F,B)) . c) - r) by A9, A25, A26, VALUED_1: 13

            .= ((( Rlor (F,B)) - r) . c) by A3, VALUED_1: 3;

          end;

        end;

        hence (( Rlor ((F - r),B)) . c) = ((( Rlor (F,B)) - r) . c);

      end;

      ( dom (( Rlor (F,B)) - r)) = C by A3, VALUED_1: 3;

      hence thesis by A2, A7, A10, Th20, PARTFUN1: 5;

    end;

    theorem :: REARRAN1:39

    for F be PartFunc of D, REAL , A be RearrangmentGen of C st F is total & ( card D) = ( card C) holds (( Rland (F,A)),F) are_fiberwise_equipotent & (( Rlor (F,A)),F) are_fiberwise_equipotent & ( rng ( Rland (F,A))) = ( rng F) & ( rng ( Rlor (F,A))) = ( rng F)

    proof

      let F be PartFunc of D, REAL , A be RearrangmentGen of C;

      assume that

       A1: F is total and

       A2: ( card D) = ( card C);

      

       A3: ( dom F) = D by A1, PARTFUN1:def 2;

      ( dom (F | D)) = (( dom F) /\ D) by RELAT_1: 61

      .= D by A3;

      then

       A4: (( FinS (F,D)),(F | D)) are_fiberwise_equipotent by RFUNCT_3:def 13;

      (( Rlor (F,A)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th23;

      then

       A5: (( Rlor (F,A)),(F | D)) are_fiberwise_equipotent by A4, CLASSES1: 76;

      (( Rland (F,A)),( FinS (F,D))) are_fiberwise_equipotent by A1, A2, Th16;

      then (( Rland (F,A)),(F | D)) are_fiberwise_equipotent by A4, CLASSES1: 76;

      hence (( Rland (F,A)),F) are_fiberwise_equipotent & (( Rlor (F,A)),F) are_fiberwise_equipotent by A3, A5, RELAT_1: 68;

      hence thesis by CLASSES1: 75;

    end;