rfinseq2.miz



    begin

    reserve n,m for Nat;

    definition

      let f be FinSequence of REAL ;

      :: RFINSEQ2:def1

      func max_p f -> Nat means

      : Def1: (( len f) = 0 implies it = 0 ) & (( len f) > 0 implies it in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . it ) holds r1 <= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . it ) holds it <= j);

      existence

      proof

        

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

        per cases ;

          suppose ( len f) = 0 ;

          hence thesis;

        end;

          suppose

           A2: ( len f) <> 0 ;

          defpred P[ Nat] means (ex n be Nat st ($1 <> 0 implies n <= $1 & n in ( dom f)) & (for i be Nat, r1,r2 be Real st i <= $1 & i in ( dom f) & r1 = (f . i) & r2 = (f . n) holds r1 <= r2) & (for j be Nat st j <= $1 & j in ( dom f) & (f . j) = (f . n) holds n <= j));

          

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

          proof

            let k be Nat;

            assume P[k];

            then

            consider n1 be Nat such that

             A4: k <> 0 implies n1 <= k & n1 in ( dom f) and

             A5: for i be Nat, r1,r2 be Real st i <= k & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 <= r2 and

             A6: for j be Nat st j <= k & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j;

            per cases ;

              suppose

               A7: k = 0 ;

              

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

              

               A9: for i be Nat, r1,r2 be Real st i <= 1 & i in ( dom f) & r1 = (f . i) & r2 = (f . 1) holds r1 <= r2

              proof

                let i be Nat, r1,r2 be Real;

                assume that

                 A10: i <= 1 and

                 A11: i in ( dom f) and

                 A12: r1 = (f . i) & r2 = (f . 1);

                1 <= i by A11, FINSEQ_3: 25;

                hence thesis by A10, A12, XXREAL_0: 1;

              end;

              ( len f) >= ( 0 + 1) by A2, NAT_1: 13;

              then

               A13: 1 in ( dom f) by A8, FINSEQ_1: 1;

              for j be Nat st j <= 1 & j in ( dom f) & (f . j) = (f . 1) holds 1 <= j by A8, FINSEQ_1: 1;

              hence thesis by A7, A13, A9;

            end;

              suppose

               A14: k <> 0 ;

              now

                per cases ;

                  case

                   A15: (f . n1) >= (f . (k + 1));

                  

                   A16: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 <= r2

                  proof

                    let i be Nat, r1,r2 be Real;

                    assume that

                     A17: i <= (k + 1) and

                     A18: i in ( dom f) and

                     A19: r1 = (f . i) & r2 = (f . n1);

                    per cases ;

                      suppose i < (k + 1);

                      then i <= k by NAT_1: 13;

                      hence thesis by A5, A18, A19;

                    end;

                      suppose i >= (k + 1);

                      hence thesis by A15, A17, A19, XXREAL_0: 1;

                    end;

                  end;

                  

                   A20: n1 <= (k + 1) by A4, A14, NAT_1: 13;

                  

                   A21: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

                  proof

                    let j be Nat;

                    assume that

                     A22: j <= (k + 1) and

                     A23: j in ( dom f) & (f . j) = (f . n1);

                    now

                      per cases ;

                        case j < (k + 1);

                        then j <= k by NAT_1: 13;

                        hence thesis by A6, A23;

                      end;

                        case j >= (k + 1);

                        hence thesis by A20, A22, XXREAL_0: 1;

                      end;

                    end;

                    hence thesis;

                  end;

                  (k + 1) <> 0 implies n1 <= (k + 1) & n1 in ( dom f) by A4, A14, NAT_1: 13;

                  hence thesis by A16, A21;

                end;

                  case

                   A24: (f . n1) < (f . (k + 1));

                  now

                    per cases ;

                      case

                       A25: (k + 1) > ( len f);

                      

                       A26: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

                      proof

                        let j be Nat;

                        assume that j <= (k + 1) and

                         A27: j in ( dom f) & (f . j) = (f . n1);

                        per cases ;

                          suppose j < (k + 1);

                          then j <= k by NAT_1: 13;

                          hence thesis by A6, A27;

                        end;

                          suppose j >= (k + 1);

                          then k < j by NAT_1: 13;

                          hence thesis by A4, A14, XXREAL_0: 2;

                        end;

                      end;

                      

                       A28: k >= ( len f) by A25, NAT_1: 13;

                      

                       A29: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 <= r2

                      proof

                        let i be Nat, r1,r2 be Real;

                        assume that i <= (k + 1) and

                         A30: i in ( dom f) and

                         A31: r1 = (f . i) & r2 = (f . n1);

                        i <= ( len f) by A1, A30, FINSEQ_1: 1;

                        then i <= k by A28, XXREAL_0: 2;

                        hence thesis by A5, A30, A31;

                      end;

                      n1 <= ( len f) by A1, A4, A14, FINSEQ_1: 1;

                      then (k + 1) <> 0 implies n1 <= (k + 1) & n1 in ( dom f) by A4, A14, A25, XXREAL_0: 2;

                      hence thesis by A29, A26;

                    end;

                      case

                       A32: (k + 1) <= ( len f);

                      set n2 = (k + 1);

                      

                       A33: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n2) holds r1 <= r2

                      proof

                        let i be Nat, r1,r2 be Real;

                        assume that

                         A34: i <= (k + 1) and

                         A35: i in ( dom f) and

                         A36: r1 = (f . i) and

                         A37: r2 = (f . n2);

                        per cases ;

                          suppose

                           A38: i < (k + 1);

                          reconsider r3 = (f . n1) as Real;

                          i <= k by A38, NAT_1: 13;

                          then r1 <= r3 by A5, A35, A36;

                          hence thesis by A24, A37, XXREAL_0: 2;

                        end;

                          suppose i >= (k + 1);

                          hence thesis by A34, A36, A37, XXREAL_0: 1;

                        end;

                      end;

                      

                       A39: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n2) holds n2 <= j

                      proof

                        let j be Nat;

                        assume that j <= (k + 1) and

                         A40: j in ( dom f) & (f . j) = (f . n2);

                        per cases ;

                          suppose j < (k + 1);

                          then j <= k by NAT_1: 13;

                          hence thesis by A5, A24, A40;

                        end;

                          suppose j >= (k + 1);

                          hence thesis;

                        end;

                      end;

                      1 <= (1 + k) by NAT_1: 12;

                      then (k + 1) <> 0 implies n2 <= (k + 1) & n2 in ( dom f) by A1, A32, FINSEQ_1: 1;

                      hence thesis by A33, A39;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          (for i be Nat, r1,r2 be Real st i <= 0 & i in ( dom f) & r1 = (f . i) & r2 = (f . 1) holds r1 <= r2) & for j be Nat st j <= 0 & j in ( dom f) & (f . j) = (f . 1) holds 1 <= j by A1, FINSEQ_1: 1;

          then

           A41: P[ 0 ];

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

          then

          consider n1 be Nat such that

           A42: ( len f) <> 0 implies n1 <= ( len f) & n1 in ( dom f) and

           A43: for i be Nat, r1,r2 be Real st i <= ( len f) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 <= r2 and

           A44: for j be Nat st j <= ( len f) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j;

          

           A45: for j be Nat st j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

          proof

            let j be Nat;

            assume that

             A46: j in ( dom f) and

             A47: (f . j) = (f . n1);

            j <= ( len f) by A46, FINSEQ_3: 25;

            hence thesis by A44, A46, A47;

          end;

          for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 <= r2

          proof

            let i be Nat, r1,r2 be Real;

            assume that

             A48: i in ( dom f) and

             A49: r1 = (f . i) & r2 = (f . n1);

            i <= ( len f) by A48, FINSEQ_3: 25;

            hence thesis by A43, A48, A49;

          end;

          hence thesis by A2, A42, A45;

        end;

      end;

      uniqueness

      proof

        thus for m1,m2 be Nat st (( len f) = 0 implies m1 = 0 ) & (( len f) > 0 implies m1 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m1) holds r1 <= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m1) holds m1 <= j) & (( len f) = 0 implies m2 = 0 ) & (( len f) > 0 implies m2 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m2) holds r1 <= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m2) holds m2 <= j) holds m1 = m2

        proof

          let m1,m2 be Nat;

          assume

           A50: (( len f) = 0 implies m1 = 0 ) & (( len f) > 0 implies m1 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m1) holds r1 <= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m1) holds m1 <= j) & (( len f) = 0 implies m2 = 0 ) & (( len f) > 0 implies m2 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m2) holds r1 <= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m2) holds m2 <= j);

          then (f . m2) <= (f . m1) & (f . m1) <= (f . m2);

          then (f . m1) = (f . m2) by XXREAL_0: 1;

          then m1 <= m2 & m2 <= m1 by A50;

          hence thesis by XXREAL_0: 1;

        end;

      end;

    end

    definition

      let f be FinSequence of REAL ;

      :: RFINSEQ2:def2

      func min_p f -> Nat means

      : Def2: (( len f) = 0 implies it = 0 ) & (( len f) > 0 implies it in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . it ) holds r1 >= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . it ) holds it <= j);

      existence

      proof

        

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

        now

          per cases ;

            case ( len f) = 0 ;

            hence thesis;

          end;

            case

             A2: ( len f) <> 0 ;

            defpred P[ Nat] means (ex n be Nat st ($1 <> 0 implies n <= $1 & n in ( dom f)) & (for i be Nat, r1,r2 be Real st i <= $1 & i in ( dom f) & r1 = (f . i) & r2 = (f . n) holds r1 >= r2) & (for j be Nat st j <= $1 & j in ( dom f) & (f . j) = (f . n) holds n <= j));

            

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

            proof

              let k be Nat;

              assume P[k];

              then

              consider n1 be Nat such that

               A4: k <> 0 implies n1 <= k & n1 in ( dom f) and

               A5: for i be Nat, r1,r2 be Real st i <= k & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 >= r2 and

               A6: for j be Nat st j <= k & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j;

              now

                per cases ;

                  case

                   A7: k = 0 ;

                  

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

                  

                   A9: for i be Nat, r1,r2 be Real st i <= 1 & i in ( dom f) & r1 = (f . i) & r2 = (f . 1) holds r1 >= r2

                  proof

                    let i be Nat, r1,r2 be Real;

                    assume that

                     A10: i <= 1 and

                     A11: i in ( dom f) and

                     A12: r1 = (f . i) & r2 = (f . 1);

                    1 <= i by A11, FINSEQ_3: 25;

                    hence thesis by A10, A12, XXREAL_0: 1;

                  end;

                  ( len f) >= ( 0 + 1) by A2, NAT_1: 13;

                  then

                   A13: 1 in ( dom f) by A8, FINSEQ_1: 1;

                  for j be Nat st j <= 1 & j in ( dom f) & (f . j) = (f . 1) holds 1 <= j by A8, FINSEQ_1: 1;

                  hence thesis by A7, A13, A9;

                end;

                  case

                   A14: k <> 0 ;

                  now

                    per cases ;

                      case

                       A15: (f . n1) <= (f . (k + 1));

                      

                       A16: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 >= r2

                      proof

                        let i be Nat, r1,r2 be Real;

                        assume that

                         A17: i <= (k + 1) and

                         A18: i in ( dom f) and

                         A19: r1 = (f . i) & r2 = (f . n1);

                        per cases ;

                          suppose i < (k + 1);

                          then i <= k by NAT_1: 13;

                          hence thesis by A5, A18, A19;

                        end;

                          suppose i >= (k + 1);

                          hence thesis by A15, A17, A19, XXREAL_0: 1;

                        end;

                      end;

                      

                       A20: n1 <= (k + 1) by A4, A14, NAT_1: 13;

                      

                       A21: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

                      proof

                        let j be Nat;

                        assume that

                         A22: j <= (k + 1) and

                         A23: j in ( dom f) & (f . j) = (f . n1);

                        per cases ;

                          suppose j < (k + 1);

                          then j <= k by NAT_1: 13;

                          hence thesis by A6, A23;

                        end;

                          suppose j >= (k + 1);

                          hence thesis by A20, A22, XXREAL_0: 1;

                        end;

                      end;

                      (k + 1) <> 0 implies n1 <= (k + 1) & n1 in ( dom f) by A4, A14, NAT_1: 13;

                      hence thesis by A16, A21;

                    end;

                      case

                       A24: (f . n1) > (f . (k + 1));

                      now

                        per cases ;

                          case

                           A25: (k + 1) > ( len f);

                          

                           A26: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

                          proof

                            let j be Nat;

                            assume that j <= (k + 1) and

                             A27: j in ( dom f) & (f . j) = (f . n1);

                            per cases ;

                              suppose j < (k + 1);

                              then j <= k by NAT_1: 13;

                              hence thesis by A6, A27;

                            end;

                              suppose j >= (k + 1);

                              then k < j by NAT_1: 13;

                              hence thesis by A4, A14, XXREAL_0: 2;

                            end;

                          end;

                          

                           A28: k >= ( len f) by A25, NAT_1: 13;

                          

                           A29: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 >= r2

                          proof

                            let i be Nat, r1,r2 be Real;

                            assume that i <= (k + 1) and

                             A30: i in ( dom f) and

                             A31: r1 = (f . i) & r2 = (f . n1);

                            i <= ( len f) by A1, A30, FINSEQ_1: 1;

                            then i <= k by A28, XXREAL_0: 2;

                            hence thesis by A5, A30, A31;

                          end;

                          n1 <= ( len f) by A1, A4, A14, FINSEQ_1: 1;

                          then (k + 1) <> 0 implies n1 <= (k + 1) & n1 in ( dom f) by A4, A14, A25, XXREAL_0: 2;

                          hence thesis by A29, A26;

                        end;

                          case

                           A32: (k + 1) <= ( len f);

                          set n2 = (k + 1);

                          

                           A33: for i be Nat, r1,r2 be Real st i <= (k + 1) & i in ( dom f) & r1 = (f . i) & r2 = (f . n2) holds r1 >= r2

                          proof

                            let i be Nat, r1,r2 be Real;

                            assume that

                             A34: i <= (k + 1) and

                             A35: i in ( dom f) and

                             A36: r1 = (f . i) and

                             A37: r2 = (f . n2);

                            per cases ;

                              suppose

                               A38: i < (k + 1);

                              reconsider r3 = (f . n1) as Real;

                              i <= k by A38, NAT_1: 13;

                              then r1 >= r3 by A5, A35, A36;

                              hence thesis by A24, A37, XXREAL_0: 2;

                            end;

                              suppose i >= (k + 1);

                              hence thesis by A34, A36, A37, XXREAL_0: 1;

                            end;

                          end;

                          

                           A39: for j be Nat st j <= (k + 1) & j in ( dom f) & (f . j) = (f . n2) holds n2 <= j

                          proof

                            let j be Nat;

                            assume that j <= (k + 1) and

                             A40: j in ( dom f) & (f . j) = (f . n2);

                            per cases ;

                              suppose j < (k + 1);

                              then j <= k by NAT_1: 13;

                              hence thesis by A5, A24, A40;

                            end;

                              suppose j >= (k + 1);

                              hence thesis;

                            end;

                          end;

                          1 <= (1 + k) by NAT_1: 12;

                          then (k + 1) <> 0 implies n2 <= (k + 1) & n2 in ( dom f) by A1, A32, FINSEQ_1: 1;

                          hence thesis by A33, A39;

                        end;

                      end;

                      hence thesis;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

            (for i be Nat, r1,r2 be Real st i <= 0 & i in ( dom f) & r1 = (f . i) & r2 = (f . 1) holds r1 >= r2) & for j be Nat st j <= 0 & j in ( dom f) & (f . j) = (f . 1) holds 1 <= j by A1, FINSEQ_1: 1;

            then

             A41: P[ 0 ];

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

            then

            consider n1 be Nat such that

             A42: ( len f) <> 0 implies n1 <= ( len f) & n1 in ( dom f) and

             A43: for i be Nat, r1,r2 be Real st i <= ( len f) & i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 >= r2 and

             A44: for j be Nat st j <= ( len f) & j in ( dom f) & (f . j) = (f . n1) holds n1 <= j;

            

             A45: for j be Nat st j in ( dom f) & (f . j) = (f . n1) holds n1 <= j

            proof

              let j be Nat;

              assume that

               A46: j in ( dom f) and

               A47: (f . j) = (f . n1);

              j <= ( len f) by A46, FINSEQ_3: 25;

              hence thesis by A44, A46, A47;

            end;

            for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . n1) holds r1 >= r2

            proof

              let i be Nat, r1,r2 be Real;

              assume that

               A48: i in ( dom f) and

               A49: r1 = (f . i) & r2 = (f . n1);

              i <= ( len f) by A48, FINSEQ_3: 25;

              hence thesis by A43, A48, A49;

            end;

            hence thesis by A2, A42, A45;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        thus for m1,m2 be Nat st (( len f) = 0 implies m1 = 0 ) & (( len f) > 0 implies m1 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m1) holds r1 >= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m1) holds m1 <= j) & (( len f) = 0 implies m2 = 0 ) & (( len f) > 0 implies m2 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m2) holds r1 >= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m2) holds m2 <= j) holds m1 = m2

        proof

          let m1,m2 be Nat;

          assume

           A50: (( len f) = 0 implies m1 = 0 ) & (( len f) > 0 implies m1 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m1) holds r1 >= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m1) holds m1 <= j) & (( len f) = 0 implies m2 = 0 ) & (( len f) > 0 implies m2 in ( dom f) & (for i be Nat, r1,r2 be Real st i in ( dom f) & r1 = (f . i) & r2 = (f . m2) holds r1 >= r2) & for j be Nat st j in ( dom f) & (f . j) = (f . m2) holds m2 <= j);

          then (f . m2) >= (f . m1) & (f . m1) >= (f . m2);

          then (f . m1) = (f . m2) by XXREAL_0: 1;

          then m1 >= m2 & m2 >= m1 by A50;

          hence thesis by XXREAL_0: 1;

        end;

      end;

    end

    definition

      let f be FinSequence of REAL ;

      :: RFINSEQ2:def3

      func max f -> Real equals (f . ( max_p f));

      correctness ;

      :: RFINSEQ2:def4

      func min f -> Real equals (f . ( min_p f));

      correctness ;

    end

    theorem :: RFINSEQ2:1

    

     Th1: for f be FinSequence of REAL , i be Nat st 1 <= i & i <= ( len f) holds (f . i) <= (f . ( max_p f)) & (f . i) <= ( max f)

    proof

      let f be FinSequence of REAL , i be Nat;

      assume

       A1: 1 <= i & i <= ( len f);

      then

       A2: i in ( dom f) by FINSEQ_3: 25;

      hence (f . i) <= (f . ( max_p f)) by A1, Def1;

      thus thesis by A1, A2, Def1;

    end;

    theorem :: RFINSEQ2:2

    

     Th2: for f be FinSequence of REAL , i be Nat st 1 <= i & i <= ( len f) holds (f . i) >= (f . ( min_p f)) & (f . i) >= ( min f)

    proof

      let f be FinSequence of REAL , i be Nat;

      assume

       A1: 1 <= i & i <= ( len f);

      then

       A2: i in ( dom f) by FINSEQ_3: 25;

      hence (f . i) >= (f . ( min_p f)) by A1, Def2;

      thus thesis by A1, A2, Def2;

    end;

    theorem :: RFINSEQ2:3

    for f be FinSequence of REAL , r be Real st f = <*r*> holds ( max_p f) = 1 & ( max f) = r

    proof

      let f be FinSequence of REAL , r be Real;

      assume

       A1: f = <*r*>;

      then

       A2: (f . 1) = r by FINSEQ_1: 40;

      

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

      then ( max_p f) in ( dom f) by Def1;

      then 1 <= ( max_p f) & ( max_p f) <= ( len f) by FINSEQ_3: 25;

      hence thesis by A3, A2, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:4

    for f be FinSequence of REAL , r be Real st f = <*r*> holds ( min_p f) = 1 & ( min f) = r

    proof

      let f be FinSequence of REAL , r be Real;

      assume

       A1: f = <*r*>;

      then

       A2: (f . 1) = r by FINSEQ_1: 40;

      

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

      then ( min_p f) in ( dom f) by Def2;

      then 1 <= ( min_p f) & ( min_p f) <= ( len f) by FINSEQ_3: 25;

      hence thesis by A3, A2, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:5

    for f be FinSequence of REAL , r1,r2 be Real st f = <*r1, r2*> holds ( max f) = ( max (r1,r2)) & ( max_p f) = ( IFEQ (r1,( max (r1,r2)),1,2))

    proof

      let f be FinSequence of REAL , r1,r2 be Real;

      assume

       A1: f = <*r1, r2*>;

      then

       A2: ( len f) = 2 by FINSEQ_1: 44;

      then

       A3: (f . 2) <= (f . ( max_p f)) by Th1;

      

       A4: (f . 1) = r1 by A1, FINSEQ_1: 44;

      

       A5: ( max_p f) in ( dom f) by A2, Def1;

      then

       A6: 1 <= ( max_p f) by FINSEQ_3: 25;

      

       A7: ( max_p f) <= ( len f) by A5, FINSEQ_3: 25;

      

       A8: (f . 2) = r2 by A1, FINSEQ_1: 44;

      

       A9: (f . 1) <= (f . ( max_p f)) by A2, Th1;

      now

        per cases ;

          case r1 >= r2;

          then

           A10: ( max (r1,r2)) <= ( max f) by A4, A9, XXREAL_0:def 10;

          now

            per cases ;

              case ( max_p f) < ( len f);

              then ( max_p f) < (1 + 1) by A1, FINSEQ_1: 44;

              then ( max_p f) <= 1 by NAT_1: 13;

              then

               A11: ( max_p f) = 1 by A6, XXREAL_0: 1;

              then ( max f) <= ( max (r1,r2)) by A4, XXREAL_0: 25;

              then ( max f) = ( max (r1,r2)) by A10, XXREAL_0: 1;

              hence thesis by A4, A11, FUNCOP_1:def 8;

            end;

              case ( max_p f) >= ( len f);

              then

               A12: ( max_p f) = 2 by A2, A7, XXREAL_0: 1;

              then ( max f) <= ( max (r1,r2)) by A8, XXREAL_0: 25;

              then

               A13: ( max f) = ( max (r1,r2)) by A10, XXREAL_0: 1;

              1 in ( dom f) by A2, FINSEQ_3: 25;

              then r1 <> r2 by A2, A4, A8, A12, Def1;

              hence thesis by A8, A12, A13, FUNCOP_1:def 8;

            end;

          end;

          hence thesis;

        end;

          case r1 < r2;

          then

           A14: ( max (r1,r2)) <= ( max f) by A8, A3, XXREAL_0:def 10;

          now

            per cases ;

              case ( max_p f) < ( len f);

              then ( max_p f) < (1 + 1) by A1, FINSEQ_1: 44;

              then ( max_p f) <= 1 by NAT_1: 13;

              then

               A15: ( max_p f) = 1 by A6, XXREAL_0: 1;

              then ( max f) <= ( max (r1,r2)) by A4, XXREAL_0: 25;

              then ( max f) = ( max (r1,r2)) by A14, XXREAL_0: 1;

              hence thesis by A4, A15, FUNCOP_1:def 8;

            end;

              case ( max_p f) >= ( len f);

              then

               A16: ( max_p f) = 2 by A2, A7, XXREAL_0: 1;

              then ( max f) <= ( max (r1,r2)) by A8, XXREAL_0: 25;

              then

               A17: ( max f) = ( max (r1,r2)) by A14, XXREAL_0: 1;

              1 in ( dom f) by A2, FINSEQ_3: 25;

              then r1 <> r2 by A2, A4, A8, A16, Def1;

              hence thesis by A8, A16, A17, FUNCOP_1:def 8;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ2:6

    for f be FinSequence of REAL , r1,r2 be Real st f = <*r1, r2*> holds ( min f) = ( min (r1,r2)) & ( min_p f) = ( IFEQ (r1,( min (r1,r2)),1,2))

    proof

      let f be FinSequence of REAL , r1,r2 be Real;

      assume

       A1: f = <*r1, r2*>;

      then

       A2: ( len f) = 2 by FINSEQ_1: 44;

      then

       A3: (f . 1) >= (f . ( min_p f)) by Th2;

      

       A4: (f . 2) = r2 by A1, FINSEQ_1: 44;

      

       A5: ( min_p f) in ( dom f) by A2, Def2;

      then

       A6: 1 <= ( min_p f) by FINSEQ_3: 25;

      

       A7: (f . 2) >= (f . ( min_p f)) by A2, Th2;

      

       A8: (f . 1) = r1 by A1, FINSEQ_1: 44;

      

       A9: ( min_p f) <= ( len f) by A5, FINSEQ_3: 25;

      per cases ;

        suppose r1 <= r2;

        then

         A10: ( min (r1,r2)) >= ( min f) by A8, A3, XXREAL_0:def 9;

        now

          per cases ;

            case ( min_p f) < ( len f);

            then ( min_p f) < (1 + 1) by A1, FINSEQ_1: 44;

            then ( min_p f) <= 1 by NAT_1: 13;

            then

             A11: ( min_p f) = 1 by A6, XXREAL_0: 1;

            then ( min f) >= ( min (r1,r2)) by A8, XXREAL_0: 17;

            then ( min f) = ( min (r1,r2)) by A10, XXREAL_0: 1;

            hence thesis by A8, A11, FUNCOP_1:def 8;

          end;

            case ( min_p f) >= ( len f);

            then

             A12: ( min_p f) = 2 by A2, A9, XXREAL_0: 1;

            then ( min f) >= ( min (r1,r2)) by A4, XXREAL_0: 17;

            then

             A13: ( min f) = ( min (r1,r2)) by A10, XXREAL_0: 1;

            1 in ( dom f) by A2, FINSEQ_3: 25;

            then r1 <> r2 by A2, A8, A4, A12, Def2;

            hence thesis by A4, A12, A13, FUNCOP_1:def 8;

          end;

        end;

        hence thesis;

      end;

        suppose r1 > r2;

        then

         A14: ( min (r1,r2)) >= ( min f) by A4, A7, XXREAL_0:def 9;

        now

          per cases ;

            case ( min_p f) < ( len f);

            then ( min_p f) < (1 + 1) by A1, FINSEQ_1: 44;

            then ( min_p f) <= 1 by NAT_1: 13;

            then

             A15: ( min_p f) = 1 by A6, XXREAL_0: 1;

            then ( min f) >= ( min (r1,r2)) by A8, XXREAL_0: 17;

            then ( min f) = ( min (r1,r2)) by A14, XXREAL_0: 1;

            hence thesis by A8, A15, FUNCOP_1:def 8;

          end;

            case ( min_p f) >= ( len f);

            then

             A16: ( min_p f) = 2 by A2, A9, XXREAL_0: 1;

            then ( min f) >= ( min (r1,r2)) by A4, XXREAL_0: 17;

            then

             A17: ( min f) = ( min (r1,r2)) by A14, XXREAL_0: 1;

            1 in ( dom f) by A2, FINSEQ_3: 25;

            then r1 <> r2 by A2, A8, A4, A16, Def2;

            hence thesis by A4, A16, A17, FUNCOP_1:def 8;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: RFINSEQ2:7

    for f1,f2 be FinSequence of REAL st ( len f1) = ( len f2) & ( len f1) > 0 holds ( max (f1 + f2)) <= (( max f1) + ( max f2))

    proof

      let f1,f2 be FinSequence of REAL ;

      assume that

       A1: ( len f1) = ( len f2) and

       A2: ( len f1) > 0 ;

      

       A3: ( len (f1 + f2)) = ( len f1) by A1, RVSUM_1: 115;

      then

       A4: ( max_p (f1 + f2)) in ( dom (f1 + f2)) by A2, Def1;

      then 1 <= ( max_p (f1 + f2)) & ( max_p (f1 + f2)) <= ( len (f1 + f2)) by FINSEQ_3: 25;

      then

       A5: ( max_p (f1 + f2)) in ( Seg ( len f1)) by A3, FINSEQ_1: 1;

      then ( max_p (f1 + f2)) in ( dom f2) by A1, FINSEQ_1:def 3;

      then

       A6: (f2 . ( max_p (f1 + f2))) <= (f2 . ( max_p f2)) by A1, A2, Def1;

      ( max_p (f1 + f2)) in ( dom f1) by A5, FINSEQ_1:def 3;

      then

       A7: (f1 . ( max_p (f1 + f2))) <= (f1 . ( max_p f1)) by A2, Def1;

      ( max (f1 + f2)) = ((f1 . ( max_p (f1 + f2))) + (f2 . ( max_p (f1 + f2)))) by A4, VALUED_1:def 1;

      hence thesis by A7, A6, XREAL_1: 7;

    end;

    theorem :: RFINSEQ2:8

    for f1,f2 be FinSequence of REAL st ( len f1) = ( len f2) & ( len f1) > 0 holds ( min (f1 + f2)) >= (( min f1) + ( min f2))

    proof

      let f1,f2 be FinSequence of REAL ;

      assume that

       A1: ( len f1) = ( len f2) and

       A2: ( len f1) > 0 ;

      

       A3: ( len (f1 + f2)) = ( len f1) by A1, RVSUM_1: 115;

      then

       A4: ( min_p (f1 + f2)) in ( dom (f1 + f2)) by A2, Def2;

      then 1 <= ( min_p (f1 + f2)) & ( min_p (f1 + f2)) <= ( len (f1 + f2)) by FINSEQ_3: 25;

      then

       A5: ( min_p (f1 + f2)) in ( Seg ( len f1)) by A3, FINSEQ_1: 1;

      then ( min_p (f1 + f2)) in ( dom f2) by A1, FINSEQ_1:def 3;

      then

       A6: (f2 . ( min_p (f1 + f2))) >= (f2 . ( min_p f2)) by A1, A2, Def2;

      ( min_p (f1 + f2)) in ( dom f1) by A5, FINSEQ_1:def 3;

      then

       A7: (f1 . ( min_p (f1 + f2))) >= (f1 . ( min_p f1)) by A2, Def2;

      ( min (f1 + f2)) = ((f1 . ( min_p (f1 + f2))) + (f2 . ( min_p (f1 + f2)))) by A4, VALUED_1:def 1;

      hence thesis by A7, A6, XREAL_1: 7;

    end;

    theorem :: RFINSEQ2:9

    for f be FinSequence of REAL , a be Real st ( len f) > 0 & a > 0 holds ( max (a * f)) = (a * ( max f)) & ( max_p (a * f)) = ( max_p f)

    proof

      let f be FinSequence of REAL , a be Real;

      assume that

       A1: ( len f) > 0 and

       A2: a > 0 ;

      

       A3: ( len (a * f)) = ( len f) by RVSUM_1: 117;

      then

       A4: ( max_p (a * f)) in ( dom (a * f)) by A1, Def1;

      then 1 <= ( max_p (a * f)) & ( max_p (a * f)) <= ( len (a * f)) by FINSEQ_3: 25;

      then ( max_p (a * f)) in ( Seg ( len f)) by A3, FINSEQ_1: 1;

      then

       A5: ( max_p (a * f)) in ( dom f) by FINSEQ_1:def 3;

      then (f . ( max_p f)) >= (f . ( max_p (a * f))) by A1, Def1;

      then

       A6: (a * (f . ( max_p f))) >= (a * (f . ( max_p (a * f)))) by A2, XREAL_1: 64;

      

       A7: (a * (f . ( max_p f))) = ((a * f) . ( max_p f)) & (a * (f . ( max_p (a * f)))) = ((a * f) . ( max_p (a * f))) by RVSUM_1: 44;

      

       A8: ( dom (a * f)) = ( dom f) by VALUED_1:def 5;

      then

       A9: ( max_p f) in ( dom (a * f)) by A1, Def1;

      then ((a * f) . ( max_p f)) <= ((a * f) . ( max_p (a * f))) by A1, A3, Def1;

      then

       A10: (f . ( max_p f)) <= (f . ( max_p (a * f))) by A2, A7, XREAL_1: 68;

      (f . ( max_p (a * f))) <= (f . ( max_p f)) by A1, A5, Def1;

      then (f . ( max_p f)) = (f . ( max_p (a * f))) by A10, XXREAL_0: 1;

      then

       A11: ( max (a * f)) = (a * (f . ( max_p (a * f)))) & ( max_p (a * f)) >= ( max_p f) by A1, A8, A4, Def1, RVSUM_1: 44;

      ( max_p f) in ( dom (a * f)) by A1, A8, Def1;

      then ((a * f) . ( max_p (a * f))) >= ((a * f) . ( max_p f)) by A1, A3, Def1;

      then ((a * f) . ( max_p (a * f))) = ((a * f) . ( max_p f)) by A7, A6, XXREAL_0: 1;

      then ( max_p (a * f)) <= ( max_p f) by A1, A3, A9, Def1;

      hence thesis by A11, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:10

    for f be FinSequence of REAL , a be Real st ( len f) > 0 & a > 0 holds ( min (a * f)) = (a * ( min f)) & ( min_p (a * f)) = ( min_p f)

    proof

      let f be FinSequence of REAL , a be Real;

      assume that

       A1: ( len f) > 0 and

       A2: a > 0 ;

      

       A3: ( len (a * f)) = ( len f) by RVSUM_1: 117;

      then

       A4: ( min_p (a * f)) in ( dom (a * f)) by A1, Def2;

      then 1 <= ( min_p (a * f)) & ( min_p (a * f)) <= ( len (a * f)) by FINSEQ_3: 25;

      then

       A5: ( min_p (a * f)) in ( dom f) by A3, FINSEQ_3: 25;

      then (f . ( min_p f)) <= (f . ( min_p (a * f))) by A1, Def2;

      then

       A6: (a * (f . ( min_p f))) <= (a * (f . ( min_p (a * f)))) by A2, XREAL_1: 64;

      

       A7: (a * (f . ( min_p f))) = ((a * f) . ( min_p f)) & (a * (f . ( min_p (a * f)))) = ((a * f) . ( min_p (a * f))) by RVSUM_1: 44;

      

       A8: ( dom (a * f)) = ( dom f) by VALUED_1:def 5;

      then

       A9: ( min_p f) in ( dom (a * f)) by A1, Def2;

      then ((a * f) . ( min_p f)) >= ((a * f) . ( min_p (a * f))) by A1, A3, Def2;

      then

       A10: (f . ( min_p f)) >= (f . ( min_p (a * f))) by A2, A7, XREAL_1: 68;

      (f . ( min_p (a * f))) >= (f . ( min_p f)) by A1, A5, Def2;

      then (f . ( min_p f)) = (f . ( min_p (a * f))) by A10, XXREAL_0: 1;

      then

       A11: ( min (a * f)) = (a * (f . ( min_p (a * f)))) & ( min_p (a * f)) >= ( min_p f) by A1, A8, A4, Def2, RVSUM_1: 44;

      ( min_p f) in ( dom (a * f)) by A1, A8, Def2;

      then ((a * f) . ( min_p (a * f))) <= ((a * f) . ( min_p f)) by A1, A3, Def2;

      then ((a * f) . ( min_p (a * f))) = ((a * f) . ( min_p f)) by A7, A6, XXREAL_0: 1;

      then ( min_p (a * f)) <= ( min_p f) by A1, A3, A9, Def2;

      hence thesis by A11, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:11

    for f be FinSequence of REAL st ( len f) > 0 holds ( max ( - f)) = ( - ( min f)) & ( max_p ( - f)) = ( min_p f)

    proof

      let f be FinSequence of REAL ;

      assume

       A1: ( len f) > 0 ;

      

       A2: ( len ( - f)) = ( len f) by RVSUM_1: 114;

      then

       A3: ( max_p ( - f)) in ( dom ( - f)) by A1, Def1;

      then 1 <= ( max_p ( - f)) & ( max_p ( - f)) <= ( len ( - f)) by FINSEQ_3: 25;

      then ( max_p ( - f)) in ( Seg ( len f)) by A2, FINSEQ_1: 1;

      then

       A4: ( max_p ( - f)) in ( dom f) by FINSEQ_1:def 3;

      then (f . ( min_p f)) <= (f . ( max_p ( - f))) by A1, Def2;

      then

       A5: ( - (f . ( min_p f))) >= ( - (f . ( max_p ( - f)))) by XREAL_1: 24;

      

       A6: ( - (f . ( min_p f))) = (( - f) . ( min_p f)) & ( - (f . ( max_p ( - f)))) = (( - f) . ( max_p ( - f))) by RVSUM_1: 17;

      

       A7: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

      then

       A8: ( min_p f) in ( dom ( - f)) by A1, Def2;

      then (( - f) . ( max_p ( - f))) >= (( - f) . ( min_p f)) by A1, A2, Def1;

      then

       A9: (f . ( max_p ( - f))) <= (f . ( min_p f)) by A6, XREAL_1: 24;

      (f . ( min_p f)) <= (f . ( max_p ( - f))) by A1, A4, Def2;

      then (f . ( min_p f)) = (f . ( max_p ( - f))) by A9, XXREAL_0: 1;

      then

       A10: ( max ( - f)) = ( - (f . ( max_p ( - f)))) & ( max_p ( - f)) >= ( min_p f) by A1, A7, A3, Def2, RVSUM_1: 17;

      ( min_p f) in ( dom ( - f)) by A1, A7, Def2;

      then (( - f) . ( max_p ( - f))) >= (( - f) . ( min_p f)) by A1, A2, Def1;

      then (( - f) . ( max_p ( - f))) = (( - f) . ( min_p f)) by A6, A5, XXREAL_0: 1;

      then ( max_p ( - f)) <= ( min_p f) by A1, A2, A8, Def1;

      hence thesis by A10, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:12

    for f be FinSequence of REAL st ( len f) > 0 holds ( min ( - f)) = ( - ( max f)) & ( min_p ( - f)) = ( max_p f)

    proof

      let f be FinSequence of REAL ;

      assume

       A1: ( len f) > 0 ;

      

       A2: ( len ( - f)) = ( len f) by RVSUM_1: 114;

      then

       A3: ( min_p ( - f)) in ( dom ( - f)) by A1, Def2;

      then 1 <= ( min_p ( - f)) & ( min_p ( - f)) <= ( len ( - f)) by FINSEQ_3: 25;

      then ( min_p ( - f)) in ( Seg ( len f)) by A2, FINSEQ_1: 1;

      then

       A4: ( min_p ( - f)) in ( dom f) by FINSEQ_1:def 3;

      then (f . ( max_p f)) >= (f . ( min_p ( - f))) by A1, Def1;

      then

       A5: ( - (f . ( max_p f))) <= ( - (f . ( min_p ( - f)))) by XREAL_1: 24;

      

       A6: ( - (f . ( max_p f))) = (( - f) . ( max_p f)) & ( - (f . ( min_p ( - f)))) = (( - f) . ( min_p ( - f))) by RVSUM_1: 17;

      

       A7: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

      then

       A8: ( max_p f) in ( dom ( - f)) by A1, Def1;

      then (( - f) . ( min_p ( - f))) <= (( - f) . ( max_p f)) by A1, A2, Def2;

      then

       A9: (f . ( min_p ( - f))) >= (f . ( max_p f)) by A6, XREAL_1: 24;

      (f . ( max_p f)) >= (f . ( min_p ( - f))) by A1, A4, Def1;

      then (f . ( max_p f)) = (f . ( min_p ( - f))) by A9, XXREAL_0: 1;

      then

       A10: ( min ( - f)) = ( - (f . ( min_p ( - f)))) & ( min_p ( - f)) >= ( max_p f) by A1, A7, A3, Def1, RVSUM_1: 17;

      ( max_p f) in ( dom ( - f)) by A1, A7, Def1;

      then (( - f) . ( min_p ( - f))) <= (( - f) . ( max_p f)) by A1, A2, Def2;

      then (( - f) . ( min_p ( - f))) = (( - f) . ( max_p f)) by A6, A5, XXREAL_0: 1;

      then ( min_p ( - f)) <= ( max_p f) by A1, A2, A8, Def2;

      hence thesis by A10, XXREAL_0: 1;

    end;

    theorem :: RFINSEQ2:13

    for f be FinSequence of REAL , n be Nat st n < ( len f) holds ( max (f /^ n)) <= ( max f) & ( min (f /^ n)) >= ( min f)

    proof

      let f be FinSequence of REAL , n be Nat;

      

       A1: 1 <= (1 + n) by NAT_1: 12;

      assume

       A2: n < ( len f);

      then

       A3: ( len (f /^ n)) = (( len f) - n) by RFINSEQ:def 1;

      then

       A4: ( len (f /^ n)) > 0 by A2, XREAL_1: 50;

      then

       A5: ( min_p (f /^ n)) in ( dom (f /^ n)) by Def2;

      then

       A6: (f . (( min_p (f /^ n)) + n)) = ( min (f /^ n)) by A2, RFINSEQ:def 1;

      ( min_p (f /^ n)) <= ( len (f /^ n)) by A5, FINSEQ_3: 25;

      then

       A7: (( min_p (f /^ n)) + n) <= ((( len f) - n) + n) by A3, XREAL_1: 7;

      

       A8: 1 <= (1 + n) by NAT_1: 12;

      1 <= ( min_p (f /^ n)) by A5, FINSEQ_3: 25;

      then (1 + n) <= (( min_p (f /^ n)) + n) by XREAL_1: 7;

      then 1 <= (( min_p (f /^ n)) + n) by A8, XXREAL_0: 2;

      then

       A9: (( min_p (f /^ n)) + n) in ( dom f) by A7, FINSEQ_3: 25;

      

       A10: ( max_p (f /^ n)) in ( dom (f /^ n)) by A4, Def1;

      then ( max_p (f /^ n)) <= ( len (f /^ n)) by FINSEQ_3: 25;

      then

       A11: (( max_p (f /^ n)) + n) <= ((( len f) - n) + n) by A3, XREAL_1: 7;

      1 <= ( max_p (f /^ n)) by A10, FINSEQ_3: 25;

      then (1 + n) <= (( max_p (f /^ n)) + n) by XREAL_1: 7;

      then 1 <= (( max_p (f /^ n)) + n) by A1, XXREAL_0: 2;

      then

       A12: (( max_p (f /^ n)) + n) in ( dom f) by A11, FINSEQ_3: 25;

      (f . (( max_p (f /^ n)) + n)) = ( max (f /^ n)) by A2, A10, RFINSEQ:def 1;

      hence thesis by A2, A12, A9, A6, Def1, Def2;

    end;

    

     Lm1: for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent holds ( max f) <= ( max g)

    proof

      let f,g be FinSequence of REAL ;

      assume

       A1: (f,g) are_fiberwise_equipotent ;

      then

      consider P be Permutation of ( dom g) such that

       A2: f = (g * P) by RFINSEQ: 4;

      

       A3: ( dom f) = ( dom g) by A1, RFINSEQ: 3;

      

       A4: ( len f) = ( len g) by A1, RFINSEQ: 3;

      per cases ;

        suppose

         A5: ( len f) > 0 ;

        then

         A6: ( max_p f) in ( dom (g * P)) by A2, Def1;

        then

         A7: ((g * P) . ( max_p f)) = (g . (P . ( max_p f))) by FUNCT_1: 12;

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

        then ( dom P) = ( dom g) by A4, A5, FUNCT_2:def 1;

        then

         A8: ( rng P) = ( dom g) & (P . ( max_p f)) in ( rng P) by A2, A3, A6, FUNCT_1:def 3, FUNCT_2:def 3;

        reconsider n = (P . ( max_p f)) as Nat;

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

        then 1 <= n & n <= ( len g) by A8, FINSEQ_1: 1;

        hence thesis by A2, A7, Th1;

      end;

        suppose ( len f) <= 0 ;

        then f = {} & g = {} by A4;

        hence thesis;

      end;

    end;

    theorem :: RFINSEQ2:14

    

     Th14: for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent holds ( max f) = ( max g)

    proof

      let f,g be FinSequence of REAL ;

      assume (f,g) are_fiberwise_equipotent ;

      then ( max f) <= ( max g) & ( max g) <= ( max f) by Lm1;

      hence thesis by XXREAL_0: 1;

    end;

    

     Lm2: for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent holds ( min f) >= ( min g)

    proof

      let f,g be FinSequence of REAL ;

      assume

       A1: (f,g) are_fiberwise_equipotent ;

      then

      consider P be Permutation of ( dom g) such that

       A2: f = (g * P) by RFINSEQ: 4;

      

       A3: ( len f) = ( len g) by A1, RFINSEQ: 3;

      per cases ;

        suppose

         A4: ( len f) > 0 ;

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

        then

         A5: ( dom P) = ( dom g) by A3, A4, FUNCT_2:def 1;

        

         A6: ( min_p f) in ( dom (g * P)) by A2, A4, Def2;

        then

         A7: ((g * P) . ( min_p f)) = (g . (P . ( min_p f))) by FUNCT_1: 12;

        ( min_p f) in ( dom g) by A1, A2, A6, RFINSEQ: 3;

        then

         A8: ( rng P) = ( dom g) & (P . ( min_p f)) in ( rng P) by A5, FUNCT_1:def 3, FUNCT_2:def 3;

        reconsider n = (P . ( min_p f)) as Nat;

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

        then 1 <= n & n <= ( len g) by A8, FINSEQ_1: 1;

        hence thesis by A2, A7, Th2;

      end;

        suppose ( len f) <= 0 ;

        then f = {} & g = {} by A3;

        hence thesis;

      end;

    end;

    theorem :: RFINSEQ2:15

    

     Th15: for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent holds ( min f) = ( min g)

    proof

      let f,g be FinSequence of REAL ;

      assume (f,g) are_fiberwise_equipotent ;

      then ( min f) >= ( min g) & ( min g) >= ( min f) by Lm2;

      hence thesis by XXREAL_0: 1;

    end;

    definition

      let f be FinSequence of REAL ;

      :: RFINSEQ2:def5

      func sort_d f -> non-increasing FinSequence of REAL means

      : Def5: (f,it ) are_fiberwise_equipotent ;

      existence by RFINSEQ: 22;

      uniqueness by CLASSES1: 76, RFINSEQ: 23;

      projectivity ;

    end

    theorem :: RFINSEQ2:16

    

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

    proof

      let R be FinSequence of REAL ;

      assume

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

      per cases by A1;

        suppose ( 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;

        suppose ( 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;

    theorem :: RFINSEQ2:17

    

     Th17: for R be FinSequence of REAL holds R is non-decreasing 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-decreasing implies for n, m st n in ( dom R) & m in ( dom R) & n < m holds (R . n) <= (R . m)

      proof

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

        assume

         A1: R is non-decreasing;

        

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

        proof

          let m;

          assume

           A3: P[m];

          assume

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

          then (m + 1) <= ( len R) by FINSEQ_3: 25;

          then

           A5: m <= ( len R) by NAT_1: 13;

          let n;

          assume that

           A6: n in ( dom R) and

           A7: n < (m + 1);

          set t = (R . m), r = (R . n), s = (R . (m + 1));

          

           A8: n <= m by A7, NAT_1: 13;

          1 <= n by A6, FINSEQ_3: 25;

          then

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

          then

           A10: m in ( dom R) by A5, FINSEQ_3: 25;

          now

            per cases ;

              case n = m;

              hence thesis by A1, A4, A6;

            end;

              case n <> m;

              then n < m by A8, XXREAL_0: 1;

              then

               A11: r <= t by A3, A6, A9, A5, FINSEQ_3: 25;

              t <= s by A1, A4, A10;

              hence thesis by A11, XXREAL_0: 2;

            end;

          end;

          hence thesis;

        end;

        

         A12: P[ 0 ];

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

        hence thesis;

      end;

      assume

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

      let n;

      

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

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

      hence thesis by A13, A14;

    end;

    

     Lm3: for f,g be non-decreasing 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-decreasing 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 + 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, RFINSEQ: 7;

      

       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, Th17;

              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, Th17;

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

      now

        let x be object;

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

        .= ( card ( Coim (g,x))) by A3, CLASSES1:def 10

        .= (( card ((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 by CLASSES1:def 10;

    end;

    theorem :: RFINSEQ2:18

    

     Th18: for R be non-decreasing FinSequence of REAL , n be Nat holds (R | n) is non-decreasing FinSequence of REAL

    proof

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

      set fn = (f | n);

      now

        per cases ;

          case n = 0 ;

          then ( len fn) = 0 ;

          hence thesis by Th16;

        end;

          case n <> 0 ;

          then

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

          now

            per cases ;

              case ( len f) <= n;

              hence thesis by FINSEQ_1: 58;

            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, RFINSEQ: 6;

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

                hence (fn . m) <= (fn . (m + 1)) by A5, INTEGRA2:def 1;

              end;

              hence thesis by INTEGRA2:def 1;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    

     Lm4: for n holds for g1,g2 be non-decreasing 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-decreasing 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-decreasing FinSequence of REAL ;

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

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

        assume that

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

         A4: (g1,g2) are_fiberwise_equipotent ;

        

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

        then

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

        

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

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

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

        hence thesis by A3, A5, A6, A7, RFINSEQ: 7;

      end;

      

       A8: P[ 0 ]

      proof

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

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

        then ( len g2) = ( len g1) & g1 = ( <*> REAL ) by RFINSEQ: 3;

        hence thesis;

      end;

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

      hence thesis;

    end;

    theorem :: RFINSEQ2:19

    

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

    proof

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

      

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

      assume (g1,g2) are_fiberwise_equipotent ;

      hence thesis by A1, Lm4;

    end;

    definition

      let f be FinSequence of REAL ;

      :: RFINSEQ2:def6

      func sort_a f -> non-decreasing FinSequence of REAL means

      : Def6: (f,it ) are_fiberwise_equipotent ;

      existence by INTEGRA2: 3;

      uniqueness by Th19, CLASSES1: 76;

      projectivity ;

    end

    theorem :: RFINSEQ2:20

    for f be non-increasing FinSequence of REAL holds ( sort_d f) = f by Def5;

    theorem :: RFINSEQ2:21

    for f be non-decreasing FinSequence of REAL holds ( sort_a f) = f by Def6;

    ::$Canceled

    theorem :: RFINSEQ2:24

    

     Th22: for f be FinSequence of REAL st f is non-increasing holds ( - f) is non-decreasing

    proof

      let f be FinSequence of REAL ;

      assume

       A1: f is non-increasing;

      for n be Nat st n in ( dom ( - f)) & (n + 1) in ( dom ( - f)) holds (( - f) . n) <= (( - f) . (n + 1))

      proof

        let n be Nat;

        

         A2: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

        

         A3: (( - f) . n) = ( - (f . n)) & (( - f) . (n + 1)) = ( - (f . (n + 1))) by RVSUM_1: 17;

        assume n in ( dom ( - f)) & (n + 1) in ( dom ( - f));

        then (f . n) >= (f . (n + 1)) by A1, A2, RFINSEQ:def 3;

        hence thesis by A3, XREAL_1: 24;

      end;

      hence thesis;

    end;

    theorem :: RFINSEQ2:25

    

     Th23: for f be FinSequence of REAL st f is non-decreasing holds ( - f) is non-increasing

    proof

      let f be FinSequence of REAL ;

      assume

       A1: f is non-decreasing;

      for n be Nat st n in ( dom ( - f)) & (n + 1) in ( dom ( - f)) holds (( - f) . n) >= (( - f) . (n + 1))

      proof

        let n be Nat;

        

         A2: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

        

         A3: (( - f) . n) = ( - (f . n)) & (( - f) . (n + 1)) = ( - (f . (n + 1))) by RVSUM_1: 17;

        assume n in ( dom ( - f)) & (n + 1) in ( dom ( - f));

        then (f . n) <= (f . (n + 1)) by A1, A2;

        hence thesis by A3, XREAL_1: 24;

      end;

      hence thesis by RFINSEQ:def 3;

    end;

    theorem :: RFINSEQ2:26

    

     Th24: for f,g be FinSequence of REAL , P be Permutation of ( dom g) st f = (g * P) & ( len g) >= 1 holds ( - f) = (( - g) * P)

    proof

      let f,g be FinSequence of REAL , P be Permutation of ( dom g);

      assume that

       A1: f = (g * P) and

       A2: ( len g) >= 1;

      

       A3: ( rng P) = ( dom g) by FUNCT_2:def 3;

      

       A4: ( dom ( - g)) = ( dom g) by VALUED_1: 8;

      then

       A5: ( rng (( - g) * P)) = ( rng ( - g)) by A3, RELAT_1: 28;

      

       A6: ( dom ( - f)) = ( dom (g * P)) by A1, VALUED_1: 8;

      then

       A7: ( dom ( - f)) = ( dom P) by A3, RELAT_1: 27;

      then

       A8: ( dom ( - f)) = ( dom (( - g) * P)) by A3, A4, RELAT_1: 27;

      

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

      then ( dom P) = ( dom g) by A2, FUNCT_2:def 1;

      then (( - g) * P) is FinSequence by A9, A7, A8, FINSEQ_1:def 2;

      then

      reconsider k = (( - g) * P) as FinSequence of REAL by A5, FINSEQ_1:def 4;

      for i be Nat st i in ( dom ( - f)) holds (( - f) . i) = (k . i)

      proof

        let i be Nat;

        assume

         A10: i in ( dom ( - f));

        reconsider j = (P . i) as Nat;

        (( - f) . i) = ( - (f . i)) by RVSUM_1: 17

        .= ( - (g . (P . i))) by A1, A6, A10, FUNCT_1: 12

        .= (( - g) . j) by RVSUM_1: 17

        .= ((( - g) * P) . i) by A8, A10, FUNCT_1: 12;

        hence thesis;

      end;

      hence thesis by A8, FINSEQ_1: 13;

    end;

    theorem :: RFINSEQ2:27

    

     Th25: for f,g be FinSequence of REAL st (f,g) are_fiberwise_equipotent holds (( - f),( - g)) are_fiberwise_equipotent

    proof

      let f,g be FinSequence of REAL ;

      assume

       A1: (f,g) are_fiberwise_equipotent ;

      then

      consider P be Permutation of ( dom g) such that

       A2: f = (g * P) by RFINSEQ: 4;

       A3:

      now

        per cases ;

          case ( len g) >= 1;

          hence ( - f) = (( - g) * P) by A2, Th24;

        end;

          case ( len g) < 1;

          then ( len g) < ( 0 + 1);

          then

           A4: ( len g) = 0 by NAT_1: 13;

          then

           A5: g = {} ;

          

           A6: ( len f) = 0 by A1, A4, RFINSEQ: 3;

          then ( len ( - f)) = 0 by RVSUM_1: 114;

          then

           A7: ( - f) = {} ;

          f = {} by A6;

          hence ( - f) = (( - g) * P) by A2, A5, A7;

        end;

      end;

      ( dom ( - g)) = ( dom g) by VALUED_1: 8;

      hence thesis by A3, RFINSEQ: 4;

    end;

    theorem :: RFINSEQ2:28

    for f be FinSequence of REAL holds ( sort_d ( - f)) = ( - ( sort_a f))

    proof

      let f be FinSequence of REAL ;

      (( - f),( sort_d ( - f))) are_fiberwise_equipotent by Def5;

      then

       A1: (( - ( - f)),( - ( sort_d ( - f)))) are_fiberwise_equipotent by Th25;

      ( - ( sort_d ( - f))) is non-decreasing by Th22;

      then ( - ( sort_d ( - f))) = ( sort_a f) by A1, Def6;

      hence thesis;

    end;

    theorem :: RFINSEQ2:29

    for f be FinSequence of REAL holds ( sort_a ( - f)) = ( - ( sort_d f))

    proof

      let f be FinSequence of REAL ;

      (( - f),( sort_a ( - f))) are_fiberwise_equipotent by Def6;

      then

       A1: (( - ( - f)),( - ( sort_a ( - f)))) are_fiberwise_equipotent by Th25;

      ( - ( sort_a ( - f))) is non-increasing by Th23;

      then ( - ( sort_a ( - f))) = ( sort_d f) by A1, Def5;

      hence thesis;

    end;

    theorem :: RFINSEQ2:30

    

     Th28: for f be FinSequence of REAL holds ( dom ( sort_d f)) = ( dom f) & ( len ( sort_d f)) = ( len f)

    proof

      let f be FinSequence of REAL ;

      (f,( sort_d f)) are_fiberwise_equipotent by Def5;

      hence thesis by RFINSEQ: 3;

    end;

    theorem :: RFINSEQ2:31

    

     Th29: for f be FinSequence of REAL holds ( dom ( sort_a f)) = ( dom f) & ( len ( sort_a f)) = ( len f)

    proof

      let f be FinSequence of REAL ;

      (f,( sort_a f)) are_fiberwise_equipotent by Def6;

      hence thesis by RFINSEQ: 3;

    end;

    theorem :: RFINSEQ2:32

    for f be FinSequence of REAL st ( len f) >= 1 holds ( max_p ( sort_d f)) = 1 & ( min_p ( sort_a f)) = 1 & (( sort_d f) . 1) = ( max f) & (( sort_a f) . 1) = ( min f)

    proof

      let f be FinSequence of REAL ;

      assume

       A1: ( len f) >= 1;

      

       A2: ( len ( sort_d f)) = ( len f) by Th28;

      then 1 in ( Seg ( len ( sort_d f))) by A1, FINSEQ_1: 1;

      then

       A3: 1 in ( dom ( sort_d f)) by FINSEQ_1:def 3;

      

       A4: for i be Nat, r1,r2 be Real st i in ( dom ( sort_d f)) & r1 = (( sort_d f) . i) & r2 = (( sort_d f) . 1) holds r1 <= r2

      proof

        let i be Nat, r1,r2 be Real;

        assume that

         A5: i in ( dom ( sort_d f)) and

         A6: r1 = (( sort_d f) . i) & r2 = (( sort_d f) . 1);

        i in ( Seg ( len ( sort_d f))) by A5, FINSEQ_1:def 3;

        then

         A7: 1 <= i by FINSEQ_1: 1;

        now

          per cases ;

            case 1 = i;

            hence thesis by A6;

          end;

            case 1 <> i;

            then 1 < i by A7, XXREAL_0: 1;

            hence thesis by A3, A5, A6, RFINSEQ: 19;

          end;

        end;

        hence thesis;

      end;

      

       A8: ( len ( sort_a f)) = ( len f) by Th29;

      then

       A9: 1 in ( dom ( sort_a f)) by A1, FINSEQ_3: 25;

      

       A10: for i be Nat, r1,r2 be Real st i in ( dom ( sort_a f)) & r1 = (( sort_a f) . i) & r2 = (( sort_a f) . 1) holds r1 >= r2

      proof

        let i be Nat, r1,r2 be Real;

        assume that

         A11: i in ( dom ( sort_a f)) and

         A12: r1 = (( sort_a f) . i) & r2 = (( sort_a f) . 1);

        

         A13: 1 <= i by A11, FINSEQ_3: 25;

        per cases ;

          suppose 1 = i;

          hence thesis by A12;

        end;

          suppose 1 <> i;

          then 1 < i by A13, XXREAL_0: 1;

          hence thesis by A9, A11, A12, Th17;

        end;

      end;

      

       A14: (f,( sort_a f)) are_fiberwise_equipotent by Def6;

      

       A15: (f,( sort_d f)) are_fiberwise_equipotent by Def5;

      

       A16: for j be Nat st j in ( dom ( sort_a f)) & (( sort_a f) . j) = (( sort_a f) . 1) holds 1 <= j by FINSEQ_3: 25;

      

      then

       A17: (( sort_a f) . 1) = ( min ( sort_a f)) by A1, A8, A9, A10, Def2

      .= ( min f) by A14, Th15;

      

       A18: for j be Nat st j in ( dom ( sort_d f)) & (( sort_d f) . j) = (( sort_d f) . 1) holds 1 <= j

      proof

        let j be Nat;

        assume that

         A19: j in ( dom ( sort_d f)) and (( sort_d f) . j) = (( sort_d f) . 1);

        j in ( Seg ( len ( sort_d f))) by A19, FINSEQ_1:def 3;

        hence thesis by FINSEQ_1: 1;

      end;

      

      then (( sort_d f) . 1) = ( max ( sort_d f)) by A1, A2, A3, A4, Def1

      .= ( max f) by A15, Th14;

      hence thesis by A1, A2, A3, A4, A18, A8, A9, A10, A16, A17, Def1, Def2;

    end;