let a, b be Real; :: thesis: for u being PartFunc of REAL,REAL st a < b & u is_differentiable_on ].a,b.[ & dom u = ['a,b'] & u is continuous & ( for t being Real st t in ].a,b.[ holds
(u `| ].a,b.[) . t = 0 ) holds
ex C being Real st
for t being Real st t in ['a,b'] holds
u . t = C
let u be PartFunc of REAL,REAL; :: thesis: ( a < b & u is_differentiable_on ].a,b.[ & dom u = ['a,b'] & u is continuous & ( for t being Real st t in ].a,b.[ holds
(u `| ].a,b.[) . t = 0 ) implies ex C being Real st
for t being Real st t in ['a,b'] holds
u . t = C )
assume A1: ( a < b & u is_differentiable_on ].a,b.[ & dom u = ['a,b'] & u is continuous & ( for t being Real st t in ].a,b.[ holds
(u `| ].a,b.[) . t = 0 ) ) ; :: thesis: ex C being Real st
for t being Real st t in ['a,b'] holds
u . t = C
for x being Real st x in ].a,b.[ holds
diff (u,x) = 0

proof

let t be Real; :: thesis: ( t in ].a,b.[ implies diff (u,t) = 0 )
assume A2: t in ].a,b.[ ; :: thesis: diff (u,t) = 0
hence diff (u,t) = (u `| ].a,b.[) . t by A1, FDIFF_1:def 7
.= 0 by A1, A2 ;
:: thesis: verum

end;

then A3: u | ].a,b.[ is constant by A1, ROLLE:7;
A4: dom (u | ].a,b.[) = ].a,b.[ by A1, RELAT_1:62;
set z = a + ((b - a) / 2);
A5: 0 < b - a by A1, XREAL_1:50;
then A6: 0 + a < a + ((b - a) / 2) by XREAL_1:8;
(b - a) / 2 < b - a by A5, XREAL_1:216;
then a + ((b - a) / 2) < (b - a) + a by XREAL_1:8;
then A7: a + ((b - a) / 2) in ].a,b.[ by A6;
take C = (u | ].a,b.[) . (a + ((b - a) / 2)); :: thesis: for t being Real st t in ['a,b'] holds
u . t = C

now :: thesis: for t being Real st t in ].a,b.[ holds
u . t = C

let t be Real; :: thesis: ( t in ].a,b.[ implies u . t = C )
assume A8: t in ].a,b.[ ; :: thesis: u . t = C
hence u . t = (u | ].a,b.[) . t by FUNCT_1:49
.= C by A3, A4, A7, A8, FUNCT_1:def 10 ;
:: thesis: verum

end;

hence for t being Real st t in ['a,b'] holds
u . t = C by A1, Th1; :: thesis: verum