rfunct_2.miz

    begin

    reserve x,X,Y for set;

    reserve g,r,r1,r2,p,p1,p2 for Real;

    reserve R for Subset of REAL ;

    reserve seq,seq1,seq2,seq3 for Real_Sequence;

    reserve Ns for increasing sequence of NAT ;

    reserve n for Nat;

    reserve W for non empty set;

    reserve h,h1,h2 for PartFunc of W, REAL ;

    theorem :: RFUNCT_2:1



     Th1: seq1 = (seq2 - seq3) iff for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

    proof

      thus seq1 = (seq2 - seq3) implies for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n))

      proof

        assume

         A1: seq1 = (seq2 - seq3);

        now

          let n;

          (seq1 . n) = ((seq2 . n) + (( - seq3) . n)) by A1, SEQ_1: 7;

          then (seq1 . n) = ((seq2 . n) + ( - (seq3 . n))) by SEQ_1: 10;

          hence (seq1 . n) = ((seq2 . n) - (seq3 . n));

        end;

        hence thesis;

      end;

      assume

       A2: for n holds (seq1 . n) = ((seq2 . n) - (seq3 . n));

      now

        let n;



        thus (seq1 . n) = ((seq2 . n) - (seq3 . n)) by A2

        .= ((seq2 . n) + ( - (seq3 . n)))

        .= ((seq2 . n) + (( - seq3) . n)) by SEQ_1: 10;

      end;

      hence thesis by SEQ_1: 7;

    end;

    theorem :: RFUNCT_2:2



     Th2: ((seq1 + seq2) * Ns) = ((seq1 * Ns) + (seq2 * Ns)) & ((seq1 - seq2) * Ns) = ((seq1 * Ns) - (seq2 * Ns)) & ((seq1 (#) seq2) * Ns) = ((seq1 * Ns) (#) (seq2 * Ns))

    proof

      now

        let n be Element of NAT ;



        thus (((seq1 + seq2) * Ns) . n) = ((seq1 + seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) + (seq2 . (Ns . n))) by SEQ_1: 7

        .= (((seq1 * Ns) . n) + (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) + ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) + (seq2 * Ns)) . n) by SEQ_1: 7;

      end;

      hence ((seq1 + seq2) * Ns) = ((seq1 * Ns) + (seq2 * Ns)) by FUNCT_2: 63;

      now

        let n be Element of NAT ;



        thus (((seq1 - seq2) * Ns) . n) = ((seq1 - seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) - (seq2 . (Ns . n))) by Th1

        .= (((seq1 * Ns) . n) - (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) - ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) - (seq2 * Ns)) . n) by Th1;

      end;

      hence ((seq1 - seq2) * Ns) = ((seq1 * Ns) - (seq2 * Ns)) by FUNCT_2: 63;

      now

        let n be Element of NAT ;



        thus (((seq1 (#) seq2) * Ns) . n) = ((seq1 (#) seq2) . (Ns . n)) by FUNCT_2: 15

        .= ((seq1 . (Ns . n)) * (seq2 . (Ns . n))) by SEQ_1: 8

        .= (((seq1 * Ns) . n) * (seq2 . (Ns . n))) by FUNCT_2: 15

        .= (((seq1 * Ns) . n) * ((seq2 * Ns) . n)) by FUNCT_2: 15

        .= (((seq1 * Ns) (#) (seq2 * Ns)) . n) by SEQ_1: 8;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:3



     Th3: ((p (#) seq) * Ns) = (p (#) (seq * Ns))

    proof

      now

        let n be Element of NAT ;



        thus (((p (#) seq) * Ns) . n) = ((p (#) seq) . (Ns . n)) by FUNCT_2: 15

        .= (p * (seq . (Ns . n))) by SEQ_1: 9

        .= (p * ((seq * Ns) . n)) by FUNCT_2: 15

        .= ((p (#) (seq * Ns)) . n) by SEQ_1: 9;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:4

    (( - seq) * Ns) = ( - (seq * Ns)) & (( abs seq) * Ns) = ( abs (seq * Ns))

    proof



      thus (( - seq) * Ns) = ((( - 1) (#) seq) * Ns)

      .= (( - 1) (#) (seq * Ns)) by Th3

      .= ( - (seq * Ns));

      now

        let n be Element of NAT ;



        thus ((( abs seq) * Ns) . n) = (( abs seq) . (Ns . n)) by FUNCT_2: 15

        .= |.(seq . (Ns . n)).| by SEQ_1: 12

        .= |.((seq * Ns) . n).| by FUNCT_2: 15

        .= (( abs (seq * Ns)) . n) by SEQ_1: 12;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:5



     Th5: ((seq * Ns) " ) = ((seq " ) * Ns)

    proof

      now

        let n be Element of NAT ;



        thus (((seq * Ns) " ) . n) = (((seq * Ns) . n) " ) by VALUED_1: 10

        .= ((seq . (Ns . n)) " ) by FUNCT_2: 15

        .= ((seq " ) . (Ns . n)) by VALUED_1: 10

        .= (((seq " ) * Ns) . n) by FUNCT_2: 15;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:6

    ((seq1 /" seq) * Ns) = ((seq1 * Ns) /" (seq * Ns))

    proof



      thus ((seq1 /" seq) * Ns) = ((seq1 (#) (seq " )) * Ns)

      .= ((seq1 * Ns) (#) ((seq " ) * Ns)) by Th2

      .= ((seq1 * Ns) (#) ((seq * Ns) " )) by Th5

      .= ((seq1 * Ns) /" (seq * Ns));

    end;

    theorem :: RFUNCT_2:7

    seq is convergent & (for n holds (seq . n) <= 0 ) implies ( lim seq) <= 0

    proof

      assume that

       A1: seq is convergent and

       A2: for n holds (seq . n) <= 0 ;

      set seq1 = ( - seq);

       A3:

      now

        let n;

        (seq1 . n) = ( - (seq . n)) & (seq . n) <= 0 by A2, SEQ_1: 10;

        hence ( - 0 qua Real) <= (seq1 . n) by XREAL_1: 24;

      end;

      seq1 is convergent by A1, SEQ_2: 9;

      then 0 <= ( lim seq1) by A3, SEQ_2: 17;

      then ( - 0 qua Real) <= ( - ( lim seq)) by A1, SEQ_2: 10;

      hence thesis by XREAL_1: 24;

    end;

    theorem :: RFUNCT_2:8



     Th8: for h1,h2 be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= (( dom h1) /\ ( dom h2)) implies ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) & ((h1 (#) h2) /* seq) = ((h1 /* seq) (#) (h2 /* seq))

    proof

      let h1,h2 be PartFunc of W, REAL , seq be sequence of W;



       A1: (( dom h1) /\ ( dom h2)) c= ( dom h1) by XBOOLE_1: 17;



       A2: (( dom h1) /\ ( dom h2)) c= ( dom h2) by XBOOLE_1: 17;

      assume

       A3: ( rng seq) c= (( dom h1) /\ ( dom h2));

      then

       A4: ( rng seq) c= ( dom (h1 + h2)) by VALUED_1:def 1;

      now

        let n;



         A5: n in NAT by ORDINAL1:def 12;



         A6: (seq . n) in ( rng seq) by VALUED_0: 28;



        thus (((h1 + h2) /* seq) . n) = ((h1 + h2) . (seq . n)) by A4, FUNCT_2: 108, A5

        .= ((h1 . (seq . n)) + (h2 . (seq . n))) by A4, A6, VALUED_1:def 1

        .= (((h1 /* seq) . n) + (h2 . (seq . n))) by A3, A1, FUNCT_2: 108, XBOOLE_1: 1, A5

        .= (((h1 /* seq) . n) + ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 108, XBOOLE_1: 1, A5;

      end;

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by SEQ_1: 7;



       A7: ( rng seq) c= ( dom (h1 - h2)) by A3, VALUED_1: 12;

      now

        let n;



         A8: n in NAT by ORDINAL1:def 12;



         A9: (seq . n) in ( rng seq) by VALUED_0: 28;



        thus (((h1 - h2) /* seq) . n) = ((h1 - h2) . (seq . n)) by A7, FUNCT_2: 108, A8

        .= ((h1 . (seq . n)) - (h2 . (seq . n))) by A7, A9, VALUED_1: 13

        .= (((h1 /* seq) . n) - (h2 . (seq . n))) by A3, A1, FUNCT_2: 108, XBOOLE_1: 1, A8

        .= (((h1 /* seq) . n) - ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 108, XBOOLE_1: 1, A8;

      end;

      hence ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) by Th1;



       A10: ( rng seq) c= ( dom (h1 (#) h2)) by A3, VALUED_1:def 4;

      now

        let n;



         A11: n in NAT by ORDINAL1:def 12;



        thus (((h1 (#) h2) /* seq) . n) = ((h1 (#) h2) . (seq . n)) by A10, FUNCT_2: 108, A11

        .= ((h1 . (seq . n)) * (h2 . (seq . n))) by VALUED_1: 5

        .= (((h1 /* seq) . n) * (h2 . (seq . n))) by A3, A1, FUNCT_2: 108, XBOOLE_1: 1, A11

        .= (((h1 /* seq) . n) * ((h2 /* seq) . n)) by A3, A2, FUNCT_2: 108, XBOOLE_1: 1, A11;

      end;

      hence thesis by SEQ_1: 8;

    end;

    theorem :: RFUNCT_2:9



     Th9: for h be PartFunc of W, REAL , seq be sequence of W holds for r be Real holds ( rng seq) c= ( dom h) implies ((r (#) h) /* seq) = (r (#) (h /* seq))

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      let r be Real;

      assume

       A1: ( rng seq) c= ( dom h);

      then

       A2: ( rng seq) c= ( dom (r (#) h)) by VALUED_1:def 5;

      now

        let n;



         A3: n in NAT by ORDINAL1:def 12;



         A4: (seq . n) in ( rng seq) by VALUED_0: 28;



        thus (((r (#) h) /* seq) . n) = ((r (#) h) . (seq . n)) by A2, FUNCT_2: 108, A3

        .= (r * (h . (seq . n))) by A2, A4, VALUED_1:def 5

        .= (r * ((h /* seq) . n)) by A1, FUNCT_2: 108, A3;

      end;

      hence thesis by SEQ_1: 9;

    end;

    theorem :: RFUNCT_2:10

    for h be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= ( dom h) implies ( abs (h /* seq)) = (( abs h) /* seq) & ( - (h /* seq)) = (( - h) /* seq)

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume

       A1: ( rng seq) c= ( dom h);

      then

       A2: ( rng seq) c= ( dom ( abs h)) by VALUED_1:def 11;

      now

        let n be Element of NAT ;



        thus (( abs (h /* seq)) . n) = |.((h /* seq) . n).| by SEQ_1: 12

        .= |.(h . (seq . n)).| by A1, FUNCT_2: 108

        .= (( abs h) . (seq . n)) by VALUED_1: 18

        .= ((( abs h) /* seq) . n) by A2, FUNCT_2: 108;

      end;

      hence ( abs (h /* seq)) = (( abs h) /* seq) by FUNCT_2: 63;



      thus ( - (h /* seq)) = (( - 1) (#) (h /* seq))

      .= ((( - 1) (#) h) /* seq) by A1, Th9

      .= (( - h) /* seq);

    end;

    theorem :: RFUNCT_2:11

    for h be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= ( dom (h ^ )) implies (h /* seq) is non-zero

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume

       A1: ( rng seq) c= ( dom (h ^ ));

      then

       A2: (( dom h) \ (h " { 0 })) c= ( dom h) & ( rng seq) c= (( dom h) \ (h " { 0 })) by RFUNCT_1:def 2, XBOOLE_1: 36;

      now

        given n such that

         A3: ((h /* seq) . n) = 0 ;



         A4: n in NAT by ORDINAL1:def 12;

        (seq . n) in ( rng seq) by VALUED_0: 28;

        then (seq . n) in ( dom (h ^ )) by A1;

        then (seq . n) in (( dom h) \ (h " { 0 })) by RFUNCT_1:def 2;

        then (seq . n) in ( dom h) & not (seq . n) in (h " { 0 }) by XBOOLE_0:def 5;

        then

         A5: not (h . (seq . n)) in { 0 } by FUNCT_1:def 7;

        (h . (seq . n)) = 0 by A2, A3, FUNCT_2: 108, XBOOLE_1: 1, A4;

        hence contradiction by A5, TARSKI:def 1;

      end;

      hence thesis by SEQ_1: 5;

    end;

    theorem :: RFUNCT_2:12

    for h be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= ( dom (h ^ )) implies ((h ^ ) /* seq) = ((h /* seq) " )

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume

       A1: ( rng seq) c= ( dom (h ^ ));

      then

       A2: (( dom h) \ (h " { 0 })) c= ( dom h) & ( rng seq) c= (( dom h) \ (h " { 0 })) by RFUNCT_1:def 2, XBOOLE_1: 36;

      now

        let n be Element of NAT ;



         A3: (seq . n) in ( rng seq) by VALUED_0: 28;



        thus (((h ^ ) /* seq) . n) = ((h ^ ) . (seq . n)) by A1, FUNCT_2: 108

        .= ((h . (seq . n)) " ) by A1, A3, RFUNCT_1:def 2

        .= (((h /* seq) . n) " ) by A2, FUNCT_2: 108, XBOOLE_1: 1

        .= (((h /* seq) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:13

    for h1,h2 be PartFunc of W, REAL , seq be sequence of W holds h1 is total & h2 is total implies ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) & ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) & ((h1 (#) h2) /* seq) = ((h1 /* seq) (#) (h2 /* seq))

    proof

      let h1,h2 be PartFunc of W, REAL , seq be sequence of W;

      assume h1 is total & h2 is total;

      then ( dom (h1 + h2)) = W by PARTFUN1:def 2;

      then (( dom h1) /\ ( dom h2)) = W by VALUED_1:def 1;

      then

       A1: ( rng seq) c= (( dom h1) /\ ( dom h2));

      hence ((h1 + h2) /* seq) = ((h1 /* seq) + (h2 /* seq)) by Th8;

      thus ((h1 - h2) /* seq) = ((h1 /* seq) - (h2 /* seq)) by A1, Th8;

      thus thesis by A1, Th8;

    end;

    theorem :: RFUNCT_2:14

    for h be PartFunc of W, REAL , seq be sequence of W holds h is total implies ((r (#) h) /* seq) = (r (#) (h /* seq))

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume h is total;

      then ( dom h) = W by PARTFUN1:def 2;

      then ( rng seq) c= ( dom h);

      hence thesis by Th9;

    end;

    theorem :: RFUNCT_2:15

    for h be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= ( dom (h | X)) implies ( abs ((h | X) /* seq)) = ((( abs h) | X) /* seq)

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume

       A1: ( rng seq) c= ( dom (h | X));



       A2: ( dom (h | X)) = (( dom h) /\ X) by RELAT_1: 61

      .= (( dom ( abs h)) /\ X) by VALUED_1:def 11

      .= ( dom (( abs h) | X)) by RELAT_1: 61;

      now

        let n be Element of NAT ;



         A3: (seq . n) in ( rng seq) by VALUED_0: 28;

        then (seq . n) in ( dom (h | X)) by A1;

        then (seq . n) in (( dom h) /\ X) by RELAT_1: 61;

        then

         A4: (seq . n) in X by XBOOLE_0:def 4;



        thus (( abs ((h | X) /* seq)) . n) = |.(((h | X) /* seq) . n).| by SEQ_1: 12

        .= |.((h | X) . (seq . n)).| by A1, FUNCT_2: 108

        .= |.(h . (seq . n)).| by A1, A3, FUNCT_1: 47

        .= (( abs h) . (seq . n)) by VALUED_1: 18

        .= ((( abs h) | X) . (seq . n)) by A4, FUNCT_1: 49

        .= (((( abs h) | X) /* seq) . n) by A1, A2, FUNCT_2: 108;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    theorem :: RFUNCT_2:16

    for h be PartFunc of W, REAL , seq be sequence of W holds ( rng seq) c= ( dom (h | X)) & (h " { 0 }) = {} implies (((h ^ ) | X) /* seq) = (((h | X) /* seq) " )

    proof

      let h be PartFunc of W, REAL , seq be sequence of W;

      assume that

       A1: ( rng seq) c= ( dom (h | X)) and

       A2: (h " { 0 }) = {} ;

      now

        let x be object;

        assume x in ( rng seq);

        then x in ( dom (h | X)) by A1;

        then

         A3: x in (( dom h) /\ X) by RELAT_1: 61;

        then x in (( dom h) \ (h " { 0 })) by A2, XBOOLE_0:def 4;

        then

         A4: x in ( dom (h ^ )) by RFUNCT_1:def 2;

        x in X by A3, XBOOLE_0:def 4;

        then x in (( dom (h ^ )) /\ X) by A4, XBOOLE_0:def 4;

        hence x in ( dom ((h ^ ) | X)) by RELAT_1: 61;

      end;

      then

       A5: ( rng seq) c= ( dom ((h ^ ) | X)) by TARSKI:def 3;

      now

        let n be Element of NAT ;



         A6: (seq . n) in ( rng seq) by VALUED_0: 28;

        then (seq . n) in ( dom (h | X)) by A1;

        then

         A7: (seq . n) in (( dom h) /\ X) by RELAT_1: 61;

        then

         A8: (seq . n) in X by XBOOLE_0:def 4;

        (seq . n) in (( dom h) \ (h " { 0 })) by A2, A7, XBOOLE_0:def 4;

        then

         A9: (seq . n) in ( dom (h ^ )) by RFUNCT_1:def 2;



        thus ((((h ^ ) | X) /* seq) . n) = (((h ^ ) | X) . (seq . n)) by A5, FUNCT_2: 108

        .= ((h ^ ) . (seq . n)) by A8, FUNCT_1: 49

        .= ((h . (seq . n)) " ) by A9, RFUNCT_1:def 2

        .= (((h | X) . (seq . n)) " ) by A1, A6, FUNCT_1: 47

        .= ((((h | X) /* seq) . n) " ) by A1, FUNCT_2: 108

        .= ((((h | X) /* seq) " ) . n) by VALUED_1: 10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    registration

      let Z be set;

      let f be one-to-one Function;

      cluster (f | Z) -> one-to-one;

      coherence by FUNCT_1: 52;

    end

    theorem :: RFUNCT_2:17

    for h be one-to-one Function holds ((h | X) " ) = ((h " ) | (h .: X))

    proof

      let h be one-to-one Function;

      reconsider hX = (h | X) as one-to-one Function;

      now

        let r be object;

        thus r in ( dom ((h | X) " )) implies r in ( dom ((h " ) | (h .: X)))

        proof

          assume r in ( dom ((h | X) " ));

          then r in ( rng hX) by FUNCT_1: 33;

          then

          consider g be object such that

           A1: g in ( dom (h | X)) and

           A2: ((h | X) . g) = r by FUNCT_1:def 3;



           A3: (h . g) = r by A1, A2, FUNCT_1: 47;



           A4: g in (( dom h) /\ X) by A1, RELAT_1: 61;

          then g in ( dom h) by XBOOLE_0:def 4;

          then r in ( rng h) by A3, FUNCT_1:def 3;

          then

           A5: r in ( dom (h " )) by FUNCT_1: 33;

          g in ( dom h) & g in X by A4, XBOOLE_0:def 4;

          then r in (h .: X) by A3, FUNCT_1:def 6;

          then r in (( dom (h " )) /\ (h .: X)) by A5, XBOOLE_0:def 4;

          hence thesis by RELAT_1: 61;

        end;

        assume r in ( dom ((h " ) | (h .: X)));

        then r in (( dom (h " )) /\ (h .: X)) by RELAT_1: 61;

        then r in (h .: X) by XBOOLE_0:def 4;

        then

        consider t be object such that

         A6: t in ( dom h) and

         A7: t in X and

         A8: (h . t) = r by FUNCT_1:def 6;

        t in (( dom h) /\ X) by A6, A7, XBOOLE_0:def 4;

        then

         A9: t in ( dom (h | X)) by RELAT_1: 61;

        ((h | X) . t) = r by A7, A8, FUNCT_1: 49;

        then r in ( rng hX) by A9, FUNCT_1:def 3;

        hence r in ( dom ((h | X) " )) by FUNCT_1: 33;

      end;

      then

       A10: ( dom (hX " )) = ( dom ((h " ) | (h .: X))) by TARSKI: 2;

      now

        given r be object such that

         A11: r in ( dom ((h | X) " )) and

         A12: (((h | X) " ) . r) <> (((h " ) | (h .: X)) . r);

        r in (( dom (h " )) /\ (h .: X)) by A10, A11, RELAT_1: 61;

        then r in (h .: X) by XBOOLE_0:def 4;

        then

        consider t be object such that t in ( dom h) and t in X and

         A13: (h . t) = r by FUNCT_1:def 6;

        r in ( rng hX) by A11, FUNCT_1: 33;

        then

        consider g be object such that

         A14: g in ( dom (h | X)) and

         A15: ((h | X) . g) = r by FUNCT_1:def 3;



         A16: (h . g) = r by A14, A15, FUNCT_1: 47;

        g in (( dom h) /\ X) by A14, RELAT_1: 61;

        then

         A17: g in ( dom h) by XBOOLE_0:def 4;

        ((hX " ) . r) <> ((h " ) . r) by A10, A11, A12, FUNCT_1: 47;

        then g <> ((h " ) . (h . t)) by A14, A15, A13, FUNCT_1: 34;

        hence contradiction by A13, A17, A16, FUNCT_1: 34;

      end;

      hence thesis by A10;

    end;

    theorem :: RFUNCT_2:18



     Th18: for h be PartFunc of W, REAL holds ( rng h) is real-bounded & ( upper_bound ( rng h)) = ( lower_bound ( rng h)) implies h is constant

    proof

      let h be PartFunc of W, REAL ;

      assume

       A1: ( rng h) is real-bounded & ( upper_bound ( rng h)) = ( lower_bound ( rng h));

      assume not h is constant;

      then

      consider x1,x2 be object such that

       A2: x1 in ( dom h) & x2 in ( dom h) and

       A3: (h . x1) <> (h . x2);

      (h . x1) in ( rng h) & (h . x2) in ( rng h) by A2, FUNCT_1:def 3;

      hence contradiction by A1, A3, SEQ_4: 12;

    end;

    theorem :: RFUNCT_2:19

    for h be PartFunc of W, REAL holds (h .: Y) is real-bounded & ( upper_bound (h .: Y)) = ( lower_bound (h .: Y)) implies (h | Y) is constant

    proof

      let h be PartFunc of W, REAL ;

      ( rng (h | Y)) = (h .: Y) by RELAT_1: 115;

      hence thesis by Th18;

    end;

    reserve e1,e2 for ExtReal;

    reserve h,h1,h2 for PartFunc of REAL , REAL ;

    definition

      let h;

      :: original: increasing

      redefine

      :: RFUNCT_2:def1

      attr h is increasing means

      : Def1: for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) < (h . r2);

      compatibility ;

      :: original: decreasing

      redefine

      :: RFUNCT_2:def2

      attr h is decreasing means

      : Def2: for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r2) < (h . r1);

      compatibility ;

      :: original: non-decreasing

      redefine

      :: RFUNCT_2:def3

      attr h is non-decreasing means

      : Def3: for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) <= (h . r2);

      compatibility

      proof

        thus h is non-decreasing implies for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) <= (h . r2);

        assume

         A1: for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) <= (h . r2);

        let e1, e2 such that

         A2: e1 in ( dom h) & e2 in ( dom h);

        assume e1 <= e2;

        then e1 < e2 or e1 = e2 by XXREAL_0: 1;

        hence thesis by A1, A2;

      end;

      :: original: non-increasing

      redefine

      :: RFUNCT_2:def4

      attr h is non-increasing means for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r2) <= (h . r1);

      compatibility

      proof

        thus h is non-increasing implies for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) >= (h . r2);

        assume

         A3: for r1, r2 st r1 in ( dom h) & r2 in ( dom h) & r1 < r2 holds (h . r1) >= (h . r2);

        let e1, e2 such that

         A4: e1 in ( dom h) & e2 in ( dom h);

        assume e1 <= e2;

        then e1 < e2 or e1 = e2 by XXREAL_0: 1;

        hence thesis by A3, A4;

      end;

    end

    theorem :: RFUNCT_2:20



     Th20: (h | Y) is increasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) < (h . r2)

    proof

      thus (h | Y) is increasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) > (h . r1)

      proof

        assume

         A1: (h | Y) is increasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) and

         A3: r2 in (Y /\ ( dom h)) and

         A4: r1 < r2;



         A5: r2 in ( dom (h | Y)) by A3, RELAT_1: 61;

        then

         A6: ((h | Y) . r2) = (h . r2) by FUNCT_1: 47;



         A7: r1 in ( dom (h | Y)) by A2, RELAT_1: 61;

        then ((h | Y) . r1) = (h . r1) by FUNCT_1: 47;

        hence thesis by A1, A4, A7, A5, A6;

      end;

      assume

       A8: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) > (h . r1);

      let r1, r2;

      assume that

       A9: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A10: r1 < r2;



       A11: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A9, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A9, RELAT_1: 61;

      hence thesis by A8, A10, A11;

    end;

    theorem :: RFUNCT_2:21



     Th21: (h | Y) is decreasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) < (h . r1)

    proof

      thus (h | Y) is decreasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) < (h . r1)

      proof

        assume

         A1: (h | Y) is decreasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) and

         A3: r2 in (Y /\ ( dom h)) and

         A4: r1 < r2;



         A5: r2 in ( dom (h | Y)) by A3, RELAT_1: 61;

        then

         A6: ((h | Y) . r2) = (h . r2) by FUNCT_1: 47;



         A7: r1 in ( dom (h | Y)) by A2, RELAT_1: 61;

        then ((h | Y) . r1) = (h . r1) by FUNCT_1: 47;

        hence thesis by A1, A4, A7, A5, A6;

      end;

      assume

       A8: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) < (h . r1);

      let r1, r2;

      assume that

       A9: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A10: r1 < r2;



       A11: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A9, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A9, RELAT_1: 61;

      hence thesis by A8, A10, A11;

    end;

    theorem :: RFUNCT_2:22



     Th22: (h | Y) is non-decreasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) <= (h . r2)

    proof

      thus (h | Y) is non-decreasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) <= (h . r2)

      proof

        assume

         A1: (h | Y) is non-decreasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) and

         A3: r2 in (Y /\ ( dom h)) and

         A4: r1 < r2;



         A5: r2 in ( dom (h | Y)) by A3, RELAT_1: 61;

        then

         A6: ((h | Y) . r2) = (h . r2) by FUNCT_1: 47;



         A7: r1 in ( dom (h | Y)) by A2, RELAT_1: 61;

        then ((h | Y) . r1) = (h . r1) by FUNCT_1: 47;

        hence thesis by A1, A4, A7, A5, A6;

      end;

      assume

       A8: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r1) <= (h . r2);

      let r1, r2;

      assume that

       A9: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A10: r1 < r2;



       A11: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A9, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A9, RELAT_1: 61;

      hence thesis by A8, A10, A11;

    end;

    theorem :: RFUNCT_2:23



     Th23: (h | Y) is non-increasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) <= (h . r1)

    proof

      thus (h | Y) is non-increasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) <= (h . r1)

      proof

        assume

         A1: (h | Y) is non-increasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) and

         A3: r2 in (Y /\ ( dom h)) and

         A4: r1 < r2;



         A5: r2 in ( dom (h | Y)) by A3, RELAT_1: 61;

        then

         A6: ((h | Y) . r2) = (h . r2) by FUNCT_1: 47;



         A7: r1 in ( dom (h | Y)) by A2, RELAT_1: 61;

        then ((h | Y) . r1) = (h . r1) by FUNCT_1: 47;

        hence thesis by A1, A4, A7, A5, A6;

      end;

      assume

       A8: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 holds (h . r2) <= (h . r1);

      let r1, r2;

      assume that

       A9: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A10: r1 < r2;



       A11: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A9, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A9, RELAT_1: 61;

      hence thesis by A8, A10, A11;

    end;

    definition

      let h;

      :: RFUNCT_2:def5

      attr h is monotone means h is non-decreasing or h is non-increasing;

    end

    registration

      cluster non-decreasing -> monotone for PartFunc of REAL , REAL ;

      coherence ;

      cluster non-increasing -> monotone for PartFunc of REAL , REAL ;

      coherence ;

      cluster non monotone -> non non-decreasing non non-increasing for PartFunc of REAL , REAL ;

      coherence ;

    end

    theorem :: RFUNCT_2:24



     Th24: (h | Y) is non-decreasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r1) <= (h . r2)

    proof

      thus (h | Y) is non-decreasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r1) <= (h . r2)

      proof

        assume

         A1: (h | Y) is non-decreasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) and

         A3: r1 <= r2;

        now

          per cases by A3, XXREAL_0: 1;

            suppose r1 < r2;

            hence thesis by A1, A2, Th22;

          end;

            suppose r1 = r2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      assume

       A4: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r1) <= (h . r2);

      let r1, r2;

      assume that

       A5: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A6: r1 < r2;



       A7: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A5, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A5, RELAT_1: 61;

      hence thesis by A4, A6, A7;

    end;

    theorem :: RFUNCT_2:25



     Th25: (h | Y) is non-increasing iff for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r2) <= (h . r1)

    proof

      thus (h | Y) is non-increasing implies for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r2) <= (h . r1)

      proof

        assume

         A1: (h | Y) is non-increasing;

        let r1, r2 such that

         A2: r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) and

         A3: r1 <= r2;

        now

          per cases by A3, XXREAL_0: 1;

            suppose r1 < r2;

            hence thesis by A1, A2, Th23;

          end;

            suppose r1 = r2;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      assume

       A4: for r1, r2 st r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 <= r2 holds (h . r2) <= (h . r1);

      let r1, r2;

      assume that

       A5: r1 in ( dom (h | Y)) & r2 in ( dom (h | Y)) and

       A6: r1 < r2;



       A7: ((h | Y) . r1) = (h . r1) & ((h | Y) . r2) = (h . r2) by A5, FUNCT_1: 47;

      r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) by A5, RELAT_1: 61;

      hence thesis by A4, A6, A7;

    end;

    registration

      cluster non-decreasing non-increasing -> constant for PartFunc of REAL , REAL ;

      coherence

      proof

        let h be PartFunc of REAL , REAL ;

        assume

         A1: h is non-decreasing non-increasing;

        let r1,r2 be object;

        assume

         A2: r1 in ( dom h) & r2 in ( dom h);

        then

        reconsider r1, r2 as Real;

        r1 < r2 or r1 = r2 or r2 < r1 by XXREAL_0: 1;

        then (h . r1) <= (h . r2) & (h . r2) <= (h . r1) by A1, A2;

        hence thesis by XXREAL_0: 1;

      end;

    end

    registration

      cluster constant -> non-increasing non-decreasing for PartFunc of REAL , REAL ;

      coherence ;

    end

    registration

      cluster trivial for PartFunc of REAL , REAL ;

      existence

      proof

        reconsider f = {} as PartFunc of REAL , REAL by RELSET_1: 12;

        take f;

        thus thesis;

      end;

    end

    registration

      let h be increasing PartFunc of REAL , REAL , X be set;

      cluster (h | X) -> increasing;

      coherence

      proof

        now

          let r1, r2;

          assume

           A1: r1 in ( dom (h | X)) & r2 in ( dom (h | X));

          then

           A2: (h . r1) = ((h | X) . r1) & (h . r2) = ((h | X) . r2) by FUNCT_1: 47;

          assume

           A3: r1 < r2;

          r1 in ( dom h) & r2 in ( dom h) by A1, RELAT_1: 57;

          hence ((h | X) . r1) < ((h | X) . r2) by A2, A3, Def1;

        end;

        hence thesis;

      end;

    end

    registration

      let h be decreasing PartFunc of REAL , REAL , X be set;

      cluster (h | X) -> decreasing;

      coherence

      proof

        now

          let r1, r2;

          assume

           A1: r1 in ( dom (h | X)) & r2 in ( dom (h | X));

          then

           A2: (h . r1) = ((h | X) . r1) & (h . r2) = ((h | X) . r2) by FUNCT_1: 47;

          assume

           A3: r1 < r2;

          r1 in ( dom h) & r2 in ( dom h) by A1, RELAT_1: 57;

          hence ((h | X) . r1) > ((h | X) . r2) by A2, A3, Def2;

        end;

        hence thesis;

      end;

    end

    registration

      let h be non-decreasing PartFunc of REAL , REAL , X be set;

      cluster (h | X) -> non-decreasing;

      coherence

      proof

        now

          let r1, r2;

          assume

           A1: r1 in ( dom (h | X)) & r2 in ( dom (h | X));

          then

           A2: (h . r1) = ((h | X) . r1) & (h . r2) = ((h | X) . r2) by FUNCT_1: 47;

          assume

           A3: r1 < r2;

          r1 in ( dom h) & r2 in ( dom h) by A1, RELAT_1: 57;

          hence ((h | X) . r1) <= ((h | X) . r2) by A2, A3, Def3;

        end;

        hence thesis;

      end;

    end

    theorem :: RFUNCT_2:26

    Y misses ( dom h) implies (h | Y) is increasing & (h | Y) is decreasing & (h | Y) is non-decreasing & (h | Y) is non-increasing & (h | Y) is monotone

    proof

      assume

       A1: (Y /\ ( dom h)) = {} ;

      then for r1, r2 holds (r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 implies (h . r1) < (h . r2));

      hence (h | Y) is increasing by Th20;

      for r1, r2 holds (r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 implies (h . r2) < (h . r1)) by A1;

      hence (h | Y) is decreasing by Th21;

      for r1, r2 holds (r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 implies (h . r1) <= (h . r2)) by A1;

      hence (h | Y) is non-decreasing by Th22;



       A2: for r1, r2 holds (r1 in (Y /\ ( dom h)) & r2 in (Y /\ ( dom h)) & r1 < r2 implies (h . r2) <= (h . r1)) by A1;

      hence (h | Y) is non-increasing by Th23;

      thus thesis by A2, Th23;

    end;

    theorem :: RFUNCT_2:27

    (h | Y) is non-decreasing & (h | X) is non-increasing implies (h | (Y /\ X)) is constant

    proof

      assume

       A1: (h | Y) is non-decreasing & (h | X) is non-increasing;

      per cases ;

        suppose ((Y /\ X) /\ ( dom h)) = {} ;

        then (Y /\ X) misses ( dom h);

        hence thesis by PARTFUN2: 39;

      end;

        suppose

         A2: ((Y /\ X) /\ ( dom h)) <> {} ;

        set x = the Element of ((Y /\ X) /\ ( dom h));

        x in ( dom h) by A2, XBOOLE_0:def 4;

        then

        reconsider x as Element of REAL ;

        now

          reconsider r1 = (h . x) as Element of REAL by XREAL_0:def 1;

          take r1;

          now

            let p be Element of REAL ;

            assume

             A3: p in ((Y /\ X) /\ ( dom h));

            then

             A4: p in (Y /\ X) by XBOOLE_0:def 4;



             A5: p in ( dom h) by A3, XBOOLE_0:def 4;

            p in X by A4, XBOOLE_0:def 4;

            then

             A6: p in (X /\ ( dom h)) by A5, XBOOLE_0:def 4;



             A7: x in ( dom h) by A2, XBOOLE_0:def 4;



             A8: x in (Y /\ X) by A2, XBOOLE_0:def 4;

            then x in Y by XBOOLE_0:def 4;

            then

             A9: x in (Y /\ ( dom h)) by A7, XBOOLE_0:def 4;

            x in X by A8, XBOOLE_0:def 4;

            then

             A10: x in (X /\ ( dom h)) by A7, XBOOLE_0:def 4;

            p in Y by A4, XBOOLE_0:def 4;

            then

             A11: p in (Y /\ ( dom h)) by A5, XBOOLE_0:def 4;

            per cases ;

              suppose x <= p;

              then (h . x) <= (h . p) & (h . p) <= (h . x) by A1, A11, A6, A9, A10, Th24, Th25;

              hence (h . p) = (h . x) by XXREAL_0: 1;

            end;

              suppose p <= x;

              then (h . p) <= (h . x) & (h . x) <= (h . p) by A1, A11, A6, A9, A10, Th24, Th25;

              hence (h . p) = (h . x) by XXREAL_0: 1;

            end;

          end;

          hence for p be Element of REAL st p in ((Y /\ X) /\ ( dom h)) holds (h . p) = r1;

        end;

        hence thesis by PARTFUN2: 57;

      end;

    end;

    theorem :: RFUNCT_2:28

    X c= Y & (h | Y) is increasing implies (h | X) is increasing

    proof

      assume that

       A1: X c= Y and

       A2: (h | Y) is increasing;

      now



         A3: (X /\ ( dom h)) c= (Y /\ ( dom h)) by A1, XBOOLE_1: 26;

        let r1, r2;

        assume r1 in (X /\ ( dom h)) & r2 in (X /\ ( dom h)) & r1 < r2;

        hence (h . r1) < (h . r2) by A2, A3, Th20;

      end;

      hence thesis by Th20;

    end;

    theorem :: RFUNCT_2:29

    X c= Y & (h | Y) is decreasing implies (h | X) is decreasing

    proof

      assume that

       A1: X c= Y and

       A2: (h | Y) is decreasing;

      now



         A3: (X /\ ( dom h)) c= (Y /\ ( dom h)) by A1, XBOOLE_1: 26;

        let r1, r2;

        assume r1 in (X /\ ( dom h)) & r2 in (X /\ ( dom h)) & r1 < r2;

        hence (h . r1) > (h . r2) by A2, A3, Th21;

      end;

      hence thesis by Th21;

    end;

    theorem :: RFUNCT_2:30

    X c= Y & (h | Y) is non-decreasing implies (h | X) is non-decreasing

    proof

      assume that

       A1: X c= Y and

       A2: (h | Y) is non-decreasing;

      now



         A3: (X /\ ( dom h)) c= (Y /\ ( dom h)) by A1, XBOOLE_1: 26;

        let r1, r2;

        assume r1 in (X /\ ( dom h)) & r2 in (X /\ ( dom h)) & r1 < r2;

        hence (h . r1) <= (h . r2) by A2, A3, Th22;

      end;

      hence thesis by Th22;

    end;

    theorem :: RFUNCT_2:31

    X c= Y & (h | Y) is non-increasing implies (h | X) is non-increasing

    proof

      assume that

       A1: X c= Y and

       A2: (h | Y) is non-increasing;

      now



         A3: (X /\ ( dom h)) c= (Y /\ ( dom h)) by A1, XBOOLE_1: 26;

        let r1, r2;

        assume r1 in (X /\ ( dom h)) & r2 in (X /\ ( dom h)) & r1 < r2;

        hence (h . r1) >= (h . r2) by A2, A3, Th23;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:32



     Th32: ((h | Y) is increasing & 0 < r implies ((r (#) h) | Y) is increasing) & (r = 0 implies ((r (#) h) | Y) is constant) & ((h | Y) is increasing & r < 0 implies ((r (#) h) | Y) is decreasing)

    proof

      thus (h | Y) is increasing & 0 < r implies ((r (#) h) | Y) is increasing

      proof

        assume that

         A1: (h | Y) is increasing and

         A2: 0 < r;

        now

          let r1, r2;

          assume that

           A3: r1 in (Y /\ ( dom (r (#) h))) and

           A4: r2 in (Y /\ ( dom (r (#) h))) and

           A5: r1 < r2;



           A6: r2 in Y by A4, XBOOLE_0:def 4;



           A7: r2 in ( dom (r (#) h)) by A4, XBOOLE_0:def 4;

          then r2 in ( dom h) by VALUED_1:def 5;

          then

           A8: r2 in (Y /\ ( dom h)) by A6, XBOOLE_0:def 4;



           A9: r1 in Y by A3, XBOOLE_0:def 4;



           A10: r1 in ( dom (r (#) h)) by A3, XBOOLE_0:def 4;

          then r1 in ( dom h) by VALUED_1:def 5;

          then r1 in (Y /\ ( dom h)) by A9, XBOOLE_0:def 4;

          then (h . r1) < (h . r2) by A1, A5, A8, Th20;

          then (r * (h . r1)) < (r * (h . r2)) by A2, XREAL_1: 68;

          then ((r (#) h) . r1) < (r * (h . r2)) by A10, VALUED_1:def 5;

          hence ((r (#) h) . r1) < ((r (#) h) . r2) by A7, VALUED_1:def 5;

        end;

        hence thesis by Th20;

      end;

      thus r = 0 implies ((r (#) h) | Y) is constant

      proof

        assume

         A11: r = 0 ;



         A12: 0 in REAL by XREAL_0:def 1;

        now

          let r1 be Element of REAL ;

          assume r1 in (Y /\ ( dom (r (#) h)));

          then

           A13: r1 in ( dom (r (#) h)) by XBOOLE_0:def 4;

          (r * (h . r1)) = 0 by A11;

          hence ((r (#) h) . r1) = 0 by A13, VALUED_1:def 5;

        end;

        hence thesis by PARTFUN2: 57, A12;

      end;

      assume that

       A14: (h | Y) is increasing and

       A15: r < 0 ;

      now

        let r1, r2;

        assume that

         A16: r1 in (Y /\ ( dom (r (#) h))) and

         A17: r2 in (Y /\ ( dom (r (#) h))) and

         A18: r1 < r2;



         A19: r2 in Y by A17, XBOOLE_0:def 4;



         A20: r2 in ( dom (r (#) h)) by A17, XBOOLE_0:def 4;

        then r2 in ( dom h) by VALUED_1:def 5;

        then

         A21: r2 in (Y /\ ( dom h)) by A19, XBOOLE_0:def 4;



         A22: r1 in Y by A16, XBOOLE_0:def 4;



         A23: r1 in ( dom (r (#) h)) by A16, XBOOLE_0:def 4;

        then r1 in ( dom h) by VALUED_1:def 5;

        then r1 in (Y /\ ( dom h)) by A22, XBOOLE_0:def 4;

        then (h . r1) < (h . r2) by A14, A18, A21, Th20;

        then (r * (h . r2)) < (r * (h . r1)) by A15, XREAL_1: 69;

        then ((r (#) h) . r2) < (r * (h . r1)) by A20, VALUED_1:def 5;

        hence ((r (#) h) . r2) < ((r (#) h) . r1) by A23, VALUED_1:def 5;

      end;

      hence thesis by Th21;

    end;

    theorem :: RFUNCT_2:33

    ((h | Y) is decreasing & 0 < r implies ((r (#) h) | Y) is decreasing) & ((h | Y) is decreasing & r < 0 implies ((r (#) h) | Y) is increasing)

    proof

      thus (h | Y) is decreasing & 0 < r implies ((r (#) h) | Y) is decreasing

      proof

        assume that

         A1: (h | Y) is decreasing and

         A2: 0 < r;

        now

          let r1, r2;

          assume that

           A3: r1 in (Y /\ ( dom (r (#) h))) and

           A4: r2 in (Y /\ ( dom (r (#) h))) and

           A5: r1 < r2;



           A6: r2 in Y by A4, XBOOLE_0:def 4;



           A7: r2 in ( dom (r (#) h)) by A4, XBOOLE_0:def 4;

          then r2 in ( dom h) by VALUED_1:def 5;

          then

           A8: r2 in (Y /\ ( dom h)) by A6, XBOOLE_0:def 4;



           A9: r1 in Y by A3, XBOOLE_0:def 4;



           A10: r1 in ( dom (r (#) h)) by A3, XBOOLE_0:def 4;

          then r1 in ( dom h) by VALUED_1:def 5;

          then r1 in (Y /\ ( dom h)) by A9, XBOOLE_0:def 4;

          then (h . r2) < (h . r1) by A1, A5, A8, Th21;

          then (r * (h . r2)) < (r * (h . r1)) by A2, XREAL_1: 68;

          then ((r (#) h) . r2) < (r * (h . r1)) by A7, VALUED_1:def 5;

          hence ((r (#) h) . r2) < ((r (#) h) . r1) by A10, VALUED_1:def 5;

        end;

        hence thesis by Th21;

      end;

      assume that

       A11: (h | Y) is decreasing and

       A12: r < 0 ;

      now

        let r1, r2;

        assume that

         A13: r1 in (Y /\ ( dom (r (#) h))) and

         A14: r2 in (Y /\ ( dom (r (#) h))) and

         A15: r1 < r2;



         A16: r2 in Y by A14, XBOOLE_0:def 4;



         A17: r2 in ( dom (r (#) h)) by A14, XBOOLE_0:def 4;

        then r2 in ( dom h) by VALUED_1:def 5;

        then

         A18: r2 in (Y /\ ( dom h)) by A16, XBOOLE_0:def 4;



         A19: r1 in Y by A13, XBOOLE_0:def 4;



         A20: r1 in ( dom (r (#) h)) by A13, XBOOLE_0:def 4;

        then r1 in ( dom h) by VALUED_1:def 5;

        then r1 in (Y /\ ( dom h)) by A19, XBOOLE_0:def 4;

        then (h . r2) < (h . r1) by A11, A15, A18, Th21;

        then (r * (h . r1)) < (r * (h . r2)) by A12, XREAL_1: 69;

        then ((r (#) h) . r1) < (r * (h . r2)) by A20, VALUED_1:def 5;

        hence ((r (#) h) . r1) < ((r (#) h) . r2) by A17, VALUED_1:def 5;

      end;

      hence thesis by Th20;

    end;

    theorem :: RFUNCT_2:34



     Th34: ((h | Y) is non-decreasing & 0 <= r implies ((r (#) h) | Y) is non-decreasing) & ((h | Y) is non-decreasing & r <= 0 implies ((r (#) h) | Y) is non-increasing)

    proof

      thus (h | Y) is non-decreasing & 0 <= r implies ((r (#) h) | Y) is non-decreasing

      proof

        assume that

         A1: (h | Y) is non-decreasing and

         A2: 0 <= r;

        now

          let r1, r2;

          assume that

           A3: r1 in (Y /\ ( dom (r (#) h))) and

           A4: r2 in (Y /\ ( dom (r (#) h))) and

           A5: r1 < r2;



           A6: r2 in Y by A4, XBOOLE_0:def 4;



           A7: r2 in ( dom (r (#) h)) by A4, XBOOLE_0:def 4;

          then r2 in ( dom h) by VALUED_1:def 5;

          then

           A8: r2 in (Y /\ ( dom h)) by A6, XBOOLE_0:def 4;



           A9: r1 in Y by A3, XBOOLE_0:def 4;



           A10: r1 in ( dom (r (#) h)) by A3, XBOOLE_0:def 4;

          then r1 in ( dom h) by VALUED_1:def 5;

          then r1 in (Y /\ ( dom h)) by A9, XBOOLE_0:def 4;

          then (h . r1) <= (h . r2) by A1, A5, A8, Th22;

          then (r * (h . r1)) <= ((h . r2) * r) by A2, XREAL_1: 64;

          then ((r (#) h) . r1) <= (r * (h . r2)) by A10, VALUED_1:def 5;

          hence ((r (#) h) . r1) <= ((r (#) h) . r2) by A7, VALUED_1:def 5;

        end;

        hence thesis by Th22;

      end;

      assume that

       A11: (h | Y) is non-decreasing and

       A12: r <= 0 ;

      now

        let r1, r2;

        assume that

         A13: r1 in (Y /\ ( dom (r (#) h))) and

         A14: r2 in (Y /\ ( dom (r (#) h))) and

         A15: r1 < r2;



         A16: r2 in Y by A14, XBOOLE_0:def 4;



         A17: r2 in ( dom (r (#) h)) by A14, XBOOLE_0:def 4;

        then r2 in ( dom h) by VALUED_1:def 5;

        then

         A18: r2 in (Y /\ ( dom h)) by A16, XBOOLE_0:def 4;



         A19: r1 in Y by A13, XBOOLE_0:def 4;



         A20: r1 in ( dom (r (#) h)) by A13, XBOOLE_0:def 4;

        then r1 in ( dom h) by VALUED_1:def 5;

        then r1 in (Y /\ ( dom h)) by A19, XBOOLE_0:def 4;

        then (h . r1) <= (h . r2) by A11, A15, A18, Th22;

        then (r * (h . r2)) <= (r * (h . r1)) by A12, XREAL_1: 65;

        then ((r (#) h) . r2) <= (r * (h . r1)) by A17, VALUED_1:def 5;

        hence ((r (#) h) . r2) <= ((r (#) h) . r1) by A20, VALUED_1:def 5;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:35

    ((h | Y) is non-increasing & 0 <= r implies ((r (#) h) | Y) is non-increasing) & ((h | Y) is non-increasing & r <= 0 implies ((r (#) h) | Y) is non-decreasing)

    proof

      thus (h | Y) is non-increasing & 0 <= r implies ((r (#) h) | Y) is non-increasing

      proof

        assume that

         A1: (h | Y) is non-increasing and

         A2: 0 <= r;

        now

          let r1, r2;

          assume that

           A3: r1 in (Y /\ ( dom (r (#) h))) and

           A4: r2 in (Y /\ ( dom (r (#) h))) and

           A5: r1 < r2;



           A6: r2 in Y by A4, XBOOLE_0:def 4;



           A7: r2 in ( dom (r (#) h)) by A4, XBOOLE_0:def 4;

          then r2 in ( dom h) by VALUED_1:def 5;

          then

           A8: r2 in (Y /\ ( dom h)) by A6, XBOOLE_0:def 4;



           A9: r1 in Y by A3, XBOOLE_0:def 4;



           A10: r1 in ( dom (r (#) h)) by A3, XBOOLE_0:def 4;

          then r1 in ( dom h) by VALUED_1:def 5;

          then r1 in (Y /\ ( dom h)) by A9, XBOOLE_0:def 4;

          then (h . r2) <= (h . r1) by A1, A5, A8, Th23;

          then (r * (h . r2)) <= ((h . r1) * r) by A2, XREAL_1: 64;

          then ((r (#) h) . r2) <= (r * (h . r1)) by A7, VALUED_1:def 5;

          hence ((r (#) h) . r2) <= ((r (#) h) . r1) by A10, VALUED_1:def 5;

        end;

        hence thesis by Th23;

      end;

      assume that

       A11: (h | Y) is non-increasing and

       A12: r <= 0 ;

      now

        let r1, r2;

        assume that

         A13: r1 in (Y /\ ( dom (r (#) h))) and

         A14: r2 in (Y /\ ( dom (r (#) h))) and

         A15: r1 < r2;



         A16: r2 in Y by A14, XBOOLE_0:def 4;



         A17: r2 in ( dom (r (#) h)) by A14, XBOOLE_0:def 4;

        then r2 in ( dom h) by VALUED_1:def 5;

        then

         A18: r2 in (Y /\ ( dom h)) by A16, XBOOLE_0:def 4;



         A19: r1 in Y by A13, XBOOLE_0:def 4;



         A20: r1 in ( dom (r (#) h)) by A13, XBOOLE_0:def 4;

        then r1 in ( dom h) by VALUED_1:def 5;

        then r1 in (Y /\ ( dom h)) by A19, XBOOLE_0:def 4;

        then (h . r2) <= (h . r1) by A11, A15, A18, Th23;

        then (r * (h . r1)) <= (r * (h . r2)) by A12, XREAL_1: 65;

        then ((r (#) h) . r1) <= (r * (h . r2)) by A20, VALUED_1:def 5;

        hence ((r (#) h) . r1) <= ((r (#) h) . r2) by A17, VALUED_1:def 5;

      end;

      hence thesis by Th22;

    end;

    theorem :: RFUNCT_2:36



     Th36: r in ((X /\ Y) /\ ( dom (h1 + h2))) implies r in (X /\ ( dom h1)) & r in (Y /\ ( dom h2))

    proof

      assume

       A1: r in ((X /\ Y) /\ ( dom (h1 + h2)));

      then r in ( dom (h1 + h2)) by XBOOLE_0:def 4;

      then r in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

      then

       A2: r in ( dom h1) & r in ( dom h2) by XBOOLE_0:def 4;

      r in (X /\ Y) by A1, XBOOLE_0:def 4;

      then r in X & r in Y by XBOOLE_0:def 4;

      hence thesis by A2, XBOOLE_0:def 4;

    end;

    theorem :: RFUNCT_2:37

    ((h1 | X) is increasing & (h2 | Y) is increasing implies ((h1 + h2) | (X /\ Y)) is increasing) & ((h1 | X) is decreasing & (h2 | Y) is decreasing implies ((h1 + h2) | (X /\ Y)) is decreasing) & ((h1 | X) is non-decreasing & (h2 | Y) is non-decreasing implies ((h1 + h2) | (X /\ Y)) is non-decreasing) & ((h1 | X) is non-increasing & (h2 | Y) is non-increasing implies ((h1 + h2) | (X /\ Y)) is non-increasing)

    proof

      thus (h1 | X) is increasing & (h2 | Y) is increasing implies ((h1 + h2) | (X /\ Y)) is increasing

      proof

        assume that

         A1: (h1 | X) is increasing and

         A2: (h2 | Y) is increasing;

        now

          let r1, r2;

          assume that

           A3: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A4: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A5: r1 < r2;

          r1 in (Y /\ ( dom h2)) & r2 in (Y /\ ( dom h2)) by A3, A4, Th36;

          then

           A6: (h2 . r1) < (h2 . r2) by A2, A5, Th20;



           A7: r1 in ( dom (h1 + h2)) by A3, XBOOLE_0:def 4;

          r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A3, A4, Th36;

          then (h1 . r1) < (h1 . r2) by A1, A5, Th20;

          then ((h1 . r1) + (h2 . r1)) < ((h1 . r2) + (h2 . r2)) by A6, XREAL_1: 8;

          then

           A8: ((h1 + h2) . r1) < ((h1 . r2) + (h2 . r2)) by A7, VALUED_1:def 1;

          r2 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

          hence ((h1 + h2) . r1) < ((h1 + h2) . r2) by A8, VALUED_1:def 1;

        end;

        hence thesis by Th20;

      end;

      thus (h1 | X) is decreasing & (h2 | Y) is decreasing implies ((h1 + h2) | (X /\ Y)) is decreasing

      proof

        assume that

         A9: (h1 | X) is decreasing and

         A10: (h2 | Y) is decreasing;

        now

          let r1, r2;

          assume that

           A11: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A12: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A13: r1 < r2;

          r1 in (Y /\ ( dom h2)) & r2 in (Y /\ ( dom h2)) by A11, A12, Th36;

          then

           A14: (h2 . r2) < (h2 . r1) by A10, A13, Th21;



           A15: r2 in ( dom (h1 + h2)) by A12, XBOOLE_0:def 4;

          r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A11, A12, Th36;

          then (h1 . r2) < (h1 . r1) by A9, A13, Th21;

          then ((h1 . r2) + (h2 . r2)) < ((h1 . r1) + (h2 . r1)) by A14, XREAL_1: 8;

          then

           A16: ((h1 + h2) . r2) < ((h1 . r1) + (h2 . r1)) by A15, VALUED_1:def 1;

          r1 in ( dom (h1 + h2)) by A11, XBOOLE_0:def 4;

          hence ((h1 + h2) . r2) < ((h1 + h2) . r1) by A16, VALUED_1:def 1;

        end;

        hence thesis by Th21;

      end;

      thus (h1 | X) is non-decreasing & (h2 | Y) is non-decreasing implies ((h1 + h2) | (X /\ Y)) is non-decreasing

      proof

        assume that

         A17: (h1 | X) is non-decreasing and

         A18: (h2 | Y) is non-decreasing;

        now

          let r1, r2;

          assume that

           A19: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A20: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A21: r1 < r2;

          r1 in (Y /\ ( dom h2)) & r2 in (Y /\ ( dom h2)) by A19, A20, Th36;

          then

           A22: (h2 . r1) <= (h2 . r2) by A18, A21, Th22;



           A23: r1 in ( dom (h1 + h2)) by A19, XBOOLE_0:def 4;

          r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A19, A20, Th36;

          then (h1 . r1) <= (h1 . r2) by A17, A21, Th22;

          then ((h1 . r1) + (h2 . r1)) <= ((h1 . r2) + (h2 . r2)) by A22, XREAL_1: 7;

          then

           A24: ((h1 + h2) . r1) <= ((h1 . r2) + (h2 . r2)) by A23, VALUED_1:def 1;

          r2 in ( dom (h1 + h2)) by A20, XBOOLE_0:def 4;

          hence ((h1 + h2) . r1) <= ((h1 + h2) . r2) by A24, VALUED_1:def 1;

        end;

        hence thesis by Th22;

      end;

      assume that

       A25: (h1 | X) is non-increasing and

       A26: (h2 | Y) is non-increasing;

      now

        let r1, r2;

        assume that

         A27: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A28: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A29: r1 < r2;

        r1 in (Y /\ ( dom h2)) & r2 in (Y /\ ( dom h2)) by A27, A28, Th36;

        then

         A30: (h2 . r2) <= (h2 . r1) by A26, A29, Th23;



         A31: r2 in ( dom (h1 + h2)) by A28, XBOOLE_0:def 4;

        r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A27, A28, Th36;

        then (h1 . r2) <= (h1 . r1) by A25, A29, Th23;

        then ((h1 . r2) + (h2 . r2)) <= ((h1 . r1) + (h2 . r1)) by A30, XREAL_1: 7;

        then

         A32: ((h1 + h2) . r2) <= ((h1 . r1) + (h2 . r1)) by A31, VALUED_1:def 1;

        r1 in ( dom (h1 + h2)) by A27, XBOOLE_0:def 4;

        hence ((h1 + h2) . r2) <= ((h1 + h2) . r1) by A32, VALUED_1:def 1;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:38

    ((h1 | X) is increasing & (h2 | Y) is constant implies ((h1 + h2) | (X /\ Y)) is increasing) & ((h1 | X) is decreasing & (h2 | Y) is constant implies ((h1 + h2) | (X /\ Y)) is decreasing)

    proof

      thus (h1 | X) is increasing & (h2 | Y) is constant implies ((h1 + h2) | (X /\ Y)) is increasing

      proof

        assume that

         A1: (h1 | X) is increasing and

         A2: (h2 | Y) is constant;

        consider r be Element of REAL such that

         A3: for p be Element of REAL st p in (Y /\ ( dom h2)) holds (h2 . p) = r by A2, PARTFUN2: 57;

        now

          let r1, r2;

          assume that

           A4: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A5: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

           A6: r1 < r2;

          r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A4, A5, Th36;

          then (h1 . r1) < (h1 . r2) by A1, A6, Th20;

          then

           A7: ((h1 . r1) + r) < ((h1 . r2) + r) by XREAL_1: 6;

          r1 in (Y /\ ( dom h2)) by A4, Th36;

          then

           A8: ((h1 . r1) + (h2 . r1)) < ((h1 . r2) + r) by A3, A7;



           A9: r1 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

          r2 in (Y /\ ( dom h2)) by A5, Th36;

          then ((h1 . r1) + (h2 . r1)) < ((h1 . r2) + (h2 . r2)) by A3, A8;

          then

           A10: ((h1 + h2) . r1) < ((h1 . r2) + (h2 . r2)) by A9, VALUED_1:def 1;

          r2 in ( dom (h1 + h2)) by A5, XBOOLE_0:def 4;

          hence ((h1 + h2) . r1) < ((h1 + h2) . r2) by A10, VALUED_1:def 1;

        end;

        hence thesis by Th20;

      end;

      assume that

       A11: (h1 | X) is decreasing and

       A12: (h2 | Y) is constant;

      consider r be Element of REAL such that

       A13: for p be Element of REAL st p in (Y /\ ( dom h2)) holds (h2 . p) = r by A12, PARTFUN2: 57;

      now

        let r1, r2;

        assume that

         A14: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A15: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A16: r1 < r2;

        r1 in (X /\ ( dom h1)) & r2 in (X /\ ( dom h1)) by A14, A15, Th36;

        then (h1 . r2) < (h1 . r1) by A11, A16, Th21;

        then

         A17: ((h1 . r2) + r) < ((h1 . r1) + r) by XREAL_1: 6;

        r2 in (Y /\ ( dom h2)) by A15, Th36;

        then

         A18: ((h1 . r2) + (h2 . r2)) < ((h1 . r1) + r) by A13, A17;



         A19: r2 in ( dom (h1 + h2)) by A15, XBOOLE_0:def 4;

        r1 in (Y /\ ( dom h2)) by A14, Th36;

        then ((h1 . r2) + (h2 . r2)) < ((h1 . r1) + (h2 . r1)) by A13, A18;

        then

         A20: ((h1 + h2) . r2) < ((h1 . r1) + (h2 . r1)) by A19, VALUED_1:def 1;

        r1 in ( dom (h1 + h2)) by A14, XBOOLE_0:def 4;

        hence ((h1 + h2) . r2) < ((h1 + h2) . r1) by A20, VALUED_1:def 1;

      end;

      hence thesis by Th21;

    end;

    theorem :: RFUNCT_2:39

    (h1 | X) is increasing & (h2 | Y) is non-decreasing implies ((h1 + h2) | (X /\ Y)) is increasing

    proof

      assume that

       A1: (h1 | X) is increasing and

       A2: (h2 | Y) is non-decreasing;

      now

        let r1, r2;

        assume that

         A3: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A4: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A5: r1 < r2;



         A6: r2 in (X /\ Y) by A4, XBOOLE_0:def 4;

        then

         A7: r2 in Y by XBOOLE_0:def 4;



         A8: r2 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

        then

         A9: r2 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r2 in ( dom h2) by XBOOLE_0:def 4;

        then

         A10: r2 in (Y /\ ( dom h2)) by A7, XBOOLE_0:def 4;



         A11: r1 in (X /\ Y) by A3, XBOOLE_0:def 4;

        then

         A12: r1 in Y by XBOOLE_0:def 4;



         A13: r1 in ( dom (h1 + h2)) by A3, XBOOLE_0:def 4;

        then

         A14: r1 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r1 in ( dom h2) by XBOOLE_0:def 4;

        then r1 in (Y /\ ( dom h2)) by A12, XBOOLE_0:def 4;

        then

         A15: (h2 . r1) <= (h2 . r2) by A2, A5, A10, Th22;



         A16: r2 in X by A6, XBOOLE_0:def 4;



         A17: r1 in X by A11, XBOOLE_0:def 4;

        r2 in ( dom h1) by A9, XBOOLE_0:def 4;

        then

         A18: r2 in (X /\ ( dom h1)) by A16, XBOOLE_0:def 4;

        r1 in ( dom h1) by A14, XBOOLE_0:def 4;

        then r1 in (X /\ ( dom h1)) by A17, XBOOLE_0:def 4;

        then (h1 . r1) < (h1 . r2) by A1, A5, A18, Th20;

        then ((h1 . r1) + (h2 . r1)) < ((h1 . r2) + (h2 . r2)) by A15, XREAL_1: 8;

        then ((h1 + h2) . r1) < ((h1 . r2) + (h2 . r2)) by A13, VALUED_1:def 1;

        hence ((h1 + h2) . r1) < ((h1 + h2) . r2) by A8, VALUED_1:def 1;

      end;

      hence thesis by Th20;

    end;

    theorem :: RFUNCT_2:40

    (h1 | X) is non-increasing & (h2 | Y) is constant implies ((h1 + h2) | (X /\ Y)) is non-increasing

    proof

      assume that

       A1: (h1 | X) is non-increasing and

       A2: (h2 | Y) is constant;

      now

        let r1, r2;

        assume that

         A3: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A4: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A5: r1 < r2;



         A6: r2 in (X /\ Y) by A4, XBOOLE_0:def 4;

        then

         A7: r2 in X by XBOOLE_0:def 4;



         A8: r2 in Y by A6, XBOOLE_0:def 4;



         A9: r2 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

        then

         A10: r2 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r2 in ( dom h2) by XBOOLE_0:def 4;

        then

         A11: r2 in (Y /\ ( dom h2)) by A8, XBOOLE_0:def 4;

        r2 in ( dom h1) by A10, XBOOLE_0:def 4;

        then

         A12: r2 in (X /\ ( dom h1)) by A7, XBOOLE_0:def 4;



         A13: r1 in (X /\ Y) by A3, XBOOLE_0:def 4;

        then

         A14: r1 in X by XBOOLE_0:def 4;



         A15: r1 in Y by A13, XBOOLE_0:def 4;



         A16: r1 in ( dom (h1 + h2)) by A3, XBOOLE_0:def 4;

        then

         A17: r1 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r1 in ( dom h2) by XBOOLE_0:def 4;

        then r1 in (Y /\ ( dom h2)) by A15, XBOOLE_0:def 4;

        then

         A18: (h2 . r2) = (h2 . r1) by A2, A11, PARTFUN2: 58;

        r1 in ( dom h1) by A17, XBOOLE_0:def 4;

        then r1 in (X /\ ( dom h1)) by A14, XBOOLE_0:def 4;

        then (h1 . r2) <= (h1 . r1) by A1, A5, A12, Th23;

        then ((h1 . r2) + (h2 . r2)) <= ((h1 . r1) + (h2 . r1)) by A18, XREAL_1: 6;

        then ((h1 + h2) . r2) <= ((h1 . r1) + (h2 . r1)) by A9, VALUED_1:def 1;

        hence ((h1 + h2) . r2) <= ((h1 + h2) . r1) by A16, VALUED_1:def 1;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:41

    (h1 | X) is decreasing & (h2 | Y) is non-increasing implies ((h1 + h2) | (X /\ Y)) is decreasing

    proof

      assume that

       A1: (h1 | X) is decreasing and

       A2: (h2 | Y) is non-increasing;

      now

        let r1, r2;

        assume that

         A3: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A4: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A5: r1 < r2;



         A6: r2 in (X /\ Y) by A4, XBOOLE_0:def 4;

        then

         A7: r2 in Y by XBOOLE_0:def 4;



         A8: r2 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

        then

         A9: r2 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r2 in ( dom h2) by XBOOLE_0:def 4;

        then

         A10: r2 in (Y /\ ( dom h2)) by A7, XBOOLE_0:def 4;



         A11: r1 in (X /\ Y) by A3, XBOOLE_0:def 4;

        then

         A12: r1 in Y by XBOOLE_0:def 4;



         A13: r1 in ( dom (h1 + h2)) by A3, XBOOLE_0:def 4;

        then

         A14: r1 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r1 in ( dom h2) by XBOOLE_0:def 4;

        then r1 in (Y /\ ( dom h2)) by A12, XBOOLE_0:def 4;

        then

         A15: (h2 . r2) <= (h2 . r1) by A2, A5, A10, Th23;



         A16: r2 in X by A6, XBOOLE_0:def 4;



         A17: r1 in X by A11, XBOOLE_0:def 4;

        r2 in ( dom h1) by A9, XBOOLE_0:def 4;

        then

         A18: r2 in (X /\ ( dom h1)) by A16, XBOOLE_0:def 4;

        r1 in ( dom h1) by A14, XBOOLE_0:def 4;

        then r1 in (X /\ ( dom h1)) by A17, XBOOLE_0:def 4;

        then (h1 . r2) < (h1 . r1) by A1, A5, A18, Th21;

        then ((h1 . r2) + (h2 . r2)) < ((h1 . r1) + (h2 . r1)) by A15, XREAL_1: 8;

        then ((h1 + h2) . r2) < ((h1 . r1) + (h2 . r1)) by A8, VALUED_1:def 1;

        hence ((h1 + h2) . r2) < ((h1 + h2) . r1) by A13, VALUED_1:def 1;

      end;

      hence thesis by Th21;

    end;

    theorem :: RFUNCT_2:42

    (h1 | X) is non-decreasing & (h2 | Y) is constant implies ((h1 + h2) | (X /\ Y)) is non-decreasing

    proof

      assume that

       A1: (h1 | X) is non-decreasing and

       A2: (h2 | Y) is constant;

      now

        let r1, r2;

        assume that

         A3: r1 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A4: r2 in ((X /\ Y) /\ ( dom (h1 + h2))) and

         A5: r1 < r2;



         A6: r2 in (X /\ Y) by A4, XBOOLE_0:def 4;

        then

         A7: r2 in X by XBOOLE_0:def 4;



         A8: r2 in Y by A6, XBOOLE_0:def 4;



         A9: r2 in ( dom (h1 + h2)) by A4, XBOOLE_0:def 4;

        then

         A10: r2 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r2 in ( dom h2) by XBOOLE_0:def 4;

        then

         A11: r2 in (Y /\ ( dom h2)) by A8, XBOOLE_0:def 4;

        r2 in ( dom h1) by A10, XBOOLE_0:def 4;

        then

         A12: r2 in (X /\ ( dom h1)) by A7, XBOOLE_0:def 4;



         A13: r1 in (X /\ Y) by A3, XBOOLE_0:def 4;

        then

         A14: r1 in X by XBOOLE_0:def 4;



         A15: r1 in Y by A13, XBOOLE_0:def 4;



         A16: r1 in ( dom (h1 + h2)) by A3, XBOOLE_0:def 4;

        then

         A17: r1 in (( dom h1) /\ ( dom h2)) by VALUED_1:def 1;

        then r1 in ( dom h2) by XBOOLE_0:def 4;

        then r1 in (Y /\ ( dom h2)) by A15, XBOOLE_0:def 4;

        then

         A18: (h2 . r2) = (h2 . r1) by A2, A11, PARTFUN2: 58;

        r1 in ( dom h1) by A17, XBOOLE_0:def 4;

        then r1 in (X /\ ( dom h1)) by A14, XBOOLE_0:def 4;

        then (h1 . r1) <= (h1 . r2) by A1, A5, A12, Th22;

        then ((h1 . r1) + (h2 . r1)) <= ((h1 . r2) + (h2 . r2)) by A18, XREAL_1: 6;

        then ((h1 + h2) . r1) <= ((h1 . r2) + (h2 . r2)) by A16, VALUED_1:def 1;

        hence ((h1 + h2) . r1) <= ((h1 + h2) . r2) by A9, VALUED_1:def 1;

      end;

      hence thesis by Th22;

    end;

    theorem :: RFUNCT_2:43

    (h | {x}) is non-increasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( {x} /\ ( dom h)) and

         A2: r2 in ( {x} /\ ( dom h)) and r1 < r2;

        r1 in {x} by A1, XBOOLE_0:def 4;

        then

         A3: r1 = x by TARSKI:def 1;

        r2 in {x} by A2, XBOOLE_0:def 4;

        hence (h . r1) >= (h . r2) by A3, TARSKI:def 1;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:44

    (h | {x}) is decreasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( {x} /\ ( dom h)) and

         A2: r2 in ( {x} /\ ( dom h)) and

         A3: r1 < r2;

        r1 in {x} by A1, XBOOLE_0:def 4;

        then

         A4: r1 = x by TARSKI:def 1;

        r2 in {x} by A2, XBOOLE_0:def 4;

        hence (h . r1) > (h . r2) by A3, A4, TARSKI:def 1;

      end;

      hence thesis by Th21;

    end;

    theorem :: RFUNCT_2:45

    (h | {x}) is non-decreasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( {x} /\ ( dom h)) and

         A2: r2 in ( {x} /\ ( dom h)) and r1 < r2;

        r1 in {x} by A1, XBOOLE_0:def 4;

        then

         A3: r1 = x by TARSKI:def 1;

        r2 in {x} by A2, XBOOLE_0:def 4;

        hence (h . r1) <= (h . r2) by A3, TARSKI:def 1;

      end;

      hence thesis by Th22;

    end;

    theorem :: RFUNCT_2:46

    (h | {x}) is non-increasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in ( {x} /\ ( dom h)) and

         A2: r2 in ( {x} /\ ( dom h)) and r1 < r2;

        r1 in {x} by A1, XBOOLE_0:def 4;

        then

         A3: r1 = x by TARSKI:def 1;

        r2 in {x} by A2, XBOOLE_0:def 4;

        hence (h . r2) <= (h . r1) by A3, TARSKI:def 1;

      end;

      hence thesis by Th23;

    end;

    theorem :: RFUNCT_2:47

    (( id R) | R) is increasing

    proof

      now

        let r1, r2;

        assume that

         A1: r1 in (R /\ ( dom ( id R))) and

         A2: r2 in (R /\ ( dom ( id R))) and

         A3: r1 < r2;

        r1 in R by A1, XBOOLE_0:def 4;

        then

         A4: (( id R) . r1) = r1 by FUNCT_1: 18;

        r2 in R by A2, XBOOLE_0:def 4;

        hence (( id R) . r1) < (( id R) . r2) by A3, A4, FUNCT_1: 18;

      end;

      hence thesis by Th20;

    end;

    theorem :: RFUNCT_2:48

    (h | X) is increasing implies (( - h) | X) is decreasing by Th32;

    theorem :: RFUNCT_2:49

    (h | X) is non-decreasing implies (( - h) | X) is non-increasing by Th34;

    theorem :: RFUNCT_2:50

    ((h | [.p, g.]) is increasing or (h | [.p, g.]) is decreasing) implies (h | [.p, g.]) is one-to-one

    proof

      assume

       A1: (h | [.p, g.]) is increasing or (h | [.p, g.]) is decreasing;

      now

        per cases by A1;

          suppose

           A2: (h | [.p, g.]) is increasing;

          now

            let p1,p2 be Element of REAL ;

            assume that

             A3: p1 in ( dom (h | [.p, g.])) and

             A4: p2 in ( dom (h | [.p, g.])) and

             A5: ((h | [.p, g.]) . p1) = ((h | [.p, g.]) . p2);



             A6: p1 in ( [.p, g.] /\ ( dom h)) & p2 in ( [.p, g.] /\ ( dom h)) by A3, A4, RELAT_1: 61;



             A7: (h . p1) = ((h | [.p, g.]) . p2) by A3, A5, FUNCT_1: 47

            .= (h . p2) by A4, FUNCT_1: 47;

            thus p1 = p2

            proof

              assume

               A8: p1 <> p2;

              now

                per cases by A8, XXREAL_0: 1;

                  suppose p1 < p2;

                  hence contradiction by A2, A7, A6, Th20;

                end;

                  suppose p2 < p1;

                  hence contradiction by A2, A7, A6, Th20;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence thesis;

        end;

          suppose

           A9: (h | [.p, g.]) is decreasing;

          now

            let p1,p2 be Element of REAL ;

            assume that

             A10: p1 in ( dom (h | [.p, g.])) and

             A11: p2 in ( dom (h | [.p, g.])) and

             A12: ((h | [.p, g.]) . p1) = ((h | [.p, g.]) . p2);



             A13: p1 in ( [.p, g.] /\ ( dom h)) & p2 in ( [.p, g.] /\ ( dom h)) by A10, A11, RELAT_1: 61;



             A14: (h . p1) = ((h | [.p, g.]) . p2) by A10, A12, FUNCT_1: 47

            .= (h . p2) by A11, FUNCT_1: 47;

            thus p1 = p2

            proof

              assume

               A15: p1 <> p2;

              now

                per cases by A15, XXREAL_0: 1;

                  suppose p1 < p2;

                  hence contradiction by A9, A14, A13, Th21;

                end;

                  suppose p2 < p1;

                  hence contradiction by A9, A14, A13, Th21;

                end;

              end;

              hence contradiction;

            end;

          end;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RFUNCT_2:51

    for h be one-to-one PartFunc of REAL , REAL st (h | [.p, g.]) is increasing holds (((h | [.p, g.]) " ) | (h .: [.p, g.])) is increasing

    proof

      let h be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (h | [.p, g.]) is increasing and

       A2: not (((h | [.p, g.]) " ) | (h .: [.p, g.])) is increasing;

      consider y1,y2 be Real such that

       A3: y1 in ((h .: [.p, g.]) /\ ( dom ((h | [.p, g.]) " ))) and

       A4: y2 in ((h .: [.p, g.]) /\ ( dom ((h | [.p, g.]) " ))) and

       A5: y1 < y2 and

       A6: (((h | [.p, g.]) " ) . y1) >= (((h | [.p, g.]) " ) . y2) by A2, Th20;

      reconsider yy1 = y1, yy2 = y2 as Real;

      y1 in (h .: [.p, g.]) by A3, XBOOLE_0:def 4;

      then

       A7: yy1 in ( rng (h | [.p, g.])) by RELAT_1: 115;

      y2 in (h .: [.p, g.]) by A4, XBOOLE_0:def 4;

      then

       A8: yy2 in ( rng (h | [.p, g.])) by RELAT_1: 115;



       A9: ((h | [.p, g.]) | [.p, g.]) is increasing by A1;

      per cases ;

        suppose (((h | [.p, g.]) " ) . y1) = (((h | [.p, g.]) " ) . y2);



        then y1 = ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y2)) by A7, FUNCT_1: 35

        .= y2 by A8, FUNCT_1: 35;

        hence contradiction by A5;

      end;

        suppose

         A10: (((h | [.p, g.]) " ) . y1) <> (((h | [.p, g.]) " ) . y2);



         A11: ( dom (h | [.p, g.])) = ( dom ((h | [.p, g.]) | [.p, g.])) by RELAT_1: 72

        .= ( [.p, g.] /\ ( dom (h | [.p, g.]))) by RELAT_1: 61;

        (((h | [.p, g.]) " ) . yy2) in REAL & (((h | [.p, g.]) " ) . yy1) in REAL by XREAL_0:def 1;

        then

         A12: (((h | [.p, g.]) " ) . yy2) in ( dom (h | [.p, g.])) & (((h | [.p, g.]) " ) . yy1) in ( dom (h | [.p, g.])) by A7, A8, PARTFUN2: 60;

        (((h | [.p, g.]) " ) . y2) < (((h | [.p, g.]) " ) . y1) by A6, A10, XXREAL_0: 1;

        then ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y2)) < ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y1)) by A9, A12, A11, Th20;

        then y2 < ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y1)) by A8, FUNCT_1: 35;

        hence contradiction by A5, A7, FUNCT_1: 35;

      end;

    end;

    theorem :: RFUNCT_2:52

    for h be one-to-one PartFunc of REAL , REAL st (h | [.p, g.]) is decreasing holds (((h | [.p, g.]) " ) | (h .: [.p, g.])) is decreasing

    proof

      let h be one-to-one PartFunc of REAL , REAL ;

      assume that

       A1: (h | [.p, g.]) is decreasing and

       A2: not (((h | [.p, g.]) " ) | (h .: [.p, g.])) is decreasing;

      consider y1,y2 be Real such that

       A3: y1 in ((h .: [.p, g.]) /\ ( dom ((h | [.p, g.]) " ))) and

       A4: y2 in ((h .: [.p, g.]) /\ ( dom ((h | [.p, g.]) " ))) and

       A5: y1 < y2 and

       A6: (((h | [.p, g.]) " ) . y2) >= (((h | [.p, g.]) " ) . y1) by A2, Th21;

      y1 in (h .: [.p, g.]) by A3, XBOOLE_0:def 4;

      then

       A7: y1 in ( rng (h | [.p, g.])) by RELAT_1: 115;

      y2 in (h .: [.p, g.]) by A4, XBOOLE_0:def 4;

      then

       A8: y2 in ( rng (h | [.p, g.])) by RELAT_1: 115;



       A9: ((h | [.p, g.]) | [.p, g.]) is decreasing by A1;

      now

        per cases ;

          suppose (((h | [.p, g.]) " ) . y1) = (((h | [.p, g.]) " ) . y2);



          then y1 = ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y2)) by A7, FUNCT_1: 35

          .= y2 by A8, FUNCT_1: 35;

          hence contradiction by A5;

        end;

          suppose

           A10: (((h | [.p, g.]) " ) . y1) <> (((h | [.p, g.]) " ) . y2);



           A11: ( dom (h | [.p, g.])) = ( dom ((h | [.p, g.]) | [.p, g.])) by RELAT_1: 72

          .= ( [.p, g.] /\ ( dom (h | [.p, g.]))) by RELAT_1: 61;

          (((h | [.p, g.]) " ) . y2) in REAL & (((h | [.p, g.]) " ) . y1) in REAL & y1 in REAL & y2 in REAL by XREAL_0:def 1;

          then

           A12: (((h | [.p, g.]) " ) . y2) in ( dom (h | [.p, g.])) & (((h | [.p, g.]) " ) . y1) in ( dom (h | [.p, g.])) by A7, A8, PARTFUN2: 60;

          (((h | [.p, g.]) " ) . y2) > (((h | [.p, g.]) " ) . y1) by A6, A10, XXREAL_0: 1;

          then ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y2)) < ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y1)) by A9, A12, A11, Th21;

          then y2 < ((h | [.p, g.]) . (((h | [.p, g.]) " ) . y1)) by A8, FUNCT_1: 35;

          hence contradiction by A5, A7, FUNCT_1: 35;

        end;

      end;

      hence contradiction;

    end;