let g, p 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:6;

A6: ( f . p < f . g implies ex s being Real st

( s in [.p,g.] & r = f . s ) )

( s in [.p,g.] & r = f . s ) )

( s in [.p,g.] & r = f . s ) )

( s in [.p,g.] & r = f . s ) by A6, A51, XXREAL_0:1; :: thesis: verum

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:6;

A6: ( f . p < f . g implies ex s being Real st

( s in [.p,g.] & r = f . s ) )

proof

A51:
( f . g < f . p implies ex s being Real st
r in REAL
by XREAL_0:def 1;

then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;

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 [.p,g.] by A1, XXREAL_1:1;

then A10: r <> f . p by A8;

reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;

A11: dom f1 = [.p,g.] by FUNCOP_1:13;

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} = {}

.= 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 ;

reconsider r = r as Element of REAL by XREAL_0:def 1;

for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds

f1 . x0 = r by A11, FUNCOP_1:7;

then f1 | [.p,g.] is V8() by PARTFUN2:57;

then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:18;

then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:21;

then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A14, FCONT_1:22;

then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A18, FCONT_1:29, RCOMP_1:10;

then consider M being Real such that

A19: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;

A20: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds

x1 <= M by A19, XXREAL_2:def 1;

0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;

then 0 < (|.M.| + 1) " ;

then A21: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;

f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;

then consider s being Real such that

A22: 0 < s and

A23: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A21, Th1;

end;then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;

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 [.p,g.] by A1, XXREAL_1:1;

then A10: r <> f . p by A8;

reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;

A11: dom f1 = [.p,g.] by FUNCOP_1:13;

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

A18: dom ((abs (f1 - f)) ^) =
(dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0})
by RFUNCT_1:def 2
assume
(abs (f1 - f)) " {0} <> {}
; :: thesis: contradiction

then consider x2 being Element of REAL such that

A15: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;

x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def 7;

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 7;

then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;

then |.((f1 - f) . x2).| = 0 by VALUED_1:18;

then (f1 - f) . x2 = 0 by ABSVALUE:2;

then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13;

then r - (f . x2) = 0 by A17, FUNCOP_1:7;

hence contradiction by A8, A17; :: thesis: verum

end;then consider x2 being Element of REAL such that

A15: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;

x2 in dom (abs (f1 - f)) by A15, FUNCT_1:def 7;

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 7;

then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;

then |.((f1 - f) . x2).| = 0 by VALUED_1:18;

then (f1 - f) . x2 = 0 by ABSVALUE:2;

then (f1 . x2) - (f . x2) = 0 by A16, VALUED_1:13;

then r - (f . x2) = 0 by A17, FUNCOP_1:7;

hence contradiction by A8, A17; :: thesis: verum

.= 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 ;

reconsider r = r as Element of REAL by XREAL_0:def 1;

for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds

f1 . x0 = r by A11, FUNCOP_1:7;

then f1 | [.p,g.] is V8() by PARTFUN2:57;

then (f1 - f) | [.p,g.] is continuous by A3, A12, FCONT_1:18;

then (abs (f1 - f)) | [.p,g.] is continuous by A13, FCONT_1:21;

then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A14, FCONT_1:22;

then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A18, FCONT_1:29, RCOMP_1:10;

then consider M being Real such that

A19: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;

A20: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds

x1 <= M by A19, XXREAL_2:def 1;

0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;

then 0 < (|.M.| + 1) " ;

then A21: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;

f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;

then consider s being Real such that

A22: 0 < s and

A23: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A21, Th1;

A24: now :: thesis: for x1 being Real st x1 in [.p,g.] holds

1 / (|.M.| + 1) < |.(r - (f . x1)).|

1 / (|.M.| + 1) < |.(r - (f . x1)).|

let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / (|.M.| + 1) < |.(r - (f . x1)).| )

assume A25: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|

then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A18, FUNCT_1:def 6;

then ((abs (f1 - f)) ^) . x1 <= M by A20;

then ((abs (f1 - f)) . x1) " <= M by A18, A25, RFUNCT_1:def 2;

then A26: |.((f1 - f) . x1).| " <= M by VALUED_1:18;

x1 in (dom f1) /\ (dom f) by A2, A11, A25, XBOOLE_0:def 4;

then x1 in dom (f1 - f) by VALUED_1:12;

then |.((f1 . x1) - (f . x1)).| " <= M by A26, VALUED_1:13;

then A27: |.(r - (f . x1)).| " <= M by A25, FUNCOP_1:7;

r - (f . x1) <> 0 by A8, A25;

then A28: 0 < |.(r - (f . x1)).| by COMPLEX1:47;

M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;

then |.(r - (f . x1)).| " < |.M.| + 1 by A27, XXREAL_0:2;

then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A28, XREAL_1:76;

hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

end;assume A25: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|

then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A18, FUNCT_1:def 6;

then ((abs (f1 - f)) ^) . x1 <= M by A20;

then ((abs (f1 - f)) . x1) " <= M by A18, A25, RFUNCT_1:def 2;

then A26: |.((f1 - f) . x1).| " <= M by VALUED_1:18;

x1 in (dom f1) /\ (dom f) by A2, A11, A25, XBOOLE_0:def 4;

then x1 in dom (f1 - f) by VALUED_1:12;

then |.((f1 . x1) - (f . x1)).| " <= M by A26, VALUED_1:13;

then A27: |.(r - (f . x1)).| " <= M by A25, FUNCOP_1:7;

r - (f . x1) <> 0 by A8, A25;

then A28: 0 < |.(r - (f . x1)).| by COMPLEX1:47;

M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;

then |.(r - (f . x1)).| " < |.M.| + 1 by A27, XXREAL_0:2;

then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A28, XREAL_1:76;

hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p = g or p <> g )
;

end;

suppose
p <> g
; :: thesis: contradiction

then
p < g
by A1, XXREAL_0:1;

then A29: 0 < g - p by XREAL_1:50;

then A30: 0 < (g - p) / s by A22, XREAL_1:139;

consider k being Nat such that

A31: (g - p) / s < k by SEQ_4:3;

((g - p) / s) * s < s * k by A22, A31, XREAL_1:68;

then g - p < s * k by A22, XCMPLX_1:87;

then (g - p) / k < (s * k) / k by A31, A30, XREAL_1:74;

then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;

then (g - p) / k < s * (k * (k ")) ;

then A32: (g - p) / k < s * 1 by A31, A30, XCMPLX_0:def 7;

deffunc H_{1}( Nat) -> set = p + (((g - p) / k) * $1);

consider s1 being Real_Sequence such that

A33: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

A34: 0 < (g - p) / k by A29, A31, A30, XREAL_1:139;

_{1}[ Nat] means r <= f . (s1 . $1);

A42: s1 . k = p + (((g - p) / k) * k) by A33

.= p + (g - p) by A31, A30, XCMPLX_1:87

.= g ;

then A43: ex n being Nat st S_{1}[n]
by A9;

consider l being Nat such that

A44: ( S_{1}[l] & ( for m being Nat st S_{1}[m] holds

l <= m ) ) from NAT_1:sch 5(A43);

s1 . 0 = p + (((g - p) / k) * 0) by A33

.= p ;

then l <> 0 by A9, A10, A44, XXREAL_0:1;

then consider l1 being Nat such that

A45: l = l1 + 1 by NAT_1:6;

reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;

A46: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;

l1 + 1 <= k by A9, A42, A44, A45;

then A47: l1 < k by NAT_1:13;

then A48: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A35;

f . (s1 . l1) < r

then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;

then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;

then A50: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A49, A46, ABSVALUE:def 1;

s1 . l1 in [.p,g.] by A35, A47;

hence contradiction by A24, A50, A48, XXREAL_0:2; :: thesis: verum

end;then A29: 0 < g - p by XREAL_1:50;

then A30: 0 < (g - p) / s by A22, XREAL_1:139;

consider k being Nat such that

A31: (g - p) / s < k by SEQ_4:3;

((g - p) / s) * s < s * k by A22, A31, XREAL_1:68;

then g - p < s * k by A22, XCMPLX_1:87;

then (g - p) / k < (s * k) / k by A31, A30, XREAL_1:74;

then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;

then (g - p) / k < s * (k * (k ")) ;

then A32: (g - p) / k < s * 1 by A31, A30, XCMPLX_0:def 7;

deffunc H

consider s1 being Real_Sequence such that

A33: for n being Nat holds s1 . n = H

A34: 0 < (g - p) / k by A29, A31, A30, XREAL_1:139;

A35: now :: thesis: for n being Element of NAT st n < k holds

( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

defpred S( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) ) )

A36: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;

assume A37: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

then ((g - p) / k) * n < ((g - p) / k) * k by A34, XREAL_1:68;

then ((g - p) / k) * n < g - p by A31, A30, XCMPLX_1:87;

then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:6;

then A38: s1 . n < p + (g - p) by A33;

n + 1 <= k by A37, NAT_1:13;

then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A29, XREAL_1:64;

then ((g - p) / k) * (n + 1) <= g - p by A31, A30, XCMPLX_1:87;

then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:7;

then A39: s1 . (n + 1) <= p + (g - p) by A33;

p + 0 <= p + (((g - p) / k) * n) by A29, XREAL_1:7;

then p <= s1 . n by A33;

then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38;

hence A40: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

p + 0 <= p + (((g - p) / k) * (n + 1)) by A29, XREAL_1:7;

then p <= s1 . (n + 1) by A33;

then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A39;

hence A41: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)

|.((s1 . (n + 1)) - (s1 . n)).| = |.((p + (((g - p) / k) * (n + 1))) - (s1 . n)).| by A33

.= |.((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))).| by A33

.= (g - p) / k by A29, ABSVALUE:def 1 ;

hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A23, A32, A40, A41, A36; :: thesis: verum

end;A36: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;

assume A37: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

then ((g - p) / k) * n < ((g - p) / k) * k by A34, XREAL_1:68;

then ((g - p) / k) * n < g - p by A31, A30, XCMPLX_1:87;

then p + (((g - p) / k) * n) < p + (g - p) by XREAL_1:6;

then A38: s1 . n < p + (g - p) by A33;

n + 1 <= k by A37, NAT_1:13;

then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A29, XREAL_1:64;

then ((g - p) / k) * (n + 1) <= g - p by A31, A30, XCMPLX_1:87;

then p + (((g - p) / k) * (n + 1)) <= p + (g - p) by XREAL_1:7;

then A39: s1 . (n + 1) <= p + (g - p) by A33;

p + 0 <= p + (((g - p) / k) * n) by A29, XREAL_1:7;

then p <= s1 . n by A33;

then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A38;

hence A40: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

p + 0 <= p + (((g - p) / k) * (n + 1)) by A29, XREAL_1:7;

then p <= s1 . (n + 1) by A33;

then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A39;

hence A41: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)

|.((s1 . (n + 1)) - (s1 . n)).| = |.((p + (((g - p) / k) * (n + 1))) - (s1 . n)).| by A33

.= |.((p + (((g - p) / k) * (n + 1))) - (p + (((g - p) / k) * n))).| by A33

.= (g - p) / k by A29, ABSVALUE:def 1 ;

hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A23, A32, A40, A41, A36; :: thesis: verum

A42: s1 . k = p + (((g - p) / k) * k) by A33

.= p + (g - p) by A31, A30, XCMPLX_1:87

.= g ;

then A43: ex n being Nat st S

consider l being Nat such that

A44: ( S

l <= m ) ) from NAT_1:sch 5(A43);

s1 . 0 = p + (((g - p) / k) * 0) by A33

.= p ;

then l <> 0 by A9, A10, A44, XXREAL_0:1;

then consider l1 being Nat such that

A45: l = l1 + 1 by NAT_1:6;

reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;

A46: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;

l1 + 1 <= k by A9, A42, A44, A45;

then A47: l1 < k by NAT_1:13;

then A48: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A35;

f . (s1 . l1) < r

proof

then A49:
0 < r - (f . (s1 . l1))
by XREAL_1:50;
assume
r <= f . (s1 . l1)
; :: thesis: contradiction

then l <= l1 by A44;

then l + 0 < l by A45, XREAL_1:8;

hence contradiction ; :: thesis: verum

end;then l <= l1 by A44;

then l + 0 < l by A45, XREAL_1:8;

hence contradiction ; :: thesis: verum

then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A44, A45, XREAL_1:9;

then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;

then A50: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A49, A46, ABSVALUE:def 1;

s1 . l1 in [.p,g.] by A35, A47;

hence contradiction by A24, A50, A48, XXREAL_0:2; :: thesis: verum

( s in [.p,g.] & r = f . s ) )

proof

( f . p = f . g implies ex s being Real st
r in REAL
by XREAL_0:def 1;

then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;

assume that

A52: f . g < f . p and

A53: 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 A52, 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 A54: 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 A55: r <> f . g by A53;

reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;

A56: dom f1 = [.p,g.] by FUNCOP_1:13;

then A57: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;

then A58: [.p,g.] c= dom (f1 - f) by VALUED_1:12;

A59: (abs (f1 - f)) " {0} = {}

.= dom (f1 - f) by A59, VALUED_1:def 11

.= [.p,g.] /\ (dom f) by A56, VALUED_1:12

.= [.p,g.] by A2, XBOOLE_1:28 ;

reconsider r = r as Element of REAL by XREAL_0:def 1;

for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds

f1 . x0 = r by A56, FUNCOP_1:7;

then f1 | [.p,g.] is V8() by PARTFUN2:57;

then (f1 - f) | [.p,g.] is continuous by A3, A57, FCONT_1:18;

then (abs (f1 - f)) | [.p,g.] is continuous by A58, FCONT_1:21;

then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A59, FCONT_1:22;

then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A63, FCONT_1:29, RCOMP_1:10;

then consider M being Real such that

A64: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;

A65: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds

x1 <= M by A64, XXREAL_2:def 1;

0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;

then 0 < (|.M.| + 1) " ;

then A66: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;

f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;

then consider s being Real such that

A67: 0 < s and

A68: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A66, Th1;

end;then reconsider f1 = [.p,g.] --> r as Function of [.p,g.],REAL by FUNCOP_1:45;

assume that

A52: f . g < f . p and

A53: 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 A52, 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 A54: 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 A55: r <> f . g by A53;

reconsider f1 = f1 as PartFunc of REAL,REAL by RELSET_1:7;

A56: dom f1 = [.p,g.] by FUNCOP_1:13;

then A57: [.p,g.] c= (dom f1) /\ (dom f) by A2, XBOOLE_1:19;

then A58: [.p,g.] c= dom (f1 - f) by VALUED_1:12;

A59: (abs (f1 - f)) " {0} = {}

proof

A63: dom ((abs (f1 - f)) ^) =
(dom (abs (f1 - f))) \ ((abs (f1 - f)) " {0})
by RFUNCT_1:def 2
assume
(abs (f1 - f)) " {0} <> {}
; :: thesis: contradiction

then consider x2 being Element of REAL such that

A60: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;

x2 in dom (abs (f1 - f)) by A60, FUNCT_1:def 7;

then A61: x2 in dom (f1 - f) by VALUED_1:def 11;

then x2 in (dom f1) /\ (dom f) by VALUED_1:12;

then A62: x2 in [.p,g.] by A56, XBOOLE_0:def 4;

(abs (f1 - f)) . x2 in {0} by A60, FUNCT_1:def 7;

then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;

then |.((f1 - f) . x2).| = 0 by VALUED_1:18;

then (f1 - f) . x2 = 0 by ABSVALUE:2;

then (f1 . x2) - (f . x2) = 0 by A61, VALUED_1:13;

then r - (f . x2) = 0 by A62, FUNCOP_1:7;

hence contradiction by A53, A62; :: thesis: verum

end;then consider x2 being Element of REAL such that

A60: x2 in (abs (f1 - f)) " {0} by SUBSET_1:4;

x2 in dom (abs (f1 - f)) by A60, FUNCT_1:def 7;

then A61: x2 in dom (f1 - f) by VALUED_1:def 11;

then x2 in (dom f1) /\ (dom f) by VALUED_1:12;

then A62: x2 in [.p,g.] by A56, XBOOLE_0:def 4;

(abs (f1 - f)) . x2 in {0} by A60, FUNCT_1:def 7;

then (abs (f1 - f)) . x2 = 0 by TARSKI:def 1;

then |.((f1 - f) . x2).| = 0 by VALUED_1:18;

then (f1 - f) . x2 = 0 by ABSVALUE:2;

then (f1 . x2) - (f . x2) = 0 by A61, VALUED_1:13;

then r - (f . x2) = 0 by A62, FUNCOP_1:7;

hence contradiction by A53, A62; :: thesis: verum

.= dom (f1 - f) by A59, VALUED_1:def 11

.= [.p,g.] /\ (dom f) by A56, VALUED_1:12

.= [.p,g.] by A2, XBOOLE_1:28 ;

reconsider r = r as Element of REAL by XREAL_0:def 1;

for x0 being Element of REAL st x0 in [.p,g.] /\ (dom f1) holds

f1 . x0 = r by A56, FUNCOP_1:7;

then f1 | [.p,g.] is V8() by PARTFUN2:57;

then (f1 - f) | [.p,g.] is continuous by A3, A57, FCONT_1:18;

then (abs (f1 - f)) | [.p,g.] is continuous by A58, FCONT_1:21;

then ((abs (f1 - f)) ^) | [.p,g.] is continuous by A59, FCONT_1:22;

then ((abs (f1 - f)) ^) .: [.p,g.] is real-bounded by A5, A63, FCONT_1:29, RCOMP_1:10;

then consider M being Real such that

A64: M is UpperBound of ((abs (f1 - f)) ^) .: [.p,g.] by XXREAL_2:def 10;

A65: for x1 being Real st x1 in ((abs (f1 - f)) ^) .: [.p,g.] holds

x1 <= M by A64, XXREAL_2:def 1;

0 + 0 < |.M.| + 1 by COMPLEX1:46, XREAL_1:8;

then 0 < (|.M.| + 1) " ;

then A66: 0 < 1 / (|.M.| + 1) by XCMPLX_1:215;

f | [.p,g.] is uniformly_continuous by A2, A3, Th11, RCOMP_1:6;

then consider s being Real such that

A67: 0 < s and

A68: for x1, x2 being Real st x1 in dom (f | [.p,g.]) & x2 in dom (f | [.p,g.]) & |.(x1 - x2).| < s holds

|.((f . x1) - (f . x2)).| < 1 / (|.M.| + 1) by A66, Th1;

A69: now :: thesis: for x1 being Real st x1 in [.p,g.] holds

1 / (|.M.| + 1) < |.(r - (f . x1)).|

1 / (|.M.| + 1) < |.(r - (f . x1)).|

let x1 be Real; :: thesis: ( x1 in [.p,g.] implies 1 / (|.M.| + 1) < |.(r - (f . x1)).| )

assume A70: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|

then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A63, FUNCT_1:def 6;

then ((abs (f1 - f)) ^) . x1 <= M by A65;

then ((abs (f1 - f)) . x1) " <= M by A63, A70, RFUNCT_1:def 2;

then A71: |.((f1 - f) . x1).| " <= M by VALUED_1:18;

x1 in (dom f1) /\ (dom f) by A2, A56, A70, XBOOLE_0:def 4;

then x1 in dom (f1 - f) by VALUED_1:12;

then |.((f1 . x1) - (f . x1)).| " <= M by A71, VALUED_1:13;

then A72: |.(r - (f . x1)).| " <= M by A70, FUNCOP_1:7;

r - (f . x1) <> 0 by A53, A70;

then A73: 0 < |.(r - (f . x1)).| by COMPLEX1:47;

M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;

then |.(r - (f . x1)).| " < |.M.| + 1 by A72, XXREAL_0:2;

then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A73, XREAL_1:76;

hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

end;assume A70: x1 in [.p,g.] ; :: thesis: 1 / (|.M.| + 1) < |.(r - (f . x1)).|

then ((abs (f1 - f)) ^) . x1 in ((abs (f1 - f)) ^) .: [.p,g.] by A63, FUNCT_1:def 6;

then ((abs (f1 - f)) ^) . x1 <= M by A65;

then ((abs (f1 - f)) . x1) " <= M by A63, A70, RFUNCT_1:def 2;

then A71: |.((f1 - f) . x1).| " <= M by VALUED_1:18;

x1 in (dom f1) /\ (dom f) by A2, A56, A70, XBOOLE_0:def 4;

then x1 in dom (f1 - f) by VALUED_1:12;

then |.((f1 . x1) - (f . x1)).| " <= M by A71, VALUED_1:13;

then A72: |.(r - (f . x1)).| " <= M by A70, FUNCOP_1:7;

r - (f . x1) <> 0 by A53, A70;

then A73: 0 < |.(r - (f . x1)).| by COMPLEX1:47;

M + 0 < |.M.| + 1 by ABSVALUE:4, XREAL_1:8;

then |.(r - (f . x1)).| " < |.M.| + 1 by A72, XXREAL_0:2;

then 1 / (|.M.| + 1) < 1 / (|.(r - (f . x1)).| ") by A73, XREAL_1:76;

hence 1 / (|.M.| + 1) < |.(r - (f . x1)).| by XCMPLX_1:216; :: thesis: verum

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( p = g or p <> g )
;

end;

suppose
p <> g
; :: thesis: contradiction

then
p < g
by A1, XXREAL_0:1;

then A74: 0 < g - p by XREAL_1:50;

then A75: 0 < (g - p) / s by A67, XREAL_1:139;

consider k being Nat such that

A76: (g - p) / s < k by SEQ_4:3;

((g - p) / s) * s < s * k by A67, A76, XREAL_1:68;

then g - p < s * k by A67, XCMPLX_1:87;

then (g - p) / k < (s * k) / k by A76, A75, XREAL_1:74;

then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;

then (g - p) / k < s * (k * (k ")) ;

then A77: (g - p) / k < s * 1 by A76, A75, XCMPLX_0:def 7;

deffunc H_{1}( Nat) -> set = g - (((g - p) / k) * $1);

consider s1 being Real_Sequence such that

A78: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

A79: 0 < (g - p) / k by A74, A76, A75, XREAL_1:139;

_{1}[ Nat] means r <= f . (s1 . $1);

A87: s1 . k = g - (((g - p) / k) * k) by A78

.= g - (g - p) by A76, A75, XCMPLX_1:87

.= p ;

then A88: ex n being Nat st S_{1}[n]
by A54;

consider l being Nat such that

A89: ( S_{1}[l] & ( for m being Nat st S_{1}[m] holds

l <= m ) ) from NAT_1:sch 5(A88);

s1 . 0 = g - (((g - p) / k) * 0) by A78

.= g ;

then l <> 0 by A54, A55, A89, XXREAL_0:1;

then consider l1 being Nat such that

A90: l = l1 + 1 by NAT_1:6;

reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;

A91: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;

l1 + 1 <= k by A54, A87, A89, A90;

then A92: l1 < k by NAT_1:13;

then A93: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A80;

f . (s1 . l1) < r

then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;

then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;

then A95: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A94, A91, ABSVALUE:def 1;

s1 . l1 in [.p,g.] by A80, A92;

hence contradiction by A69, A95, A93, XXREAL_0:2; :: thesis: verum

end;then A74: 0 < g - p by XREAL_1:50;

then A75: 0 < (g - p) / s by A67, XREAL_1:139;

consider k being Nat such that

A76: (g - p) / s < k by SEQ_4:3;

((g - p) / s) * s < s * k by A67, A76, XREAL_1:68;

then g - p < s * k by A67, XCMPLX_1:87;

then (g - p) / k < (s * k) / k by A76, A75, XREAL_1:74;

then (g - p) / k < (s * k) * (k ") by XCMPLX_0:def 9;

then (g - p) / k < s * (k * (k ")) ;

then A77: (g - p) / k < s * 1 by A76, A75, XCMPLX_0:def 7;

deffunc H

consider s1 being Real_Sequence such that

A78: for n being Nat holds s1 . n = H

A79: 0 < (g - p) / k by A74, A76, A75, XREAL_1:139;

A80: now :: thesis: for n being Element of NAT st n < k holds

( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

defpred S( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

let n be Element of NAT ; :: thesis: ( n < k implies ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) ) )

A81: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;

assume A82: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

then ((g - p) / k) * n < ((g - p) / k) * k by A79, XREAL_1:68;

then ((g - p) / k) * n < g - p by A76, A75, XCMPLX_1:87;

then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:15;

then A83: g - (g - p) < s1 . n by A78;

n + 1 <= k by A82, NAT_1:13;

then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A74, XREAL_1:64;

then ((g - p) / k) * (n + 1) <= g - p by A76, A75, XCMPLX_1:87;

then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:13;

then A84: g - (g - p) <= s1 . (n + 1) by A78;

g - (((g - p) / k) * n) <= g - 0 by A74, XREAL_1:13;

then s1 . n <= g by A78;

then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A83;

hence A85: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

g - (((g - p) / k) * (n + 1)) <= g - 0 by A74, XREAL_1:13;

then s1 . (n + 1) <= g by A78;

then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A84;

hence A86: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)

|.((s1 . (n + 1)) - (s1 . n)).| = |.((g - (((g - p) / k) * (n + 1))) - (s1 . n)).| by A78

.= |.((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))).| by A78

.= |.(- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n))).|

.= |.(((g - p) / k) * ((n + 1) - n)).| by COMPLEX1:52

.= (g - p) / k by A74, ABSVALUE:def 1 ;

hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A68, A77, A85, A86, A81; :: thesis: verum

end;A81: dom (f | [.p,g.]) = [.p,g.] by A2, RELAT_1:62;

assume A82: n < k ; :: thesis: ( s1 . n in [.p,g.] & s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

then ((g - p) / k) * n < ((g - p) / k) * k by A79, XREAL_1:68;

then ((g - p) / k) * n < g - p by A76, A75, XCMPLX_1:87;

then g - (g - p) < g - (((g - p) / k) * n) by XREAL_1:15;

then A83: g - (g - p) < s1 . n by A78;

n + 1 <= k by A82, NAT_1:13;

then ((g - p) / k) * (n + 1) <= ((g - p) / k) * k by A74, XREAL_1:64;

then ((g - p) / k) * (n + 1) <= g - p by A76, A75, XCMPLX_1:87;

then g - (g - p) <= g - (((g - p) / k) * (n + 1)) by XREAL_1:13;

then A84: g - (g - p) <= s1 . (n + 1) by A78;

g - (((g - p) / k) * n) <= g - 0 by A74, XREAL_1:13;

then s1 . n <= g by A78;

then s1 . n in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A83;

hence A85: s1 . n in [.p,g.] by RCOMP_1:def 1; :: thesis: ( s1 . (n + 1) in [.p,g.] & |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) )

g - (((g - p) / k) * (n + 1)) <= g - 0 by A74, XREAL_1:13;

then s1 . (n + 1) <= g by A78;

then s1 . (n + 1) in { x2 where x2 is Real : ( p <= x2 & x2 <= g ) } by A84;

hence A86: s1 . (n + 1) in [.p,g.] by RCOMP_1:def 1; :: thesis: |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1)

|.((s1 . (n + 1)) - (s1 . n)).| = |.((g - (((g - p) / k) * (n + 1))) - (s1 . n)).| by A78

.= |.((g - (((g - p) / k) * (n + 1))) - (g - (((g - p) / k) * n))).| by A78

.= |.(- ((((g - p) / k) * (n + 1)) - (((g - p) / k) * n))).|

.= |.(((g - p) / k) * ((n + 1) - n)).| by COMPLEX1:52

.= (g - p) / k by A74, ABSVALUE:def 1 ;

hence |.((f . (s1 . (n + 1))) - (f . (s1 . n))).| < 1 / (|.M.| + 1) by A68, A77, A85, A86, A81; :: thesis: verum

A87: s1 . k = g - (((g - p) / k) * k) by A78

.= g - (g - p) by A76, A75, XCMPLX_1:87

.= p ;

then A88: ex n being Nat st S

consider l being Nat such that

A89: ( S

l <= m ) ) from NAT_1:sch 5(A88);

s1 . 0 = g - (((g - p) / k) * 0) by A78

.= g ;

then l <> 0 by A54, A55, A89, XXREAL_0:1;

then consider l1 being Nat such that

A90: l = l1 + 1 by NAT_1:6;

reconsider l1 = l1 as Element of NAT by ORDINAL1:def 12;

A91: r - (f . (s1 . l1)) <= (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;

l1 + 1 <= k by A54, A87, A89, A90;

then A92: l1 < k by NAT_1:13;

then A93: |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| < 1 / (|.M.| + 1) by A80;

f . (s1 . l1) < r

proof

then A94:
0 < r - (f . (s1 . l1))
by XREAL_1:50;
assume
r <= f . (s1 . l1)
; :: thesis: contradiction

then l <= l1 by A89;

then l + 0 < l by A90, XREAL_1:8;

hence contradiction ; :: thesis: verum

end;then l <= l1 by A89;

then l + 0 < l by A90, XREAL_1:8;

hence contradiction ; :: thesis: verum

then 0 < (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by A89, A90, XREAL_1:9;

then |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| = (f . (s1 . (l1 + 1))) - (f . (s1 . l1)) by ABSVALUE:def 1;

then A95: |.(r - (f . (s1 . l1))).| <= |.((f . (s1 . (l1 + 1))) - (f . (s1 . l1))).| by A94, A91, ABSVALUE:def 1;

s1 . l1 in [.p,g.] by A80, A92;

hence contradiction by A69, A95, A93, XXREAL_0:2; :: thesis: verum

( s in [.p,g.] & r = f . s ) )

proof

hence
ex s being Real st
assume A96:
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 A96, XXREAL_1:17;

hence r = f . p by A4, TARSKI:def 1; :: thesis: verum

end;( 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 A96, XXREAL_1:17;

hence r = f . p by A4, TARSKI:def 1; :: thesis: verum

( s in [.p,g.] & r = f . s ) by A6, A51, XXREAL_0:1; :: thesis: verum