:: Average Value Theorems for Real Functions of One Variable :: by Jaros{\l}aw Kotowicz, Konrad Raczkowski and Pawe{\l} Sadowski :: :: Received June 18, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, ARYTM_3, XXREAL_1, TARSKI, RELAT_1, ORDINAL2, FUNCT_1, FDIFF_1, CARD_1, RCOMP_1, XXREAL_2, SEQ_4, XXREAL_0, XBOOLE_0, ARYTM_1, VALUED_0, SEQ_2, VALUED_1, FUNCT_2, FUNCOP_1, FUNCT_7, NAT_1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_1, FUNCT_2, NUMBERS, XREAL_0, XXREAL_0, XXREAL_2, XCMPLX_0, REAL_1, RELSET_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, SEQ_4, PARTFUN1, PARTFUN2, RCOMP_1, FCONT_1, FDIFF_1; constructors PARTFUN1, REAL_1, NAT_1, SEQ_2, SEQ_4, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, VALUED_1, XXREAL_2, COMPLEX1, RELSET_1, BINOP_2, COMSEQ_2; registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, RCOMP_1, FDIFF_1, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve y for set; reserve g,r,s,p,t,x,x0,x1,x2 for Real; reserve n,n1 for Nat; reserve s1,s2,s3 for Real_Sequence; reserve f,f1,f2 for PartFunc of REAL,REAL; theorem :: ROLLE:1 for p,g st p0) ex s st 0