let p, g be Real; :: thesis: for f being PartFunc of REAL ,REAL st p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous holds
for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let f be PartFunc of REAL ,REAL ; :: thesis: ( p <= g & [.p,g.] c= dom f & f | [.p,g.] is continuous implies for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume that
A1: p <= g and
A2: [.p,g.] c= dom f and
A3: f | [.p,g.] is continuous ; :: thesis: for r being Real st r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] holds
ex s being Real st
( s in [.p,g.] & r = f . s )
let r be Real; :: thesis: ( r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
assume A4: r in [.(f . p),(f . g).] \/ [.(f . g),(f . p).] ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
A5: [.p,g.] is compact by RCOMP_1:24;
A6: ( f . p < f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:57;
assume that
A7: f . p < f . g and
A8: for s being Real st s in [.p,g.] holds
r <> f . s ; :: thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = [.(f . p),(f . g).] \/ {} by A7, XXREAL_1:29
.= [.(f . p),(f . g).] ;
then r in { s where s is Real : ( f . p <= s & s <= f . g ) } by A4, RCOMP_1:def 1;
then A9: ex s being Real st
( s = r & f . p <= s & s <= f . g ) ;
p in { s where s is Real : ( p <= s & s <= g ) } by A1;
then p in [.p,g.] by RCOMP_1:def 1;
then A10: r <> f . p by A8;
reconsider f1 = f1 as PartFunc of REAL ,REAL ;
A11: dom f1 = [.p,g.] by FUNCOP_1:19;
then A12: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A13: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A14: (abs (f1 - f)) " {0 } = {}
proof
assume (abs (f1 - f)) " {0 } <> {} ; :: thesis: contradiction
then consider x2 being Real such that
A15: x2 in (abs (f1 - f)) " {0 } by SUBSET_1:10;
x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def 13;
then A16: x2 in dom (f1 - f) by VALUED_1:def 11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A17: x2 in [.p,g.] by A11, XBOOLE_0:def 4;
(abs (f1 - f)) . x2 in {0 } by A15, FUNCT_1:def 13;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;
then abs ((f1 - f) . x2) = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:7;
then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13;
then r - (f . x2) = 0 by A17, FUNCOP_1:13;
hence contradiction by A8, A17; :: thesis: verum
end;
A18: dom ((abs (f1 - f)) ^ ) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0 }) by RFUNCT_1:def 8
.= dom (f1 - f) by A14, VALUED_1:def 11
.= [.p,g.] /\ (dom f) by A11, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A11, FUNCOP_1:13;
then f1 | [.p,g.] is constant by PARTFUN2:76;
then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:19;
then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:22;
then ((abs (f1 - f)) ^ ) | [.p,g.] is continuous by A14, FCONT_1:23;
then ((abs (f1 - f)) ^ ) .: [.p,g.] is bounded by A5, A18, FCONT_1:30, RCOMP_1:28;
then consider M being real number such that
A19: for x1 being real number st x1 in ((abs (f1 - f)) ^ ) .: [.p,g.] holds
x1 <= M by SEQ_4:def 1;
0 + 0 < (abs M) + 1 by COMPLEX1:132, XREAL_1:10;
then 0 < ((abs M) + 1) " ;
then A20: 0 < 1 / ((abs M) + 1) by XCMPLX_1:217;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:24;
then consider s being Real such that
A21: 0 < s and
A22: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A20, Th1;
A23: now
let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) )
assume A24: x1 in [.p,g.] ; :: thesis: 1 / ((abs M) + 1) < abs (r - (f . x1))
then ((abs (f1 - f)) ^ ) . x1 in ((abs (f1 - f)) ^ ) .: [.p,g.] by A18, FUNCT_1:def 12;
then ((abs (f1 - f)) ^ ) . x1 <= M by A19;
then ((abs (f1 - f)) . x1) " <= M by A18, A24, RFUNCT_1:def 8;
then A25: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A11, A24, XBOOLE_0:def 4;
then x1 in dom (f1 - f) by VALUED_1:12;
then (abs ((f1 . x1) - (f . x1))) " <= M by A25, VALUED_1:13;
then A26: (abs (r - (f . x1))) " <= M by A24, FUNCOP_1:13;
r - (f . x1) <> 0 by A8, A24;
then A27: 0 < abs (r - (f . x1)) by COMPLEX1:133;
M + 0 < (abs M) + 1 by ABSVALUE:11, XREAL_1:10;
then (abs (r - (f . x1))) " < (abs M) + 1 by A26, XXREAL_0:2;
then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) " ) by A27, XREAL_1:78;
hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:218; :: thesis: verum
end;
now
per cases ( p = g or p <> g ) ;
suppose p <> g ; :: thesis: contradiction
then p < g by A1, XXREAL_0:1;
then A28: 0 < g - p by XREAL_1:52;
then A29: 0 < (g - p) / s by A21, XREAL_1:141;
consider k being Element of NAT such that
A30: (g - p) / s < k by SEQ_4:10;
((g - p) / s) * s < s * k by A21, A30, XREAL_1:70;
then g - p < s * k by A21, XCMPLX_1:88;
then (g - p) / k < (s * k) / k by A30, A29, XREAL_1:76;
then (g - p) / k < (s * k) * (k " ) by XCMPLX_0:def 9;
then (g - p) / k < s * (k * (k " )) ;
then A31: (g - p) / k < s * 1 by A30, A29, XCMPLX_0:def 7;
deffunc H1( Element of NAT ) -> Element of REAL = p + (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A32: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch 1();
A33: 0 < (g - p) / k by A28, A30, A29, XREAL_1:141;
A34: now
let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) )
A35: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:91;
assume A36: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A33, XREAL_1:70;
then ((g - p) / k) * n < g - p by A30, A29, XCMPLX_1:88;
then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:8;
then A37: s1 . n < p + (g - p) by A32;
n + 1 <= k by A36, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A28, XREAL_1:66;
then ((g - p) / k) * (n + 1) <= g - p by A30, A29, XCMPLX_1:88;
then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:9;
then A38: s1 . (n + 1) <= p + (g - p) by A32;
p + 0 <= p + (((g - p) / k) * n) by A28, XREAL_1:9;
then p <= s1 . n by A32;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A37;
hence A39: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
p + 0 <= p + (((g - p) / k) * (n + 1)) by A28, XREAL_1:9;
then p <= s1 . (n + 1) by A32;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38;
hence A40: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1)
abs ((s1 . (n + 1)) - (s1 . n)) = abs ((p + (((g - p) / k) * (n + 1))) - (s1 . n)) by A32
.= abs ((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))) by A32
.= (g - p) / k by A28, ABSVALUE:def 1 ;
hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A22, A31, A39, A40, A35; :: thesis: verum
end;
defpred S1[ Nat] means r <= f . (s1 . $1);
A41: s1 . k = p + (((g - p) / k) * k) by A32
.= p + (g - p) by A30, A29, XCMPLX_1:88
.= g ;
then A42: ex n being Nat st S1[n] by A9;
consider l being Nat such that
A43: ( S1[l] & ( for m being Nat st S1[m] holds
l <= m ) ) from NAT_1:sch 5(A42);
s1 . 0 = p + (((g - p) / k) * 0 ) by A32
.= p ;
then l <> 0 by A9, A10, A43, XXREAL_0:1;
then consider l1 being Nat such that
A44: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 13;
A45: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A43, A44, XREAL_1:11;
l1 + 1 <= k by A9, A41, A43, A44;
then A46: l1 < k by NAT_1:13;
then A47: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A34;
f . (s1 . l1) < r
proof
assume r <= f . (s1 . l1) ; :: thesis: contradiction
then l <= l1 by A43;
then l + 0 < l by A44, XREAL_1:10;
hence contradiction ; :: thesis: verum
end;
then A48: 0 < r - (f . (s1 . l1)) by XREAL_1:52;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A43, A44, XREAL_1:11;
then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;
then A49: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A48, A45, ABSVALUE:def 1;
s1 . l1 in [.p,g.] by A34, A46;
hence contradiction by A23, A49, A47, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
A50: ( f . g < f . p implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:57;
assume that
A51: f . g < f . p and
A52: for s being Real st s in [.p,g.] holds
r <> f . s ; :: thesis: contradiction
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {} \/ [.(f . g),(f . p).] by A51, XXREAL_1:29
.= [.(f . g),(f . p).] ;
then r in { s where s is Real : ( f . g <= s & s <= f . p ) } by A4, RCOMP_1:def 1;
then A53: ex s being Real st
( s = r & f . g <= s & s <= f . p ) ;
g in { s where s is Real : ( p <= s & s <= g ) } by A1;
then g in [.p,g.] by RCOMP_1:def 1;
then A54: r <> f . g by A52;
reconsider f1 = f1 as PartFunc of REAL ,REAL ;
A55: dom f1 = [.p,g.] by FUNCOP_1:19;
then A56: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;
then A57: [.p,g.] c= dom (f1 - f) by VALUED_1:12;
A58: (abs (f1 - f)) " {0 } = {}
proof
assume (abs (f1 - f)) " {0 } <> {} ; :: thesis: contradiction
then consider x2 being Real such that
A59: x2 in (abs (f1 - f)) " {0 } by SUBSET_1:10;
x2 in dom (abs (f1 - f)) by A59, FUNCT_1:def 13;
then A60: x2 in dom (f1 - f) by VALUED_1:def 11;
then x2 in (dom f1) /\ (dom f) by VALUED_1:12;
then A61: x2 in [.p,g.] by A55, XBOOLE_0:def 4;
(abs (f1 - f)) . x2 in {0 } by A59, FUNCT_1:def 13;
then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;
then abs ((f1 - f) . x2) = 0 by VALUED_1:18;
then (f1 - f) . x2 = 0 by ABSVALUE:7;
then (f1 . x2) - (f . x2) = 0 by A60, VALUED_1:13;
then r - (f . x2) = 0 by A61, FUNCOP_1:13;
hence contradiction by A52, A61; :: thesis: verum
end;
A62: dom ((abs (f1 - f)) ^ ) = (dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0 }) by RFUNCT_1:def 8
.= dom (f1 - f) by A58, VALUED_1:def 11
.= [.p,g.] /\ (dom f) by A55, VALUED_1:12
.= [.p,g.] by A2, XBOOLE_1:28 ;
for x0 being Real st x0 in [.p,g.] /\ (dom f1) holds
f1 . x0 = r by A55, FUNCOP_1:13;
then f1 | [.p,g.] is constant by PARTFUN2:76;
then (f1 - f) | [.p,g.] is continuous by A3, A56, FCONT_1:19;
then (abs (f1 - f)) | [.p,g.] is continuous by A57, FCONT_1:22;
then ((abs (f1 - f)) ^ ) | [.p,g.] is continuous by A58, FCONT_1:23;
then ((abs (f1 - f)) ^ ) .: [.p,g.] is bounded by A5, A62, FCONT_1:30, RCOMP_1:28;
then consider M being real number such that
A63: for x1 being real number st x1 in ((abs (f1 - f)) ^ ) .: [.p,g.] holds
x1 <= M by SEQ_4:def 1;
0 + 0 < (abs M) + 1 by COMPLEX1:132, XREAL_1:10;
then 0 < ((abs M) + 1) " ;
then A64: 0 < 1 / ((abs M) + 1) by XCMPLX_1:217;
f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:24;
then consider s being Real such that
A65: 0 < s and
A66: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & abs (x1 - x2) < s holds
abs ((f . x1) - (f . x2)) < 1 / ((abs M) + 1) by A64, Th1;
A67: now
let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / ((abs M) + 1) < abs (r - (f . x1)) )
assume A68: x1 in [.p,g.] ; :: thesis: 1 / ((abs M) + 1) < abs (r - (f . x1))
then ((abs (f1 - f)) ^ ) . x1 in ((abs (f1 - f)) ^ ) .: [.p,g.] by A62, FUNCT_1:def 12;
then ((abs (f1 - f)) ^ ) . x1 <= M by A63;
then ((abs (f1 - f)) . x1) " <= M by A62, A68, RFUNCT_1:def 8;
then A69: (abs ((f1 - f) . x1)) " <= M by VALUED_1:18;
x1 in (dom f1) /\ (dom f) by A2, A55, A68, XBOOLE_0:def 4;
then x1 in dom (f1 - f) by VALUED_1:12;
then (abs ((f1 . x1) - (f . x1))) " <= M by A69, VALUED_1:13;
then A70: (abs (r - (f . x1))) " <= M by A68, FUNCOP_1:13;
r - (f . x1) <> 0 by A52, A68;
then A71: 0 < abs (r - (f . x1)) by COMPLEX1:133;
M + 0 < (abs M) + 1 by ABSVALUE:11, XREAL_1:10;
then (abs (r - (f . x1))) " < (abs M) + 1 by A70, XXREAL_0:2;
then 1 / ((abs M) + 1) < 1 / ((abs (r - (f . x1))) " ) by A71, XREAL_1:78;
hence 1 / ((abs M) + 1) < abs (r - (f . x1)) by XCMPLX_1:218; :: thesis: verum
end;
now
per cases ( p = g or p <> g ) ;
suppose p <> g ; :: thesis: contradiction
then p < g by A1, XXREAL_0:1;
then A72: 0 < g - p by XREAL_1:52;
then A73: 0 < (g - p) / s by A65, XREAL_1:141;
consider k being Element of NAT such that
A74: (g - p) / s < k by SEQ_4:10;
((g - p) / s) * s < s * k by A65, A74, XREAL_1:70;
then g - p < s * k by A65, XCMPLX_1:88;
then (g - p) / k < (s * k) / k by A74, A73, XREAL_1:76;
then (g - p) / k < (s * k) * (k " ) by XCMPLX_0:def 9;
then (g - p) / k < s * (k * (k " )) ;
then A75: (g - p) / k < s * 1 by A74, A73, XCMPLX_0:def 7;
deffunc H1( Element of NAT ) -> Element of REAL = g - (((g - p) / k) * $1);
consider s1 being Real_Sequence such that
A76: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch 1();
A77: 0 < (g - p) / k by A72, A74, A73, XREAL_1:141;
A78: now
let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) ) )
A79: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:91;
assume A80: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
then ((g - p) / k) * n < ((g - p) / k) * k by A77, XREAL_1:70;
then ((g - p) / k) * n < g - p by A74, A73, XCMPLX_1:88;
then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:17;
then A81: g - (g - p) < s1 . n by A76;
n + 1 <= k by A80, NAT_1:13;
then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A72, XREAL_1:66;
then ((g - p) / k) * (n + 1) <= g - p by A74, A73, XCMPLX_1:88;
then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:15;
then A82: g - (g - p) <= s1 . (n + 1) by A76;
g - (((g - p) / k) * n) <= g - 0 by A72, XREAL_1:15;
then s1 . n <= g by A76;
then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A81;
hence A83: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) )
g - (((g - p) / k) * (n + 1)) <= g - 0 by A72, XREAL_1:15;
then s1 . (n + 1) <= g by A76;
then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A82;
hence A84: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1)
abs ((s1 . (n + 1)) - (s1 . n)) = abs ((g - (((g - p) / k) * (n + 1))) - (s1 . n)) by A76
.= abs ((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))) by A76
.= abs (- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n)))
.= abs (((g - p) / k) * ((n + 1) - n)) by COMPLEX1:138
.= (g - p) / k by A72, ABSVALUE:def 1 ;
hence abs ((f . (s1 . (n + 1))) - (f . (s1 . n))) < 1 / ((abs M) + 1) by A66, A75, A83, A84, A79; :: thesis: verum
end;
defpred S1[ Nat] means r <= f . (s1 . $1);
A85: s1 . k = g - (((g - p) / k) * k) by A76
.= g - (g - p) by A74, A73, XCMPLX_1:88
.= p ;
then A86: ex n being Nat st S1[n] by A53;
consider l being Nat such that
A87: ( S1[l] & ( for m being Nat st S1[m] holds
l <= m ) ) from NAT_1:sch 5(A86);
s1 . 0 = g - (((g - p) / k) * 0 ) by A76
.= g ;
then l <> 0 by A53, A54, A87, XXREAL_0:1;
then consider l1 being Nat such that
A88: l = l1 + 1 by NAT_1:6;
reconsider l1 = l1 as Element of NAT by ORDINAL1:def 13;
A89: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A87, A88, XREAL_1:11;
l1 + 1 <= k by A53, A85, A87, A88;
then A90: l1 < k by NAT_1:13;
then A91: abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) < 1 / ((abs M) + 1) by A78;
f . (s1 . l1) < r
proof
assume r <= f . (s1 . l1) ; :: thesis: contradiction
then l <= l1 by A87;
then l + 0 < l by A88, XREAL_1:10;
hence contradiction ; :: thesis: verum
end;
then A92: 0 < r - (f . (s1 . l1)) by XREAL_1:52;
then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A87, A88, XREAL_1:11;
then abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;
then A93: abs (r - (f . (s1 . l1))) <= abs ((f . (s1 . (l1 + 1))) - (f . (s1 . l1))) by A92, A89, ABSVALUE:def 1;
s1 . l1 in [.p,g.] by A78, A90;
hence contradiction by A67, A93, A91, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
( f . p = f . g implies ex s being Real st
( s in [.p,g.] & r = f . s ) )
proof
assume A94: f . p = f . g ; :: thesis: ex s being Real st
( s in [.p,g.] & r = f . s )
take p ; :: thesis: ( p in [.p,g.] & r = f . p )
thus p in [.p,g.] by A1, XXREAL_1:1; :: thesis: r = f . p
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] = {(f . p)} by A94, XXREAL_1:17;
hence r = f . p by A4, TARSKI:def 1; :: thesis: verum
end;
hence ex s being Real st
( s in [.p,g.] & r = f . s ) by A6, A50, XXREAL_0:1; :: thesis: verum