rfinseq.miz



    begin

    reserve x,y for set,

n,m for Nat,

r,s for Real;

    registration

      let f be finite Relation, x be object;

      cluster ( Coim (f,x)) -> finite;

      coherence

      proof

        ( Coim (f,x)) c= ( dom f) by RELAT_1: 132;

        hence thesis;

      end;

    end

    theorem :: RFINSEQ:1

    

     Th1: for f,g,h be FinSequence holds (f,g) are_fiberwise_equipotent iff ((f ^ h),(g ^ h)) are_fiberwise_equipotent

    proof

      let f,g,h be FinSequence;

      thus (f,g) are_fiberwise_equipotent implies ((f ^ h),(g ^ h)) are_fiberwise_equipotent

      proof

        assume

         A1: (f,g) are_fiberwise_equipotent ;

        now

          let y be object;

          ( card ( Coim (f,y))) = ( card ( Coim (g,y))) by A1;

          

          hence ( card ( Coim ((f ^ h),y))) = (( card ( Coim (g,y))) + ( card ( Coim (h,y)))) by FINSEQ_3: 57

          .= ( card ( Coim ((g ^ h),y))) by FINSEQ_3: 57;

        end;

        hence thesis;

      end;

      assume

       A2: ((f ^ h),(g ^ h)) are_fiberwise_equipotent ;

      now

        let x be object;

        

         A3: ( card ( Coim ((f ^ h),x))) = (( card ( Coim (f,x))) + ( card ( Coim (h,x)))) & ( card ( Coim ((g ^ h),x))) = (( card ( Coim (g,x))) + ( card ( Coim (h,x)))) by FINSEQ_3: 57;

        ( card ( Coim ((f ^ h),x))) = ( card ( Coim ((g ^ h),x))) by A2;

        hence ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A3;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:2

    for f,g be FinSequence holds ((f ^ g),(g ^ f)) are_fiberwise_equipotent

    proof

      let f,g be FinSequence;

      let y be object;

      

      thus ( card ( Coim ((f ^ g),y))) = (( card (g " {y})) + ( card (f " {y}))) by FINSEQ_3: 57

      .= ( card ( Coim ((g ^ f),y))) by FINSEQ_3: 57;

    end;

    theorem :: RFINSEQ:3

    

     Th3: for f,g be FinSequence st (f,g) are_fiberwise_equipotent holds ( len f) = ( len g) & ( dom f) = ( dom g)

    proof

      let f,g be FinSequence;

      

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

      assume (f,g) are_fiberwise_equipotent ;

      then

       A2: ( card (f " ( rng f))) = ( card (g " ( rng f))) & ( rng f) = ( rng g) by CLASSES1: 75, CLASSES1: 78;

      

       A3: ( Seg ( len g)) = ( dom g) by FINSEQ_1:def 3;

      

      thus ( len f) = ( card ( Seg ( len f))) by FINSEQ_1: 57

      .= ( card (g " ( rng g))) by A1, A2, RELAT_1: 134

      .= ( card ( Seg ( len g))) by A3, RELAT_1: 134

      .= ( len g) by FINSEQ_1: 57;

      hence thesis by A1, FINSEQ_1:def 3;

    end;

    theorem :: RFINSEQ:4

    

     Th4: for f,g be FinSequence holds (f,g) are_fiberwise_equipotent iff ex P be Permutation of ( dom g) st f = (g * P)

    proof

      let f,g be FinSequence;

      thus (f,g) are_fiberwise_equipotent implies ex P be Permutation of ( dom g) st f = (g * P)

      proof

        assume

         A1: (f,g) are_fiberwise_equipotent ;

        then ( dom f) = ( dom g) by Th3;

        hence thesis by A1, CLASSES1: 80;

      end;

      given P be Permutation of ( dom g) such that

       A2: f = (g * P);

      ( dom g) = {} implies ( dom g) = {} ;

      then ( rng P) c= ( dom g) & ( dom P) = ( dom g) by FUNCT_2:def 1;

      then ( dom f) = ( dom g) by A2, RELAT_1: 27;

      hence thesis by A2, CLASSES1: 80;

    end;

    defpred P[ Nat] means for X be finite set, F be Function st ( card ( dom (F | X))) = $1 holds ex a be FinSequence st ((F | X),a) are_fiberwise_equipotent ;

    

     Lm1: P[ 0 ]

    proof

      let X be finite set, F be Function;

      assume

       A1: ( card ( dom (F | X))) = 0 ;

      take A = {} ;

      let x be object;

      ( dom (F | X)) = {} by A1;

      hence ( card ( Coim ((F | X),x))) = ( card ( Coim (A,x))) by RELAT_1: 132, XBOOLE_1: 3;

    end;

    

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

    proof

      let n be Nat;

      assume

       A1: P[n];

      let X be finite set, F be Function;

      reconsider dx = ( dom (F | X)) as finite set;

      set x = the Element of dx;

      set Y = (X \ {x}), dy = ( dom (F | Y));

      

       A2: dy = (( dom F) /\ Y) by RELAT_1: 61;

      

       A3: dx = (( dom F) /\ X) by RELAT_1: 61;

      

       A4: dy = (dx \ {x})

      proof

        thus dy c= (dx \ {x})

        proof

          let y be object;

          assume

           A5: y in dy;

          then y in (X \ {x}) by A2, XBOOLE_0:def 4;

          then

           A6: not y in {x} by XBOOLE_0:def 5;

          y in ( dom F) by A2, A5, XBOOLE_0:def 4;

          then y in dx by A2, A3, A5, XBOOLE_0:def 4;

          hence thesis by A6, XBOOLE_0:def 5;

        end;

        let y be object;

        assume

         A7: y in (dx \ {x});

        then ( not y in {x}) & y in X by A3, XBOOLE_0:def 4, XBOOLE_0:def 5;

        then

         A8: y in Y by XBOOLE_0:def 5;

        y in ( dom F) by A3, A7, XBOOLE_0:def 4;

        hence thesis by A2, A8, XBOOLE_0:def 4;

      end;

      assume

       A9: ( card ( dom (F | X))) = (n + 1);

      then {x} c= dx by CARD_1: 27, ZFMISC_1: 31;

      

      then ( card ( dom (F | Y))) = (( card dx) - ( card {x})) by A4, CARD_2: 44

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

      .= n;

      then

      consider a be FinSequence such that

       A10: ((F | Y),a) are_fiberwise_equipotent by A1;

      take A = (a ^ <*(F . x)*>);

      dx <> {} by A9;

      then x in dx;

      then

       A11: x in (( dom F) /\ X) by RELAT_1: 61;

      then x in ( dom F) by XBOOLE_0:def 4;

      then

       A12: {x} c= ( dom F) by ZFMISC_1: 31;

      x in X by A11, XBOOLE_0:def 4;

      then

       A13: {x} c= X by ZFMISC_1: 31;

      now

        let y be object;

        

         A14: Y misses {x} by XBOOLE_1: 79;

        

         A15: (((F | Y) " {y}) \/ ((F | {x}) " {y})) = ((Y /\ (F " {y})) \/ ((F | {x}) " {y})) by FUNCT_1: 70

        .= ((Y /\ (F " {y})) \/ ( {x} /\ (F " {y}))) by FUNCT_1: 70

        .= ((Y \/ {x}) /\ (F " {y})) by XBOOLE_1: 23

        .= ((X \/ {x}) /\ (F " {y})) by XBOOLE_1: 39

        .= (X /\ (F " {y})) by A13, XBOOLE_1: 12

        .= ((F | X) " {y}) by FUNCT_1: 70;

        reconsider FF = ( <*(F . x)*> " {y}) as finite set;

        

         A16: ( card ( Coim ((F | Y),y))) = ( card ( Coim (a,y))) by A10;

        

         A17: ( dom (F | {x})) = {x} by A12, RELAT_1: 62;

        

         A18: ( dom <*(F . x)*>) = {1} by FINSEQ_1: 2, FINSEQ_1: 38;

         A19:

        now

          per cases ;

            case

             A20: y = (F . x);

            

             A21: {x} c= ((F | {x}) " {y})

            proof

              let z be object;

              

               A22: y in {y} by TARSKI:def 1;

              assume

               A23: z in {x};

              then z = x by TARSKI:def 1;

              then y = ((F | {x}) . z) by A17, A20, A23, FUNCT_1: 47;

              hence thesis by A17, A23, A22, FUNCT_1:def 7;

            end;

            ((F | {x}) " {y}) c= {x} by A17, RELAT_1: 132;

            then ((F | {x}) " {y}) = {x} by A21;

            then

             A24: ( card ((F | {x}) " {y})) = 1 by CARD_1: 30;

            

             A25: {1} c= ( <*(F . x)*> " {y})

            proof

              let z be object;

              

               A26: y in {y} by TARSKI:def 1;

              assume

               A27: z in {1};

              then z = 1 by TARSKI:def 1;

              then y = ( <*(F . x)*> . z) by A20, FINSEQ_1: 40;

              hence thesis by A18, A27, A26, FUNCT_1:def 7;

            end;

            ( <*(F . x)*> " {y}) c= {1} by A18, RELAT_1: 132;

            then ( <*(F . x)*> " {y}) = {1} by A25;

            hence ( card ((F | {x}) " {y})) = ( card FF) by A24, CARD_1: 30;

          end;

            case

             A28: y <> (F . x);

             A29:

            now

              set z = the Element of ( <*(F . x)*> " {y});

              assume

               A30: ( <*(F . x)*> " {y}) <> {} ;

              then ( <*(F . x)*> . z) in {y} by FUNCT_1:def 7;

              then

               A31: ( <*(F . x)*> . z) = y by TARSKI:def 1;

              z in {1} by A18, A30, FUNCT_1:def 7;

              then z = 1 by TARSKI:def 1;

              hence contradiction by A28, A31, FINSEQ_1: 40;

            end;

            now

              set z = the Element of ((F | {x}) " {y});

              assume

               A32: ((F | {x}) " {y}) <> {} ;

              then ((F | {x}) . z) in {y} by FUNCT_1:def 7;

              then

               A33: ((F | {x}) . z) = y by TARSKI:def 1;

              

               A34: z in {x} by A17, A32, FUNCT_1:def 7;

              then z = x by TARSKI:def 1;

              hence contradiction by A17, A28, A34, A33, FUNCT_1: 47;

            end;

            hence ( card ((F | {x}) " {y})) = ( card FF) by A29;

          end;

        end;

        (((F | Y) " {y}) /\ ((F | {x}) " {y})) = ((Y /\ (F " {y})) /\ ((F | {x}) " {y})) by FUNCT_1: 70

        .= ((Y /\ (F " {y})) /\ ( {x} /\ (F " {y}))) by FUNCT_1: 70

        .= ((((F " {y}) /\ Y) /\ {x}) /\ (F " {y})) by XBOOLE_1: 16

        .= (((F " {y}) /\ (Y /\ {x})) /\ (F " {y})) by XBOOLE_1: 16

        .= ( {} /\ (F " {y})) by A14

        .= {} ;

        

        hence ( card ( Coim ((F | X),y))) = ((( card ((F | Y) " {y})) + ( card FF)) - ( card {} )) by A15, A19, CARD_2: 45

        .= ( card ( Coim (A,y))) by A16, FINSEQ_3: 57;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:5

    for F be Function, X be finite set holds ex f be FinSequence st ((F | X),f) are_fiberwise_equipotent

    proof

      let F be Function, X be finite set;

      

       A1: ( card ( dom (F | X))) = ( card ( dom (F | X)));

      for n holds P[n] from NAT_1:sch 2( Lm1, Lm2);

      hence thesis by A1;

    end;

    definition

      let n be Nat, f be FinSequence;

      :: RFINSEQ:def1

      func f /^ n -> FinSequence means

      : Def1: ( len it ) = (( len f) - n) & for m be Nat st m in ( dom it ) holds (it . m) = (f . (m + n)) if n <= ( len f)

      otherwise it = {} ;

      existence

      proof

        thus n <= ( len f) implies ex p1 be FinSequence st ( len p1) = (( len f) - n) & for m be Nat st m in ( dom p1) holds (p1 . m) = (f . (m + n))

        proof

          assume n <= ( len f);

          then

          reconsider k = (( len f) - n) as Element of NAT by NAT_1: 21;

          deffunc F( Nat) = (f . ($1 + n));

          consider p be FinSequence such that

           A1: ( len p) = k & for m be Nat st m in ( dom p) holds (p . m) = F(m) from FINSEQ_1:sch 2;

          take p;

          thus ( len p) = (( len f) - n) by A1;

          let m be Nat;

          assume m in ( dom p);

          hence thesis by A1;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence;

        thus n <= ( len f) & (( len p1) = (( len f) - n) & for m be Nat st m in ( dom p1) holds (p1 . m) = (f . (m + n))) & (( len p2) = (( len f) - n) & for m be Nat st m in ( dom p2) holds (p2 . m) = (f . (m + n))) implies p1 = p2

        proof

          assume that n <= ( len f) and

           A2: ( len p1) = (( len f) - n) and

           A3: for m be Nat st m in ( dom p1) holds (p1 . m) = (f . (m + n)) and

           A4: ( len p2) = (( len f) - n) and

           A5: for m be Nat st m in ( dom p2) holds (p2 . m) = (f . (m + n));

          

           A6: ( dom p1) = ( Seg ( len p1)) & ( Seg ( len p2)) = ( dom p2) by FINSEQ_1:def 3;

          now

            let m be Nat;

            assume

             A7: m in ( dom p1);

            then (p1 . m) = (f . (m + n)) by A3;

            hence (p1 . m) = (p2 . m) by A2, A4, A5, A6, A7;

          end;

          hence thesis by A2, A4, FINSEQ_2: 9;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let D be set, n be Nat, f be FinSequence of D;

      :: original: /^

      redefine

      func f /^ n -> FinSequence of D ;

      coherence

      proof

        set p = (f /^ n);

        per cases ;

          suppose

           A1: n <= ( len f);

          then

          reconsider k = (( len f) - n) as Element of NAT by NAT_1: 21;

          

           A2: ( len p) = k by A1, Def1;

          ( rng p) c= ( rng f)

          proof

            let x be object;

            assume x in ( rng p);

            then

            consider m be Nat such that

             A3: m in ( dom p) and

             A4: (p . m) = x by FINSEQ_2: 10;

            m <= ( len p) by A3, FINSEQ_3: 25;

            then

             A5: (m + n) <= ( len f) by A2, XREAL_1: 19;

            

             A6: m <= (m + n) by NAT_1: 11;

            1 <= m by A3, FINSEQ_3: 25;

            then 1 <= (m + n) by A6, XXREAL_0: 2;

            then

             A7: (m + n) in ( dom f) by A5, FINSEQ_3: 25;

            (p . m) = (f . (m + n)) by A1, A3, Def1;

            hence thesis by A4, A7, FUNCT_1:def 3;

          end;

          then ( rng p) c= D by XBOOLE_1: 1;

          hence thesis by FINSEQ_1:def 4;

        end;

          suppose ( len f) < n;

          then (f /^ n) = ( <*> D) by Def1;

          hence thesis;

        end;

      end;

    end

    

     Lm3: for n be Nat holds for f be FinSequence st ( len f) <= n holds (f | n) = f

    proof

      let n be Nat;

      let f be FinSequence;

      

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

      assume ( len f) <= n;

      then (f | n) = (f | ( Seg n)) & ( dom f) c= ( Seg n) by A1, FINSEQ_1: 5;

      hence thesis by RELAT_1: 68;

    end;

    theorem :: RFINSEQ:6

    

     Th6: for f be FinSequence, n,m be Nat holds n in ( dom f) & m in ( Seg n) implies ((f | n) . m) = (f . m) & m in ( dom f)

    proof

      let f be FinSequence, n,m be Nat;

      assume that

       A1: n in ( dom f) and

       A2: m in ( Seg n);

      ( dom f) = ( Seg ( len f)) & n <= ( len f) by A1, FINSEQ_1:def 3, FINSEQ_3: 25;

      then

       A4: ( Seg n) c= ( dom f) by FINSEQ_1: 5;

      

      then ( Seg n) = (( dom f) /\ ( Seg n)) by XBOOLE_1: 28

      .= ( dom (f | n)) by RELAT_1: 61;

      hence thesis by A2, A4, FUNCT_1: 47;

    end;

    theorem :: RFINSEQ:7

    

     Th7: for f be FinSequence, n be Nat st (n + 1) = ( len f) holds f = ((f | n) ^ <*(f . (n + 1))*>)

    proof

      let f be FinSequence, n be Nat;

      assume

       A1: (n + 1) = ( len f);

      set x = (f . (n + 1));

      set fn = (f | n);

      

       A3: ( len fn) = n by A1, FINSEQ_1: 59, NAT_1: 11;

      

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

      

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

       A6:

      now

        let m be Nat;

        assume

         A7: m in ( dom f);

        then

         A8: 1 <= m by A4, FINSEQ_1: 1;

        

         A9: m <= ( len f) by A4, A7, FINSEQ_1: 1;

        now

          per cases ;

            case m = ( len f);

            hence (f . m) = ((fn ^ <*x*>) . m) by A1, A3, FINSEQ_1: 42;

          end;

            case m <> ( len f);

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

            then

             A10: m <= n by NAT_1: 13;

            then 1 <= n by A8, XXREAL_0: 2;

            then

             A11: n in ( dom f) by A1, A5, FINSEQ_3: 25;

            

             A12: ( Seg ( len fn)) = ( dom fn) by FINSEQ_1:def 3;

            

             A13: m in ( dom fn) by A3, A8, A10, FINSEQ_3: 25;

            

            hence ((fn ^ <*x*>) . m) = (fn . m) by FINSEQ_1:def 7

            .= (f . m) by A3, A13, A11, A12, Th6;

          end;

        end;

        hence (f . m) = ((fn ^ <*x*>) . m);

      end;

      ( len (fn ^ <*x*>)) = (n + ( len <*x*>)) by A3, FINSEQ_1: 22

      .= ( len f) by A1, FINSEQ_1: 40;

      hence thesis by A6, FINSEQ_2: 9;

    end;

    

     Th8A: for D be non empty set, f be FinSequence of D, n be Nat holds ((f | n) ^ (f /^ n)) = f

    proof

      let D be non empty set, f be FinSequence of D, n be Nat;

      set fn = (f /^ n);

      now

        per cases ;

          case ( len f) < n;

          then (f /^ n) = ( <*> D) & (f | n) = f by Def1, Lm3;

          hence thesis by FINSEQ_1: 34;

        end;

          case

           A1: n <= ( len f);

          

           A2: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

          

           A3: ( len (f | n)) = n by A1, FINSEQ_1: 59;

          

           A4: ( len fn) = (( len f) - n) by A1, Def1;

          

          then

           A5: ( len ((f | n) ^ (f /^ n))) = (n + (( len f) - n)) by A3, FINSEQ_1: 22

          .= ( len f);

          

           A6: ( dom (f | n)) = ( Seg n) by A3, FINSEQ_1:def 3;

          now

            let m be Nat;

            assume

             A7: m in ( dom f);

            then

             A8: m <= ( len f) by A2, FINSEQ_1: 1;

            

             A9: 1 <= m by A2, A7, FINSEQ_1: 1;

            now

              per cases ;

                case

                 A10: m <= n;

                then 1 <= n by A9, XXREAL_0: 2;

                then

                 A11: n in ( dom f) by A1, FINSEQ_3: 25;

                

                 A12: m in ( Seg n) by A9, A10;

                

                hence (((f | n) ^ (f /^ n)) . m) = ((f | n) . m) by A6, FINSEQ_1:def 7

                .= (f . m) by A12, A11, Th6;

              end;

                case

                 A13: n < m;

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

                then

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

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

                then

                 A14: 1 <= k by XREAL_1: 19;

                k <= ( len fn) by A4, A8, XREAL_1: 9;

                then

                 A15: k in ( dom fn) by A14, FINSEQ_3: 25;

                

                thus (((f | n) ^ (f /^ n)) . m) = (fn . k) by A3, A5, A8, A13, FINSEQ_1: 24

                .= (f . (k + n)) by A1, A15, Def1

                .= (f . m);

              end;

            end;

            hence (((f | n) ^ (f /^ n)) . m) = (f . m);

          end;

          hence thesis by A5, FINSEQ_2: 9;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:8

    

     Th8: for f be FinSequence, n be Nat holds ((f | n) ^ (f /^ n)) = f

    proof

      let f be FinSequence, n be Nat;

      reconsider D = (( rng f) \/ {1}) as non empty set;

      f is FinSequence of D by FINSEQ_1:def 4, XBOOLE_1: 7;

      hence thesis by Th8A;

    end;

    registration

      let f be FinSequence, n be Nat;

      reduce ((f | n) ^ (f /^ n)) to f;

      reducibility by Th8;

    end

    theorem :: RFINSEQ:9

    for R1,R2 be FinSequence of REAL st (R1,R2) are_fiberwise_equipotent holds ( Sum R1) = ( Sum R2)

    proof

      let R1,R2 be FinSequence of REAL ;

      defpred P[ Nat] means for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent & ( len f) = $1 holds ( Sum f) = ( Sum g);

      assume

       A1: (R1,R2) are_fiberwise_equipotent ;

      

       A2: ( len R1) = ( len R1);

      

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

      proof

        let n;

        assume

         A4: P[n];

        let f,g be FinSequence of REAL ;

        assume that

         A5: (f,g) are_fiberwise_equipotent and

         A6: ( len f) = (n + 1);

        set a = (f . (n + 1));

        

         A7: ( rng f) = ( rng g) by A5, CLASSES1: 75;

        ( 0 qua Nat + 1) <= (n + 1) by NAT_1: 13;

        then (n + 1) in ( dom f) by A6, FINSEQ_3: 25;

        then a in ( rng g) by A7, FUNCT_1:def 3;

        then

        consider m be Nat such that

         A8: m in ( dom g) and

         A9: (g . m) = a by FINSEQ_2: 10;

        set gg = (g /^ m), gm = (g | m);

        m <= ( len g) by A8, FINSEQ_3: 25;

        then

         A10: ( len gm) = m by FINSEQ_1: 59;

        

         A11: 1 <= m by A8, FINSEQ_3: 25;

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

        then

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

        

         A12: m = (m1 + 1);

        then m1 <= m by NAT_1: 11;

        then

         A13: ( Seg m1) c= ( Seg m) by FINSEQ_1: 5;

        m in ( Seg m) by A11;

        then (gm . m) = a by A8, A9, Th6;

        then

         A14: gm = ((gm | m1) ^ <*a*>) by A10, A12, Th7;

        set fn = (f | n);

        

         A15: g = ((g | m) ^ (g /^ m));

        

         A16: (gm | m1) = (gm | ( Seg m1))

        .= ((g | ( Seg m)) | ( Seg m1))

        .= (g | (( Seg m) /\ ( Seg m1))) by RELAT_1: 71

        .= (g | ( Seg m1)) by A13, XBOOLE_1: 28

        .= (g | m1);

        

         A17: f = (fn ^ <*a*>) by A6, Th7;

        now

          let x be object;

          ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A5;

          

          then (( card (fn " {x})) + ( card ( <*a*> " {x}))) = ( card ((((g | m1) ^ <*a*>) ^ (g /^ m)) " {x})) by A14, A16, A17, FINSEQ_3: 57

          .= (( card (((g | m1) ^ <*a*>) " {x})) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ( <*a*> " {x}))) + ( card ((g /^ m) " {x}))) by FINSEQ_3: 57

          .= ((( card ((g | m1) " {x})) + ( card ((g /^ m) " {x}))) + ( card ( <*a*> " {x})))

          .= (( card (((g | m1) ^ (g /^ m)) " {x})) + ( card ( <*a*> " {x}))) by FINSEQ_3: 57;

          hence ( card ( Coim (fn,x))) = ( card ( Coim (((g | m1) ^ (g /^ m)),x)));

        end;

        then

         A18: (fn,((g | m1) ^ (g /^ m))) are_fiberwise_equipotent ;

        ( len fn) = n by A6, FINSEQ_1: 59, NAT_1: 11;

        then ( Sum fn) = ( Sum ((g | m1) ^ gg)) by A4, A18;

        

        hence ( Sum f) = (( Sum ((g | m1) ^ gg)) + ( Sum <*a*>)) by A17, RVSUM_1: 75

        .= ((( Sum (g | m1)) + ( Sum gg)) + ( Sum <*a*>)) by RVSUM_1: 75

        .= ((( Sum (g | m1)) + ( Sum <*a*>)) + ( Sum gg))

        .= (( Sum gm) + ( Sum gg)) by A14, A16, RVSUM_1: 75

        .= ( Sum g) by A15, RVSUM_1: 75;

      end;

      

       A19: P[ 0 ]

      proof

        let f,g be FinSequence of REAL ;

        assume (f,g) are_fiberwise_equipotent & ( len f) = 0 ;

        then

         A20: ( len g) = 0 & f = ( <*> REAL ) by Th3;

        then g = ( <*> REAL );

        hence thesis by A20;

      end;

      for n holds P[n] from NAT_1:sch 2( A19, A3);

      hence thesis by A1, A2;

    end;

    definition

      let R be real-valued FinSequence;

      :: RFINSEQ:def2

      func MIM (R) -> FinSequence of REAL means

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

      existence

      proof

        per cases ;

          suppose

           A1: ( len R) = 0 ;

          reconsider RR = R as FinSequence of REAL by RVSUM_1: 145;

          take a = RR;

          thus ( len a) = ( len R) & (a . ( len a)) = (R . ( len R));

          let n be Nat;

          assume 1 <= n & n <= (( len a) - 1);

          hence thesis by A1;

        end;

          suppose ( len R) <> 0 ;

          then 0 < ( len R);

          then ( 0 qua Nat + 1) <= ( len R) by NAT_1: 13;

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

          then

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

          defpred P[ Nat, object] means $2 = ((R . $1) - (R . ($1 + 1)));

          set t = (R . ( len R));

          

           A2: for n be Nat st n in ( Seg l) holds ex x be Element of REAL st P[n, x]

          proof

            let n be Nat;

            assume n in ( Seg l);

            consider x be Real such that

             A3: P[n, x];

            reconsider x as Element of REAL by XREAL_0:def 1;

            take x;

            thus thesis by A3;

          end;

          consider p be FinSequence of REAL such that

           A4: ( dom p) = ( Seg l) & for n be Nat st n in ( Seg l) holds P[n, (p . n)] from FINSEQ_1:sch 5( A2);

          reconsider t as Element of REAL by XREAL_0:def 1;

          take a = (p ^ <*t*>);

          

          thus

           A5: ( len a) = (( len p) + ( len <*t*>)) by FINSEQ_1: 22

          .= (l + ( len <*t*>)) by A4, FINSEQ_1:def 3

          .= (l + 1) by FINSEQ_1: 39

          .= ( len R);

          

          hence (a . ( len a)) = (a . (l + 1))

          .= (a . (( len p) + 1)) by A4, FINSEQ_1:def 3

          .= (R . ( len R)) by FINSEQ_1: 42;

          let n be Nat;

          assume 1 <= n & n <= (( len a) - 1);

          then

           A6: n in ( Seg l) by A5;

          then (p . n) = ((R . n) - (R . (n + 1))) by A4;

          hence thesis by A4, A6, FINSEQ_1:def 7;

        end;

      end;

      uniqueness

      proof

        let p1,p2 be FinSequence of REAL ;

        assume that

         A7: ( len p1) = ( len R) and

         A8: (p1 . ( len p1)) = (R . ( len R)) and

         A9: for n be Nat st 1 <= n & n <= (( len p1) - 1) holds (p1 . n) = ((R . n) - (R . (n + 1))) and

         A10: ( len p2) = ( len R) and

         A11: (p2 . ( len p2)) = (R . ( len R)) and

         A12: for n be Nat st 1 <= n & n <= (( len p2) - 1) holds (p2 . n) = ((R . n) - (R . (n + 1)));

        

         A13: ( dom p1) = ( Seg ( len R)) by A7, FINSEQ_1:def 3;

        now

          let n be Nat;

          set r = (R . n);

          assume

           A14: n in ( dom p1);

          then

           A15: 1 <= n by A13, FINSEQ_1: 1;

          

           A16: n <= ( len R) by A13, A14, FINSEQ_1: 1;

          now

            per cases ;

              case n = ( len R);

              hence (p1 . n) = (p2 . n) by A7, A8, A10, A11;

            end;

              case

               A17: n <> ( len R);

              set s = (R . (n + 1));

              n < ( len R) by A16, A17, XXREAL_0: 1;

              then (n + 1) <= ( len R) by NAT_1: 13;

              then

               A18: n <= (( len R) - 1) by XREAL_1: 19;

              then (p1 . n) = (r - s) by A7, A9, A15;

              hence (p1 . n) = (p2 . n) by A10, A12, A15, A18;

            end;

          end;

          hence (p1 . n) = (p2 . n);

        end;

        hence thesis by A7, A10, FINSEQ_2: 9;

      end;

    end

    theorem :: RFINSEQ:10

    

     Th10: for R be FinSequence of REAL , n be Nat st ( len R) = (n + 2) holds ( MIM (R | (n + 1))) = ((( MIM R) | n) ^ <*(R . (n + 1))*>)

    proof

      let R be FinSequence of REAL , n;

      assume that

       A1: ( len R) = (n + 2);

      set s = (R . (n + 1));

      set f1 = (R | (n + 1)), m1 = ( MIM f1), mf = ( MIM R), fn = (mf | n);

      

       A3: ( 0 qua Nat + 1) <= (n + 1) by NAT_1: 13;

      

       A4: ((n + 1) + 1) = (n + (1 + 1));

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

      then

       A5: ( Seg ( len R)) = ( dom R) & (n + 1) in ( Seg (n + 2)) by A3, FINSEQ_1:def 3;

      

       A6: ( len f1) = (n + 1) by A1, A4, FINSEQ_1: 59, NAT_1: 11;

      then

       A7: ( len ( MIM f1)) = (n + 1) by Def2;

      then

       A8: ( dom m1) = ( Seg (n + 1)) by FINSEQ_1:def 3;

      (n + 1) in ( Seg (n + 1)) by A3;

      then (f1 . (n + 1)) = s by A1, A5, Th6;

      then

       A9: (m1 . (n + 1)) = s by A6, A7, Def2;

      

       A10: ( Seg ( len fn)) = ( dom fn) by FINSEQ_1:def 3;

      

       A11: ( Seg ( len mf)) = ( dom mf) by FINSEQ_1:def 3;

      

       A12: ( len mf) = (n + 2) by A1, Def2;

      then

       A13: ( len fn) = n by FINSEQ_1: 59, NAT_1: 11;

      

       A14: n <= (n + 2) by NAT_1: 11;

       A15:

      now

        let m be Nat;

        assume

         A16: m in ( dom m1);

        then

         A17: 1 <= m by A8, FINSEQ_1: 1;

        

         A18: m <= (n + 1) by A8, A16, FINSEQ_1: 1;

        now

          per cases ;

            case m = (n + 1);

            hence (m1 . m) = ((fn ^ <*s*>) . m) by A13, A9, FINSEQ_1: 42;

          end;

            case m <> (n + 1);

            then

             A19: m < (n + 1) by A18, XXREAL_0: 1;

            then

             A20: m <= n by NAT_1: 13;

            then

             A21: m in ( Seg n) by A17;

            set r2 = (R . (m + 1));

            set r1 = (R . m);

            

             A22: (( len mf) - 1) = (n + 1) by A12;

            1 <= n by A17, A20, XXREAL_0: 2;

            then n in ( Seg (n + 2)) by A14;

            then (fn . m) = (mf . m) by A12, A11, A21, Th6;

            

            then

             A23: (r1 - r2) = (fn . m) by A17, A18, A22, Def2

            .= ((fn ^ <*s*>) . m) by A13, A10, A21, FINSEQ_1:def 7;

            1 <= (m + 1) & (m + 1) <= (n + 1) by A19, NAT_1: 11, NAT_1: 13;

            then (m + 1) in ( Seg (n + 1));

            then

             A24: (f1 . (m + 1)) = r2 by A1, A5, Th6;

            (( len m1) - 1) = n & (f1 . m) = r1 by A1, A7, A5, A8, A16, Th6;

            hence (m1 . m) = ((fn ^ <*s*>) . m) by A17, A20, A23, A24, Def2;

          end;

        end;

        hence (m1 . m) = ((fn ^ <*s*>) . m);

      end;

      ( len (fn ^ <*s*>)) = (n + ( len <*s*>)) by A13, FINSEQ_1: 22

      .= (n + 1) by FINSEQ_1: 40;

      hence thesis by A7, A15, FINSEQ_2: 9;

    end;

    theorem :: RFINSEQ:11

    

     Th11: for R be FinSequence of REAL , r,s be Real, n be Nat st ( len R) = (n + 2) & (R . (n + 1)) = r & (R . (n + 2)) = s holds ( MIM R) = ((( MIM R) | n) ^ <*(r - s), s*>)

    proof

      let R be FinSequence of REAL , r, s, n;

      set mf = ( MIM R), nf = (mf | n);

      assume that

       A1: ( len R) = (n + 2) and

       A2: (R . (n + 1)) = r and

       A3: (R . (n + 2)) = s;

      

       A4: ( len mf) = (n + 2) by A1, Def2;

      then

       A5: ( dom mf) = ( Seg (n + 2)) by FINSEQ_1:def 3;

      

       A6: (n + (1 + 1)) = ((n + 1) + 1);

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

      then

       A7: n < (n + 2) by NAT_1: 13;

      

       A8: ( len nf) = n by A4, FINSEQ_1: 59, NAT_1: 11;

      then ( len (nf ^ <*(r - s), s*>)) = (n + ( len <*(r - s), s*>)) by FINSEQ_1: 22;

      then

       A9: ( len (nf ^ <*(r - s), s*>)) = (n + 2) by FINSEQ_1: 44;

      

       A10: n <= (n + 2) by NAT_1: 11;

      now

        let m be Nat;

        assume

         A11: m in ( dom mf);

        then

         A12: 1 <= m by A5, FINSEQ_1: 1;

        

         A13: m <= (n + 2) by A5, A11, FINSEQ_1: 1;

        now

          per cases ;

            case

             A14: m = (n + 2);

            

            hence (mf . m) = s by A1, A3, A4, Def2

            .= ( <*(r - s), s*> . ((n + 2) - n)) by FINSEQ_1: 44

            .= ((nf ^ <*(r - s), s*>) . m) by A8, A9, A7, A14, FINSEQ_1: 24;

          end;

            case m <> (n + 2);

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

            then

             A15: m <= (n + 1) by A6, NAT_1: 13;

            

             A16: (( len mf) - 1) = (n + 1) by A4;

            now

              per cases ;

                case

                 A17: m = (n + 1);

                then

                 A18: n < m by NAT_1: 13;

                

                thus (mf . m) = (r - s) by A2, A3, A6, A12, A16, A17, Def2

                .= ( <*(r - s), s*> . ((n + 1) - n)) by FINSEQ_1: 44

                .= ((nf ^ <*(r - s), s*>) . m) by A8, A9, A13, A17, A18, FINSEQ_1: 24;

              end;

                case m <> (n + 1);

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

                then

                 A19: m <= n by NAT_1: 13;

                then

                 A20: m in ( Seg n) by A12;

                1 <= n by A12, A19, XXREAL_0: 2;

                then

                 A21: n in ( Seg (n + 2)) by A10;

                

                 A22: ( dom nf) = ( Seg ( len nf)) by FINSEQ_1:def 3;

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

                

                hence (mf . m) = (nf . m) by A4, A20, A21, Th6

                .= ((nf ^ <*(r - s), s*>) . m) by A8, A20, A22, FINSEQ_1:def 7;

              end;

            end;

            hence (mf . m) = ((nf ^ <*(r - s), s*>) . m);

          end;

        end;

        hence (mf . m) = ((nf ^ <*(r - s), s*>) . m);

      end;

      hence thesis by A4, A9, FINSEQ_2: 9;

    end;

    theorem :: RFINSEQ:12

    

     Th12: ( MIM ( <*> REAL )) = ( <*> REAL )

    proof

      set o = ( <*> REAL ), mo = ( MIM o);

      ( len mo) = ( len o) by Def2;

      hence thesis;

    end;

    theorem :: RFINSEQ:13

    

     Th13: for r be Real holds ( MIM <*r*>) = <*r*>

    proof

      let r be Real;

      set f = <*r*>;

      

       A1: ( len f) = 1 by FINSEQ_1: 40;

      then

       A2: ( len ( MIM f)) = 1 by Def2;

      then

       A3: ( dom ( MIM f)) = ( Seg 1) by FINSEQ_1:def 3;

      now

        let n be Nat;

        assume n in ( dom ( MIM f));

        then n = 1 by A3, FINSEQ_1: 2, TARSKI:def 1;

        hence (( MIM f) . n) = (f . n) by A1, A2, Def2;

      end;

      hence thesis by A1, A2, FINSEQ_2: 9;

    end;

    theorem :: RFINSEQ:14

    for r,s be Real holds ( MIM <*r, s*>) = <*(r - s), s*>

    proof

      let r,s be Real;

      reconsider r, s as Element of REAL by XREAL_0:def 1;

      set f = <*r, s*>;

      

       A1: ( len f) = 2 & (f . 1) = r by FINSEQ_1: 44;

      

       A2: (f . 2) = s by FINSEQ_1: 44;

      ( 0 qua Nat + 2) = 2 & ( 0 qua Nat + 1) = 1;

      then ( MIM f) = ((( MIM f) | 0 ) ^ <*(r - s), s*>) by A1, A2, Th11;

      hence thesis by FINSEQ_1: 34;

    end;

    theorem :: RFINSEQ:15

    for R be FinSequence of REAL , n be Nat holds (( MIM R) /^ n) = ( MIM (R /^ n))

    proof

      let R be FinSequence of REAL , n;

      set mf = ( MIM R), fn = (R /^ n), mn = ( MIM fn);

      

       A1: ( len mf) = ( len R) by Def2;

      

       A2: ( len mn) = ( len fn) by Def2;

      now

        per cases ;

          case

           A3: ( len R) < n;

          then (mf /^ n) = ( <*> REAL ) by A1, Def1;

          hence thesis by A3, Def1, Th12;

        end;

          case

           A4: n <= ( len R);

          then

           A5: ( len (mf /^ n)) = (( len R) - n) by A1, Def1;

          

           A6: ( len mn) = ( len fn) by Def2;

          then

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

          

           A8: ( Seg ( len (mf /^ n))) = ( dom (mf /^ n)) by FINSEQ_1:def 3;

          

           A9: ( len fn) = (( len R) - n) by A4, Def1;

          

           A10: ( Seg ( len fn)) = ( dom fn) by FINSEQ_1:def 3;

          now

            let m be Nat;

            set r1 = (R . (m + n));

            assume

             A11: m in ( dom mn);

            then

             A12: 1 <= m by A7, FINSEQ_1: 1;

            

             A13: m <= ( len fn) by A7, A11, FINSEQ_1: 1;

            

             A14: (fn . m) = r1 by A4, A10, A7, A11, Def1;

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

            then

             A15: 1 <= (m + n) by A12, XXREAL_0: 2;

            now

              per cases ;

                case

                 A16: m = ( len fn);

                

                thus ((mf /^ n) . m) = (mf . (m + n)) by A1, A4, A5, A9, A8, A7, A11, Def1

                .= r1 by A1, A9, A16, Def2

                .= (mn . m) by A6, A14, A16, Def2;

              end;

                case m <> ( len fn);

                then m < ( len fn) by A13, XXREAL_0: 1;

                then

                 A17: (m + 1) <= ( len fn) by NAT_1: 13;

                then

                 A18: m <= (( len fn) - 1) by XREAL_1: 19;

                set r2 = (R . ((m + 1) + n));

                

                 A19: ((m + 1) + n) = ((m + n) + 1);

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

                then (m + 1) in ( dom fn) by A17, FINSEQ_3: 25;

                then

                 A20: (fn . (m + 1)) = r2 by A4, Def1;

                ((m + 1) + n) <= ( len R) by A9, A17, XREAL_1: 19;

                then

                 A21: (m + n) <= (( len R) - 1) by A19, XREAL_1: 19;

                

                thus ((mf /^ n) . m) = (mf . (m + n)) by A1, A4, A5, A9, A8, A7, A11, Def1

                .= (r1 - r2) by A1, A15, A19, A21, Def2

                .= (mn . m) by A2, A12, A14, A18, A20, Def2;

              end;

            end;

            hence ((mf /^ n) . m) = (mn . m);

          end;

          hence thesis by A5, A9, A6, FINSEQ_2: 9;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:16

    

     Th16: for R be FinSequence of REAL st ( len R) <> 0 holds ( Sum ( MIM R)) = (R . 1)

    proof

      defpred P[ Nat] means for R be FinSequence of REAL st ( len R) <> 0 & ( len R) = $1 holds ( Sum ( MIM R)) = (R . 1);

      let R be FinSequence of REAL ;

      assume

       A1: ( len R) <> 0 ;

      

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

      proof

        let n;

        assume

         A3: P[n];

        let R be FinSequence of REAL ;

        assume that ( len R) <> 0 and

         A4: ( len R) = (n + 1);

        now

          per cases ;

            case

             A5: n = 0 ;

            

             A6: (R . 1) in REAL by XREAL_0:def 1;

            

             A7: R = <*(R . 1)*> by A4, A5, FINSEQ_1: 40;

            then ( MIM R) = R by Th13;

            hence thesis by A7, A6, FINSOP_1: 11;

          end;

            case n <> 0 ;

            then 0 < n;

            then ( 0 qua Nat + 1) <= n by NAT_1: 13;

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

            then

            reconsider n1 = (n - 1) as Element of NAT by FINSEQ_2: 5;

            

             A8: ( 0 qua Nat + 1) <= (n1 + 1) by NAT_1: 11;

            then

             A9: ( Seg ( len R)) = ( dom R) & 1 in ( Seg (n1 + 1)) by FINSEQ_1:def 3;

            (n1 + 2) = ((n1 + 1) + 1);

            then (n1 + 1) <= (n1 + 2) by NAT_1: 11;

            then

             A10: (n1 + 1) in ( Seg (n1 + 2)) by A8;

            set f1 = (R | (n1 + 1));

            set s = (R . (n1 + 2));

            set r = (R . (n1 + 1));

            

             A11: (n1 + 2) = ( len R) by A4;

            

             A12: ( len f1) = (n1 + 1) by A4, FINSEQ_1: 59, NAT_1: 11;

            

            thus ( Sum ( MIM R)) = ( Sum ((( MIM R) | n1) ^ <*(r - s), s*>)) by A4, Th11

            .= (( Sum (( MIM R) | n1)) + ( Sum <*(r - s), s*>)) by RVSUM_1: 75

            .= (( Sum (( MIM R) | n1)) + ((r - s) + s)) by RVSUM_1: 77

            .= ( Sum ((( MIM R) | n1) ^ <*r*>)) by RVSUM_1: 74

            .= ( Sum ( MIM f1)) by A11, Th10

            .= (f1 . 1) by A3, A12

            .= (R . 1) by A4, A10, A9, Th6;

          end;

        end;

        hence thesis;

      end;

      

       A13: P[ 0 ];

      for n holds P[n] from NAT_1:sch 2( A13, A2);

      hence thesis by A1;

    end;

    theorem :: RFINSEQ:17

    for R be FinSequence of REAL , n be Nat st n < ( len R) holds ( Sum ( MIM (R /^ n))) = (R . (n + 1))

    proof

      let R be FinSequence of REAL , n;

      assume

       A1: n < ( len R);

      then

       A2: ( len (R /^ n)) = (( len R) - n) by Def1;

      (n + 1) <= ( len R) by A1, NAT_1: 13;

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

      then

       A3: 1 in ( dom (R /^ n)) by A2, FINSEQ_3: 25;

      ( len (R /^ n)) <> 0 by A1, A2;

      

      hence ( Sum ( MIM (R /^ n))) = ((R /^ n) . 1) by Th16

      .= (R . (n + 1)) by A1, A3, Def1;

    end;

    definition

      let IT be real-valued FinSequence;

      :: original: non-increasing

      redefine

      :: RFINSEQ:def3

      attr IT is non-increasing means

      : Def3: for n be Nat st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) >= (IT . (n + 1));

      compatibility

      proof

        thus IT is non-increasing implies for n be Nat st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) >= (IT . (n + 1))

        proof

          assume

           A1: IT is non-increasing;

          let n be Nat such that

           A2: n in ( dom IT) & (n + 1) in ( dom IT);

          (n + 0 qua Nat) <= (n + 1) by XREAL_1: 6;

          hence thesis by A1, A2;

        end;

        assume

         A3: for n be Nat st n in ( dom IT) & (n + 1) in ( dom IT) holds (IT . n) >= (IT . (n + 1));

        let m,n be Nat such that

         A4: m in ( dom IT) and

         A5: n in ( dom IT) & m <= n;

        defpred P[ Nat] means $1 in ( dom IT) & m <= $1 implies (IT . m) >= (IT . $1);

        

         A6: for k be Nat st P[k] holds P[(k + 1)]

        proof

          let k be Nat such that

           A7: P[k] and

           A8: (k + 1) in ( dom IT);

          assume m <= (k + 1);

          then

           A9: m < (k + 1) or m = (k + 1) by XXREAL_0: 1;

          per cases by A9, NAT_1: 13;

            suppose

             A10: m <= k;

            (k + 0 qua Nat) <= (k + 1) & (k + 1) <= ( len IT) by A8, FINSEQ_3: 25, XREAL_1: 6;

            then

             A11: k <= ( len IT) by XXREAL_0: 2;

            1 <= m by A4, FINSEQ_3: 25;

            then

             A12: 1 <= k by A10, XXREAL_0: 2;

            then k in ( dom IT) by A11, FINSEQ_3: 25;

            then (IT . k) >= (IT . (k + 1)) by A3, A8;

            hence thesis by A7, A10, A12, A11, FINSEQ_3: 25, XXREAL_0: 2;

          end;

            suppose m = (k + 1);

            hence thesis;

          end;

        end;

        

         A13: P[ 0 ] by FINSEQ_3: 24;

        for k be Nat holds P[k] from NAT_1:sch 2( A13, A6);

        hence thesis by A5;

      end;

    end

    registration

      cluster non-increasing for FinSequence of REAL ;

      existence

      proof

        take ( <*> REAL );

        let n;

        thus thesis;

      end;

    end

    theorem :: RFINSEQ:18

    

     Th18: for R be FinSequence of REAL st ( len R) = 0 or ( len R) = 1 holds R is non-increasing

    proof

      let R be FinSequence of REAL ;

      assume

       A1: ( len R) = 0 or ( len R) = 1;

      now

        per cases by A1;

          case ( len R) = 0 ;

          then R = ( <*> REAL );

          then for n st n in ( dom R) & (n + 1) in ( dom R) holds (R . n) >= (R . (n + 1));

          hence thesis;

        end;

          case ( len R) = 1;

          then

           A2: ( dom R) = {1} by FINSEQ_1: 2, FINSEQ_1:def 3;

          now

            let n;

            assume that

             A3: n in ( dom R) and

             A4: (n + 1) in ( dom R);

            n = 1 by A2, A3, TARSKI:def 1;

            hence (R . n) >= (R . (n + 1)) by A2, A4, TARSKI:def 1;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:19

    

     Th19: for R be FinSequence of REAL holds R is non-increasing iff for n,m be Nat st n in ( dom R) & m in ( dom R) & n < m holds (R . n) >= (R . m)

    proof

      let R be FinSequence of REAL ;

      thus R is non-increasing implies for n,m be Nat st n in ( dom R) & m in ( dom R) & n < m holds (R . n) >= (R . m);

      assume

       A1: for n,m be Nat st n in ( dom R) & m in ( dom R) & n < m holds (R . n) >= (R . m);

      let n;

      

       A2: n < (n + 1) by NAT_1: 13;

      assume n in ( dom R) & (n + 1) in ( dom R);

      hence thesis by A1, A2;

    end;

    theorem :: RFINSEQ:20

    

     Th20: for R be non-increasing FinSequence of REAL , n holds (R | n) is non-increasing FinSequence of REAL

    proof

      let f be non-increasing FinSequence of REAL , n;

      set fn = (f | n);

      now

        per cases ;

          case n = 0 ;

          then ( len fn) = 0 ;

          hence thesis by Th18;

        end;

          case n <> 0 ;

          then 0 < n;

          then

           A1: ( 0 qua Nat + 1) <= n by NAT_1: 13;

          now

            per cases ;

              case ( len f) <= n;

              hence thesis by Lm3;

            end;

              case n < ( len f);

              then

               A2: n in ( dom f) & ( len fn) = n by A1, FINSEQ_1: 59, FINSEQ_3: 25;

              now

                let m;

                

                 A3: ( dom fn) = ( Seg ( len fn)) by FINSEQ_1:def 3;

                assume

                 A4: m in ( dom fn) & (m + 1) in ( dom fn);

                then

                 A5: m in ( dom f) & (m + 1) in ( dom f) by A2, A3, Th6;

                (f . m) = (fn . m) & (f . (m + 1)) = (fn . (m + 1)) by A2, A4, A3, Th6;

                hence (fn . m) >= (fn . (m + 1)) by A5, Def3;

              end;

              hence thesis by Def3;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:21

    for R be non-increasing FinSequence of REAL , n be Element of NAT holds (R /^ n) is non-increasing

    proof

      let f be non-increasing FinSequence of REAL , n;

      set fn = (f /^ n);

      now

        let m;

        assume that

         A1: m in ( dom fn) and

         A2: (m + 1) in ( dom fn);

        

         A3: m <= (m + n) by NAT_1: 11;

        1 <= m by A1, FINSEQ_3: 25;

        then

         A4: 1 <= (m + n) by A3, XXREAL_0: 2;

        

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

        

         A6: (m + 1) <= ( len fn) by A2, FINSEQ_3: 25;

        set r = (fn . m), s = (fn . (m + 1));

        

         A7: ((m + 1) + n) = ((m + n) + 1);

        

         A8: m <= ( len fn) by A1, FINSEQ_3: 25;

        now

          per cases ;

            case

             A9: n <= ( len f);

            then

             A10: ( len fn) = (( len f) - n) by Def1;

            then (m + n) <= ( len f) by A8, XREAL_1: 19;

            then

             A11: (m + n) in ( dom f) by A4, FINSEQ_3: 25;

            ((m + n) + 1) <= ( len f) by A6, A7, A10, XREAL_1: 19;

            then

             A12: ((m + n) + 1) in ( dom f) by A5, FINSEQ_3: 25;

            r = (f . (m + n)) & s = (f . ((m + n) + 1)) by A1, A2, A7, A9, Def1;

            hence r >= s by A11, A12, Def3;

          end;

            case ( len f) < n;

            then fn = ( <*> REAL ) by Def1;

            hence r >= s;

          end;

        end;

        hence r >= s;

      end;

      hence thesis;

    end;

    

     Lm4: for f,g be non-increasing FinSequence of REAL , n st ( len f) = (n + 1) & ( len f) = ( len g) & (f,g) are_fiberwise_equipotent holds (f . ( len f)) = (g . ( len g)) & ((f | n),(g | n)) are_fiberwise_equipotent

    proof

      let f,g be non-increasing FinSequence of REAL , n;

      assume that

       A1: ( len f) = (n + 1) and

       A2: ( len f) = ( len g) and

       A3: (f,g) are_fiberwise_equipotent ;

      set r = (f . (n + 1)), s = (g . (n + 1));

      

       A4: ( 0 qua Nat + 1) <= (n + 1) by NAT_1: 13;

      then

       A5: (n + 1) in ( dom f) by A1, FINSEQ_3: 25;

      

       A6: f = ((f | n) ^ <*r*>) by A1, Th7;

      

       A7: (n + 1) in ( dom g) by A1, A2, A4, FINSEQ_3: 25;

       A8:

      now

        

         A9: ( rng f) = ( rng g) by A3, CLASSES1: 75;

        assume

         A10: r <> s;

        now

          per cases by A10, XXREAL_0: 1;

            case

             A11: r > s;

            s in ( rng f) by A7, A9, FUNCT_1:def 3;

            then

            consider m be Nat such that

             A12: m in ( dom f) and

             A13: (f . m) = s by FINSEQ_2: 10;

            

             A14: m <= ( len f) by A12, FINSEQ_3: 25;

            now

              per cases ;

                case m = ( len f);

                hence contradiction by A1, A11, A13;

              end;

                case m <> ( len f);

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

                hence contradiction by A5, A11, A12, A13, Th19;

              end;

            end;

            hence contradiction;

          end;

            case

             A15: r < s;

            r in ( rng g) by A5, A9, FUNCT_1:def 3;

            then

            consider m be Nat such that

             A16: m in ( dom g) and

             A17: (g . m) = r by FINSEQ_2: 10;

            

             A18: m <= ( len g) by A16, FINSEQ_3: 25;

            now

              per cases ;

                case m = ( len g);

                hence contradiction by A1, A2, A15, A17;

              end;

                case m <> ( len g);

                then m < (n + 1) by A1, A2, A18, XXREAL_0: 1;

                hence contradiction by A7, A15, A16, A17, Th19;

              end;

            end;

            hence contradiction;

          end;

        end;

        hence contradiction;

      end;

      hence (f . ( len f)) = (g . ( len g)) by A1, A2;

      

       A19: g = ((g | n) ^ <*r*>) by A1, A2, A8, Th7;

      now

        let x be object;

        (( card ( Coim ((f | n),x))) + ( card ( <*r*> " {x}))) = ( card ( Coim (f,x))) by A6, FINSEQ_3: 57

        .= ( card ( Coim (g,x))) by A3

        .= (( card ( Coim ((g | n),x))) + ( card ( <*r*> " {x}))) by A19, FINSEQ_3: 57;

        hence ( card ( Coim ((f | n),x))) = ( card ( Coim ((g | n),x)));

      end;

      hence thesis;

    end;

    defpred P[ Nat] means for R be FinSequence of REAL st $1 = ( len R) holds ex b be non-increasing FinSequence of REAL st (R,b) are_fiberwise_equipotent ;

    

     Lm5: P[ 0 ]

    proof

      let R be FinSequence of REAL ;

      assume ( len R) = 0 ;

      then

      reconsider a = R as non-increasing FinSequence of REAL by Th18;

      take a;

      thus thesis;

    end;

    

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

    proof

      let n;

      assume

       A1: P[n];

      let R be FinSequence of REAL ;

      set fn = (R | ( Seg n));

      

       A2: fn = (R | n);

      set q = (R . (n + 1));

      reconsider fn as FinSequence by FINSEQ_1: 15;

      ( rng fn) c= ( rng R) by RELAT_1: 70;

      then ( rng fn) c= REAL by XBOOLE_1: 1;

      then

      reconsider fn as FinSequence of REAL by FINSEQ_1:def 4;

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

      then

       A3: ( dom fn) = (( dom R) /\ ( Seg n)) & ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5, RELAT_1: 61;

      

       A4: n in NAT by ORDINAL1:def 12;

      assume

       A5: (n + 1) = ( len R);

      then ( dom R) = ( Seg (n + 1)) by FINSEQ_1:def 3;

      then ( dom fn) = ( Seg n) by A3, XBOOLE_1: 28;

      then

       A6: ( len fn) = n by FINSEQ_1:def 3, A4;

      then

      consider a be non-increasing FinSequence of REAL such that

       A7: (fn,a) are_fiberwise_equipotent by A1;

      

       A8: ( len fn) = ( len a) by A7, Th3;

      

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

      now

        per cases ;

          case

           A10: for t be Real st t in ( rng a) holds q <= t;

          set b = (a ^ <*q*>);

          

           A11: ( len b) = (n + ( len <*q*>)) by A6, A8, FINSEQ_1: 22

          .= (n + 1) by FINSEQ_1: 39;

          now

            let m;

            assume that

             A12: m in ( dom b) and

             A13: (m + 1) in ( dom b);

            

             A14: 1 <= (m + 1) by A13, FINSEQ_3: 25;

            set r = (b . m), s = (b . (m + 1));

            

             A15: 1 <= m by A12, FINSEQ_3: 25;

            

             A16: (m + 1) <= ( len b) by A13, FINSEQ_3: 25;

            then m <= ((n + 1) - 1) by A11, XREAL_1: 19;

            then m in ( Seg n) by A15;

            then

             A17: m in ( dom a) by A6, A8, FINSEQ_1:def 3;

            then

             A18: r = (a . m) by FINSEQ_1:def 7;

            

             A19: (a . m) in ( rng a) by A17, FUNCT_1:def 3;

            reconsider b as FinSequence of REAL by RVSUM_1: 145;

            per cases ;

              suppose (m + 1) = ( len b);

              then s = q by A6, A8, A11, FINSEQ_1: 42;

              hence r >= s by A10, A18, A19;

            end;

              suppose (m + 1) <> ( len b);

              then (m + 1) < ( len b) by A16, XXREAL_0: 1;

              then (m + 1) <= ((n + 1) - 1) by A11, NAT_1: 13;

              then (m + 1) in ( Seg n) by A14;

              then

               A20: (m + 1) in ( dom a) by A6, A8, FINSEQ_1:def 3;

              then (a . (m + 1)) = s by FINSEQ_1:def 7;

              hence r >= s by A17, A18, A20, Def3;

            end;

          end;

          then

          reconsider b as non-increasing FinSequence of REAL by Def3, RVSUM_1: 145;

          take b;

          (fn ^ <*q*>) = R by A5, A2, Th7;

          hence (R,b) are_fiberwise_equipotent by A7, Th1;

        end;

          case

           A21: ex t be Real st t in ( rng a) & not q <= t;

          defpred Q[ Nat] means $1 in ( dom a) & for r st r = (a . $1) holds r < q;

          

           A22: ex k be Nat st Q[k]

          proof

            consider t be Real such that

             A23: t in ( rng a) and

             A24: t < q by A21;

            consider k be Nat such that

             A25: k in ( dom a) and

             A26: (a . k) = t by A23, FINSEQ_2: 10;

            reconsider k as Element of NAT by ORDINAL1:def 12;

            take k;

            thus k in ( dom a) by A25;

            let r;

            assume r = (a . k);

            hence thesis by A24, A26;

          end;

          consider mi be Nat such that

           A27: Q[mi] & for m be Nat st Q[m] holds mi <= m from NAT_1:sch 5( A22);

          1 <= mi by A27, FINSEQ_3: 25;

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

          then

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

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

          then

           A28: k <= mi by XREAL_1: 19;

          

           A29: mi <= ( len a) by A27, FINSEQ_3: 25;

          then

           A30: k <= ( len a) by A28, XXREAL_0: 2;

          then

           A31: ( len (a /^ k)) = (( len a) - k) by Def1;

          

           A32: ( dom ((a | k) ^ <*q*>)) = ( Seg ( len ((a | k) ^ <*q*>))) by FINSEQ_1:def 3;

          

           A33: ( dom (a | k)) c= ( dom ((a | k) ^ <*q*>)) by FINSEQ_1: 26;

          set ak = (a /^ k), b = (((a | k) ^ <*q*>) ^ ak);

          

           A34: ( dom (a | k)) = ( Seg ( len (a | k))) by FINSEQ_1:def 3;

          

           A35: ( len (a | k)) = k by A29, A28, FINSEQ_1: 59, XXREAL_0: 2;

          

          then

           A36: ( len ((a | k) ^ <*q*>)) = (k + ( len <*q*>)) by FINSEQ_1: 22

          .= (k + 1) by FINSEQ_1: 39;

          then

           A37: ( len b) = ((k + 1) + ( len (a /^ k))) by FINSEQ_1: 22;

          (k + 1) <= ( len a) by A27, FINSEQ_3: 25;

          then

           A38: 1 <= ( len (a /^ k)) by A31, XREAL_1: 19;

          now

            let m;

            assume that

             A39: m in ( dom b) and

             A40: (m + 1) in ( dom b);

            

             A41: 1 <= (m + 1) by A40, FINSEQ_3: 25;

            

             A42: (m + 1) <= ( len b) by A40, FINSEQ_3: 25;

            set r = (b . m), s = (b . (m + 1));

            

             A43: 1 <= m by A39, FINSEQ_3: 25;

            

             A44: m <= ( len b) by A39, FINSEQ_3: 25;

            now

              per cases ;

                case

                 A45: (m + 1) <= k;

                ( dom (a | k)) c= ( dom ((a | k) ^ (a /^ k))) by FINSEQ_1: 26;

                then

                 A46: ( dom (a | k)) c= ( dom a);

                

                 A47: ( dom a) = ( Seg ( len a)) by FINSEQ_1:def 3;

                m <= k by A45, NAT_1: 13;

                then

                 A48: m in ( Seg k) by A43;

                1 <= k by A41, A45, XXREAL_0: 2;

                then

                 A49: k in ( dom a) by A30, A47;

                then

                 A50: (a . m) = ((a | k) . m) by A48, Th6;

                

                 A51: (m + 1) in ( Seg k) by A41, A45;

                then

                 A52: (a . (m + 1)) = ((a | k) . (m + 1)) by A49, Th6;

                

                 A53: (b . (m + 1)) = (((a | k) ^ <*q*>) . (m + 1)) by A35, A34, A33, A51, FINSEQ_1:def 7

                .= (a . (m + 1)) by A35, A34, A51, A52, FINSEQ_1:def 7;

                (b . m) = (((a | k) ^ <*q*>) . m) by A35, A34, A33, A48, FINSEQ_1:def 7

                .= (a . m) by A35, A34, A48, A50, FINSEQ_1:def 7;

                hence r >= s by A35, A34, A48, A51, A53, A46, Def3;

              end;

                case k < (m + 1);

                then

                 A54: k <= m by NAT_1: 13;

                now

                  per cases ;

                    case

                     A55: k = m;

                    then (m + 1) in ( dom ((a | k) ^ <*q*>)) by A36, A32, FINSEQ_1: 4;

                    

                    then

                     A56: (b . (m + 1)) = (((a | k) ^ <*q*>) . (k + 1)) by A55, FINSEQ_1:def 7

                    .= q by A35, FINSEQ_1: 42;

                    

                     A57: m in ( Seg k) by A43, A55;

                    

                     A58: k in ( dom a) by A9, A30, A43, A55;

                    then

                     A59: (a . m) = ((a | k) . m) by A57, Th6;

                    

                     A60: (b . m) = (((a | k) ^ <*q*>) . m) by A35, A34, A33, A57, FINSEQ_1:def 7

                    .= (a . m) by A35, A34, A57, A59, FINSEQ_1:def 7;

                    now

                      assume s > r;

                      then for t be Real st t = (a . k) holds t < q by A55, A60, A56;

                      then mi <= k by A27, A58;

                      hence contradiction by XREAL_1: 44;

                    end;

                    hence r >= s;

                  end;

                    case k <> m;

                    then k < m by A54, XXREAL_0: 1;

                    then

                     A61: (k + 1) <= m by NAT_1: 13;

                    then

                     A62: (k + 1) < (m + 1) by NAT_1: 13;

                    ( max ( 0 ,(m - (k + 1)))) = (m - (k + 1)) by A61, FINSEQ_2: 4;

                    then

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

                    

                     A63: (l + 1) = ((m + 1) - (k + 1));

                    then

                     A64: (l + 1) <= (( len b) - (k + 1)) by A42, XREAL_1: 13;

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

                    then

                     A65: l <= ( len (a /^ k)) by A37, A64, XXREAL_0: 2;

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

                    then

                     A66: (l + 1) in ( dom (a /^ k)) by A37, A64, FINSEQ_3: 25;

                    1 <= ((l + 1) + k) by A39, FINSEQ_3: 25;

                    then

                     A67: ((k + l) + 1) <= ( len a) by A31, A37, A64, XREAL_1: 19;

                    then

                     A68: ((k + l) + 1) in ( dom a) by A43, FINSEQ_3: 25;

                    (k + l) <= ((k + l) + 1) by NAT_1: 11;

                    then

                     A69: (k + l) <= ( len a) by A67, XXREAL_0: 2;

                    

                     A70: (k + (l + 1)) <= ( len a) by A31, A37, A64, XREAL_1: 19;

                    now

                      per cases ;

                        case

                         A71: (k + 1) = m;

                        then m in ( Seg (k + 1)) by A43;

                        

                        then

                         A72: (b . m) = (((a | k) ^ <*q*>) . (k + 1)) by A36, A32, A71, FINSEQ_1:def 7

                        .= q by A35, FINSEQ_1: 42;

                        

                         A73: 1 in ( dom (a /^ k)) by A38, FINSEQ_3: 25;

                        (b . (m + 1)) = ((a /^ k) . (((k + 1) + 1) - (k + 1))) by A36, A42, A62, A71, FINSEQ_1: 24

                        .= (a . mi) by A30, A73, Def1;

                        hence r >= s by A27, A72;

                      end;

                        case (k + 1) <> m;

                        then

                         A74: (k + 1) < m by A61, XXREAL_0: 1;

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

                        then

                         A75: 1 <= l by XREAL_1: 19;

                        then

                         A76: l in ( dom (a /^ k)) by A65, FINSEQ_3: 25;

                        l <= (k + l) by NAT_1: 11;

                        then 1 <= (k + l) by A75, XXREAL_0: 2;

                        then

                         A77: (k + l) in ( dom a) by A69, FINSEQ_3: 25;

                        

                         A78: (b . m) = ((a /^ k) . l) by A36, A44, A74, FINSEQ_1: 24

                        .= (a . (k + l)) by A30, A76, Def1;

                        (b . (m + 1)) = ((a /^ k) . (l + 1)) by A36, A42, A62, A63, FINSEQ_1: 24

                        .= (a . ((k + l) + 1)) by A30, A66, A70, Def1;

                        hence r >= s by A68, A78, A77, Def3;

                      end;

                    end;

                    hence r >= s;

                  end;

                end;

                hence r >= s;

              end;

            end;

            hence r >= s;

          end;

          then

          reconsider b as non-increasing FinSequence of REAL by Def3, RVSUM_1: 145;

          take b;

          now

            let x be object;

            

             A79: ( card ( Coim (fn,x))) = ( card ( Coim (a,x))) by A7;

            

            thus ( card ( Coim (b,x))) = (( card (((a | k) ^ <*q*>) " {x})) + ( card (ak " {x}))) by FINSEQ_3: 57

            .= ((( card ((a | k) " {x})) + ( card ( <*q*> " {x}))) + ( card (ak " {x}))) by FINSEQ_3: 57

            .= ((( card ((a | k) " {x})) + ( card (ak " {x}))) + ( card ( <*q*> " {x})))

            .= (( card (((a | k) ^ ak) " {x})) + ( card ( <*q*> " {x}))) by FINSEQ_3: 57

            .= (( card (fn " {x})) + ( card ( <*q*> " {x}))) by A79

            .= ( card ((fn ^ <*q*>) " {x})) by FINSEQ_3: 57

            .= ( card ( Coim (R,x))) by A5, A2, Th7;

          end;

          hence (R,b) are_fiberwise_equipotent ;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:22

    

     Th22: for R be FinSequence of REAL holds ex R1 be non-increasing FinSequence of REAL st (R,R1) are_fiberwise_equipotent

    proof

      let R be FinSequence of REAL ;

      

       A1: ( len R) = ( len R);

      for n holds P[n] from NAT_1:sch 2( Lm5, Lm6);

      hence thesis by A1;

    end;

    

     Lm7: for n holds for g1,g2 be non-increasing FinSequence of REAL st n = ( len g1) & (g1,g2) are_fiberwise_equipotent holds g1 = g2

    proof

      defpred P[ Nat] means for g1,g2 be non-increasing FinSequence of REAL st $1 = ( len g1) & (g1,g2) are_fiberwise_equipotent holds g1 = g2;

      

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

      proof

        let n;

        assume

         A2: P[n];

        let g1,g2 be non-increasing FinSequence of REAL ;

        set r = (g1 . (n + 1));

        reconsider g1n = (g1 | n), g2n = (g2 | n) as non-increasing FinSequence of REAL by Th20;

        assume that

         A3: ( len g1) = (n + 1) and

         A4: (g1,g2) are_fiberwise_equipotent ;

        

         A5: ( len g2) = ( len g1) by A4, Th3;

        then

         A6: (g1 . ( len g1)) = (g2 . ( len g2)) by A3, A4, Lm4;

        

         A7: ((g1 | n) ^ <*r*>) = g1 by A3, Th7;

        ( len (g1 | n)) = n by A3, FINSEQ_1: 59, NAT_1: 11;

        then g1n = g2n by A2, A3, A4, A5, Lm4;

        hence thesis by A3, A5, A6, A7, Th7;

      end;

      

       A8: P[ 0 ]

      proof

        let g1,g2 be non-increasing FinSequence of REAL ;

        assume ( len g1) = 0 & (g1,g2) are_fiberwise_equipotent ;

        then ( len g2) = ( len g1) & g1 = ( <*> REAL ) by Th3;

        hence thesis;

      end;

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

    end;

    theorem :: RFINSEQ:23

    for R1,R2 be non-increasing FinSequence of REAL st (R1,R2) are_fiberwise_equipotent holds R1 = R2

    proof

      let g1,g2 be non-increasing FinSequence of REAL ;

      

       A1: ( len g1) = ( len g1);

      assume (g1,g2) are_fiberwise_equipotent ;

      hence thesis by A1, Lm7;

    end;

    theorem :: RFINSEQ:24

    for R be FinSequence of REAL , r, s st r <> 0 holds (R " {(s / r)}) = ((r * R) " {s})

    proof

      let R be FinSequence of REAL , r, s;

      

       A1: ( Seg ( len R)) = ( dom R) & ( dom (r * R)) = ( Seg ( len (r * R))) by FINSEQ_1:def 3;

      assume

       A2: r <> 0 ;

      thus (R " {(s / r)}) c= ((r * R) " {s})

      proof

        let x be object;

        assume

         A3: x in (R " {(s / r)});

        then

        reconsider i = x as Element of NAT ;

        (R . i) in {(s / r)} by A3, FUNCT_1:def 7;

        then (R . i) = (s / r) by TARSKI:def 1;

        then (r * (R . i)) = s by A2, XCMPLX_1: 87;

        then ((r * R) . i) = s by RVSUM_1: 44;

        then

         A4: ((r * R) . i) in {s} by TARSKI:def 1;

        i in ( dom R) by A3, FUNCT_1:def 7;

        then i in ( dom (r * R)) by A1, FINSEQ_2: 33;

        hence thesis by A4, FUNCT_1:def 7;

      end;

      let x be object;

      assume

       A5: x in ((r * R) " {s});

      then

      reconsider i = x as Element of NAT ;

      ((r * R) . i) in {s} by A5, FUNCT_1:def 7;

      then ((r * R) . i) = s by TARSKI:def 1;

      then (r * (R . i)) = s by RVSUM_1: 44;

      then (R . i) = (s / r) by A2, XCMPLX_1: 89;

      then

       A6: (R . i) in {(s / r)} by TARSKI:def 1;

      i in ( dom (r * R)) by A5, FUNCT_1:def 7;

      then i in ( dom R) by A1, FINSEQ_2: 33;

      hence thesis by A6, FUNCT_1:def 7;

    end;

    theorem :: RFINSEQ:25

    for R be FinSequence of REAL holds (( 0 * R) " { 0 }) = ( dom R)

    proof

      let R be FinSequence of REAL ;

      

       A1: ( Seg ( len ( 0 * R))) = ( dom ( 0 * R)) by FINSEQ_1:def 3;

      

       A2: ( len ( 0 * R)) = ( len R) & ( dom R) = ( Seg ( len R)) by FINSEQ_1:def 3, FINSEQ_2: 33;

      hence (( 0 * R) " { 0 }) c= ( dom R) by A1, RELAT_1: 132;

      let x be object;

      assume

       A3: x in ( dom R);

      then

      reconsider i = x as Element of NAT ;

      (( 0 * R) . i) = ( 0 * (R . i)) by RVSUM_1: 44

      .= 0 ;

      then (( 0 * R) . i) in { 0 } by TARSKI:def 1;

      hence thesis by A2, A1, A3, FUNCT_1:def 7;

    end;

    begin

    reserve f,g for Function;

    theorem :: RFINSEQ:26

    for f, g st ( rng f) = ( rng g) & f is one-to-one & g is one-to-one holds (f,g) are_fiberwise_equipotent

    proof

      let f,g be Function such that

       A1: ( rng f) = ( rng g) and

       A2: f is one-to-one and

       A3: g is one-to-one;

      let x be object;

      per cases ;

        suppose

         A4: x in ( rng f);

        then ( card ( Coim (f,x))) = 1 by A2, FINSEQ_4: 73;

        hence thesis by A1, A3, A4, FINSEQ_4: 73;

      end;

        suppose

         A5: not x in ( rng f);

        then ( card (f " {x})) = 0 by CARD_1: 27, FUNCT_1: 72;

        hence thesis by A1, A5, CARD_1: 27, FUNCT_1: 72;

      end;

    end;

    theorem :: RFINSEQ:27

    for f be FinSequence holds (f /^ ( len f)) = {}

    proof

      let f be FinSequence;

      ( len (f /^ ( len f))) = (( len f) - ( len f)) by Def1

      .= 0 ;

      hence thesis;

    end;

    theorem :: RFINSEQ:28

    for f,g be Function, m,n be set st (f . m) = (g . n) & (f . n) = (g . m) & m in ( dom f) & n in ( dom f) & ( dom f) = ( dom g) & (for k be set st k <> m & k <> n & k in ( dom f) holds (f . k) = (g . k)) holds (f,g) are_fiberwise_equipotent

    proof

      let f,g be Function, m,n be set;

      assume that

       A1: (f . m) = (g . n) and

       A2: (f . n) = (g . m) and

       A3: m in ( dom f) and

       A4: n in ( dom f) and

       A5: ( dom f) = ( dom g) and

       A6: for k be set st k <> m & k <> n & k in ( dom f) holds (f . k) = (g . k);

      set t = ( id ( dom f)), nm = (n .--> m), mn = (m .--> n), p = ((t +* nm) +* mn);

      

       A7: ( dom nm) = {n};

      

       A8: ( dom t) = ( dom f);

      

       A9: ( rng t) = ( dom (t " )) by FUNCT_1: 33

      .= ( dom f) by A8, FUNCT_1: 45;

      ( dom mn) = {m};

      

      then

       A10: ( dom p) = (( dom (t +* nm)) \/ {m}) by FUNCT_4:def 1

      .= ((( dom t) \/ {n}) \/ {m}) by A7, FUNCT_4:def 1

      .= ((( dom f) \/ {n}) \/ {m})

      .= (( dom f) \/ {m}) by A4, ZFMISC_1: 40

      .= ( dom f) by A3, ZFMISC_1: 40;

       A11:

      now

        let x be object;

        assume

         A12: x in ( dom f);

        then

         A13: ((p * p) . x) = (p . (p . x)) by A10, FUNCT_1: 13;

        per cases ;

          suppose

           A14: x = m;

          

          hence ((p * p) . x) = (p . n) by A13, FUNCT_4: 89

          .= x by A14, FUNCT_4: 90;

        end;

          suppose

           A15: x <> m;

          now

            per cases ;

              suppose

               A16: x = n;

              

              hence ((p * p) . x) = (p . m) by A13, FUNCT_4: 90

              .= x by A16, FUNCT_4: 89;

            end;

              suppose

               A17: x <> n;

              

              hence ((p * p) . x) = (p . (t . x)) by A13, A15, FUNCT_4: 91

              .= (p . x) by A12, FUNCT_1: 17

              .= (t . x) by A15, A17, FUNCT_4: 91

              .= x by A12, FUNCT_1: 17;

            end;

          end;

          hence ((p * p) . x) = x;

        end;

      end;

      ( rng nm) = {m} by FUNCOP_1: 8;

      then (( rng t) \/ ( rng nm)) = ( dom f) by A3, ZFMISC_1: 40;

      then

       A18: (( rng (t +* nm)) \/ ( rng mn)) c= (( dom f) \/ ( rng mn)) by FUNCT_4: 17, XBOOLE_1: 9;

      for z be object st z in ( rng (p * p)) holds z in ( rng p) by FUNCT_1: 14;

      then

       A19: ( rng (p * p)) c= ( rng p);

      

       A20: ( rng p) c= (( rng (t +* nm)) \/ ( rng mn)) by FUNCT_4: 17;

      

       A21: ( rng mn) = {n} by FUNCOP_1: 8;

      then (( dom f) \/ ( rng mn)) = ( dom p) by A4, A10, ZFMISC_1: 40;

      then

       A22: ( dom (p * p)) = ( dom f) by A10, A18, A20, RELAT_1: 27, XBOOLE_1: 1;

      then (p * p) = t by A11, FUNCT_1: 17;

      then

       A23: p is one-to-one by A10, FUNCT_1: 31;

      ( rng p) c= (( dom f) \/ ( rng mn)) by A18, A20;

      then

       A24: ( rng p) c= ( dom p) by A4, A10, A21, ZFMISC_1: 40;

      then

       A25: ( dom (g * p)) = ( dom f) by A5, A10, RELAT_1: 27;

      now

        let x be object;

        assume

         A26: x in ( dom f);

        then

         A27: ((g * p) . x) = (g . (p . x)) by A25, FUNCT_1: 12;

        per cases ;

          suppose x = m;

          hence ((g * p) . x) = (f . x) by A1, A27, FUNCT_4: 89;

        end;

          suppose

           A28: x <> m;

          now

            per cases ;

              suppose x = n;

              hence ((g * p) . x) = (f . x) by A2, A27, FUNCT_4: 90;

            end;

              suppose

               A29: x <> n;

              

              hence ((g * p) . x) = (g . (t . x)) by A27, A28, FUNCT_4: 91

              .= (g . x) by A26, FUNCT_1: 17

              .= (f . x) by A6, A26, A28, A29;

            end;

          end;

          hence ((g * p) . x) = (f . x);

        end;

      end;

      then

       A30: f = (g * p) by A25, FUNCT_1: 2;

      ( rng (p * p)) = ( dom f) by A9, A22, A11, FUNCT_1: 17;

      then ( rng p) = ( dom g) by A5, A10, A24, A19;

      hence thesis by A10, A23, A30, CLASSES1: 77;

    end;

    theorem :: RFINSEQ:29

    for f be FinSequence, k be Nat holds ( len (f /^ k)) = (( len f) -' k)

    proof

      let f be FinSequence, k be Nat;

      per cases ;

        suppose

         A1: k <= ( len f);

        then (( len f) -' k) = (( len f) - k) by XREAL_1: 233;

        hence thesis by A1, Def1;

      end;

        suppose

         A2: k > ( len f);

        then (f /^ k) = {} by Def1;

        then

         A3: ( len (f /^ k)) = 0 ;

        (( len f) - k) < 0 by A2, XREAL_1: 49;

        hence thesis by A3, XREAL_0:def 2;

      end;

    end;

    theorem :: RFINSEQ:30

    

     Th30: for f,g be FinSequence, x be set st x in ( dom g) & (f,g) are_fiberwise_equipotent holds ex y be set st y in ( dom g) & (f . x) = (g . y)

    proof

      let f,g be FinSequence, x be set;

      assume that

       A1: x in ( dom g) and

       A2: (f,g) are_fiberwise_equipotent ;

      consider P be Permutation of ( dom g) such that

       A3: f = (g * P) by A2, Th4;

      take y = (P . x);

      thus y in ( dom g) by A1, FUNCT_2: 5;

      thus thesis by A1, A3, FUNCT_2: 15;

    end;

    theorem :: RFINSEQ:31

    

     Th31: for f,g,h be FinSequence holds (f,g) are_fiberwise_equipotent iff ((h ^ f),(h ^ g)) are_fiberwise_equipotent

    proof

      let f,g,h be FinSequence;

      thus (f,g) are_fiberwise_equipotent implies ((h ^ f),(h ^ g)) are_fiberwise_equipotent

      proof

        assume

         A1: (f,g) are_fiberwise_equipotent ;

        now

          let y be object;

          ( card ( Coim (f,y))) = ( card ( Coim (g,y))) by A1;

          

          hence ( card ( Coim ((h ^ f),y))) = (( card (g " {y})) + ( card (h " {y}))) by FINSEQ_3: 57

          .= ( card ( Coim ((h ^ g),y))) by FINSEQ_3: 57;

        end;

        hence thesis;

      end;

      assume

       A2: ((h ^ f),(h ^ g)) are_fiberwise_equipotent ;

      now

        let x be object;

        

         A3: ( card ( Coim ((h ^ f),x))) = (( card ( Coim (f,x))) + ( card (h " {x}))) & ( card ((h ^ g) " {x})) = (( card (g " {x})) + ( card (h " {x}))) by FINSEQ_3: 57;

        ( card ( Coim ((h ^ f),x))) = ( card ( Coim ((h ^ g),x))) by A2;

        hence ( card ( Coim (f,x))) = ( card ( Coim (g,x))) by A3;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ:32

    for f,g be FinSequence, m,n,j be Nat st (f,g) are_fiberwise_equipotent & m <= n & n <= ( len f) & (for i be Nat st 1 <= i & i <= m holds (f . i) = (g . i)) & (for i be Nat st n < i & i <= ( len f) holds (f . i) = (g . i)) & m < j & j <= n holds ex k be Nat st m < k & k <= n & (f . j) = (g . k)

    proof

      let f,g be FinSequence, m,n,j be Nat;

      assume

       A1: (f,g) are_fiberwise_equipotent ;

      assume that

       A2: m <= n and

       A3: n <= ( len f);

      assume

       A4: for i be Nat st 1 <= i & i <= m holds (f . i) = (g . i);

      reconsider m3 = (( len f) - n) as Element of NAT by A3, INT_1: 3, XREAL_1: 48;

      ( len g) = (n + m3) by A1, Th3;

      then

      consider s2,r2 be FinSequence such that

       A5: ( len s2) = n and

       A6: ( len r2) = m3 and

       A7: g = (s2 ^ r2) by FINSEQ_2: 22;

      

       A8: ( len f) = (n + m3);

      then

      consider s1,r1 be FinSequence such that

       A9: ( len s1) = n and

       A10: ( len r1) = m3 and

       A11: f = (s1 ^ r1) by FINSEQ_2: 22;

      

       A12: ( dom r1) = ( Seg m3) by A10, FINSEQ_1:def 3;

      assume

       A13: for i be Nat st n < i & i <= ( len f) holds (f . i) = (g . i);

      now

        let i be Nat;

        reconsider a = i as Nat;

        

         A14: n < (n + 1) by XREAL_1: 29;

        assume

         A15: i in ( dom r1);

        then

         A16: i in ( dom r2) by A6, A12, FINSEQ_1:def 3;

        1 <= i by A12, A15, FINSEQ_1: 1;

        then (n + 1) <= (n + i) by XREAL_1: 6;

        then

         A17: n < (i + n) by A14, XXREAL_0: 2;

        i <= m3 by A12, A15, FINSEQ_1: 1;

        then

         A18: (( len s1) + i) <= ( len f) by A8, A9, XREAL_1: 6;

        

        thus (r1 . i) = (f . (( len s1) + i)) by A11, A15, FINSEQ_1:def 7

        .= (g . (( len s2) + a)) by A13, A9, A5, A17, A18

        .= (r2 . i) by A7, A16, FINSEQ_1:def 7;

      end;

      then r1 = r2 by A10, A6, FINSEQ_2: 9;

      then

       A19: (s1,s2) are_fiberwise_equipotent by A1, A11, A7, Th1;

      reconsider m2 = (n - m) as Element of NAT by A2, INT_1: 3, XREAL_1: 48;

      

       A20: (m + 1) > m by XREAL_1: 29;

      ( len s2) = (m + m2) by A5;

      then

      consider p2,q2 be FinSequence such that

       A21: ( len p2) = m and

       A22: ( len q2) = m2 and

       A23: s2 = (p2 ^ q2) by FINSEQ_2: 22;

      

       A24: ( Seg m) = ( dom p2) by A21, FINSEQ_1:def 3;

      ( len s1) = (m + m2) by A9;

      then

      consider p1,q1 be FinSequence such that

       A25: ( len p1) = m and

       A26: ( len q1) = m2 and

       A27: s1 = (p1 ^ q1) by FINSEQ_2: 22;

      

       A28: f = (p1 ^ (q1 ^ r1)) by A11, A27, FINSEQ_1: 32;

      

       A29: ( dom p1) = ( Seg m) by A25, FINSEQ_1:def 3;

      

       A30: g = (p2 ^ (q2 ^ r2)) by A7, A23, FINSEQ_1: 32;

      now

        let i be Nat;

        reconsider a = i as Nat;

        assume

         A31: i in ( dom p1);

        then

         A32: 1 <= i & i <= m by A29, FINSEQ_1: 1;

        

        thus (p1 . i) = (f . i) by A28, A31, FINSEQ_1:def 7

        .= (g . a) by A4, A32

        .= (p2 . i) by A30, A24, A29, A31, FINSEQ_1:def 7;

      end;

      then p1 = p2 by A25, A21, FINSEQ_2: 9;

      then

       A33: (q1,q2) are_fiberwise_equipotent by A27, A23, A19, Th31;

      assume that

       A34: m < j and

       A35: j <= n;

      (j - ( len p1)) > 0 by A34, A25, XREAL_1: 50;

      then

      reconsider x = (j - ( len p1)) as Element of NAT by INT_1: 3;

      

       A36: x <= (n - ( len p1)) by A35, XREAL_1: 9;

      

       A37: ( Seg m2) = ( dom q2) by A22, FINSEQ_1:def 3;

      

       A38: (1 + 0 ) <= x by A34, A25, INT_1: 7, XREAL_1: 50;

      then x in ( dom q2) by A25, A37, A36;

      then

      consider y be set such that

       A39: y in ( dom q2) and

       A40: (q1 . x) = (q2 . y) by A33, Th30;

      reconsider y as Nat by A39;

      

       A41: (( len p2) + y) in ( dom s2) by A23, A39, FINSEQ_1: 28;

      reconsider k = (( len p2) + y) as Nat;

      take k;

      1 <= y by A37, A39, FINSEQ_1: 1;

      then k >= (( len p2) + 1) by XREAL_1: 6;

      hence m < k by A21, A20, XXREAL_0: 2;

      y <= m2 by A37, A39, FINSEQ_1: 1;

      then k <= (m2 + ( len p2)) by XREAL_1: 6;

      hence k <= n by A21;

      ( Seg m2) = ( dom q1) by A26, FINSEQ_1:def 3;

      then

       A42: x in ( dom q1) by A25, A38, A36;

      then (( len p1) + x) in ( dom s1) by A27, FINSEQ_1: 28;

      

      hence (f . j) = (s1 . (( len p1) + x)) by A11, FINSEQ_1:def 7

      .= (q2 . y) by A27, A40, A42, FINSEQ_1:def 7

      .= (s2 . (( len p2) + y)) by A23, A39, FINSEQ_1:def 7

      .= (g . k) by A7, A41, FINSEQ_1:def 7;

    end;

    theorem :: RFINSEQ:33

    for t be FinSequence of INT holds ex u be FinSequence of REAL st (t,u) are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing

    proof

      let t be FinSequence of INT ;

      t is FinSequence of REAL by FINSEQ_3: 117;

      then

      consider u be non-increasing FinSequence of REAL such that

       A1: (t,u) are_fiberwise_equipotent by Th22;

      take u;

      thus (t,u) are_fiberwise_equipotent by A1;

      ( rng t) = ( rng u) by A1, CLASSES1: 75;

      hence u is FinSequence of INT by FINSEQ_1:def 4;

      thus thesis;

    end;