let g be Function of I[01],R^1; :: thesis: for s1, s2 being Real st g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 holds
ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
let s1, s2 be Real; :: thesis: ( g is continuous & g . 0 <> g . 1 & s1 = g . 0 & s2 = g . 1 implies ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) )
assume that
A1: g is continuous and
A2: g . 0 <> g . 1 and
A3: ( s1 = g . 0 & s2 = g . 1 ) ; :: thesis: ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 )
now :: thesis: ( ( s1 < s2 & ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) ) or ( s2 < s1 & ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) ) )
per cases ( s1 < s2 or s2 < s1 ) by A2, A3, XXREAL_0:1;
case s1 < s2 ; :: thesis: ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 )
then ( s1 < (s1 + s2) / 2 & (s1 + s2) / 2 < s2 ) by XREAL_1:226;
hence ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th6, TOPMETR:20; :: thesis: verum
end;
case s2 < s1 ; :: thesis: ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 )
then ( s2 < (s1 + s2) / 2 & (s1 + s2) / 2 < s1 ) by XREAL_1:226;
hence ex rc being Real st
( g . rc = (s1 + s2) / 2 & 0 < rc & rc < 1 ) by A1, A3, Th7, TOPMETR:20; :: thesis: verum
end;
end;
end;
hence ex r1 being Real st
( 0 < r1 & r1 < 1 & g . r1 = (s1 + s2) / 2 ) ; :: thesis: verum