let a, b, c, d be Real; :: thesis: for f being Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))
for P being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); :: thesis: for P being non empty Subset of (Closed-Interval-TSpace (a,b))
for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let P be non empty Subset of (Closed-Interval-TSpace (a,b)); :: thesis: for PP, QQ being Subset of R^1 st a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ holds
f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
let PP, QQ be Subset of R^1; :: thesis: ( a < b & c < d & PP = P & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = QQ implies f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) )
assume that
A1: ( a < b & c < d ) and
A2: PP = P and
A3: f is continuous and
A4: f is one-to-one and
A5: PP is compact and
A6: ( f . a = c & f . b = d ) and
A7: f .: P = QQ ; :: thesis: f . (lower_bound ([#] PP)) = lower_bound ([#] QQ)
A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ;
set IT = f . (lower_bound ([#] PP));
A9: [#] PP is bounded by A5, WEIERSTR:11;
[#] PP <> {} by A2, WEIERSTR:def 1;
then A10: lower_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:13, WEIERSTR:12;
then A11: lower_bound ([#] PP) in P by A2, WEIERSTR:def 1;
P c= the carrier of (Closed-Interval-TSpace (a,b)) ;
then A12: [#] PP c= the carrier of (Closed-Interval-TSpace (a,b)) by A2, WEIERSTR:def 1;
then A13: f . (lower_bound ([#] PP)) in the carrier of (Closed-Interval-TSpace (c,d)) by A10, FUNCT_2:5;
A14: [#] R^1 = the carrier of R^1 ;
then A15: the carrier of (Closed-Interval-TSpace (c,d)) c= the carrier of R^1 by A8, PRE_TOPC:def 4;
then reconsider IT = f . (lower_bound ([#] PP)) as Real by A13, TOPMETR:17;
[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then A16: the carrier of (Closed-Interval-TSpace (a,b)) c= the carrier of R^1 by A14, PRE_TOPC:def 4;
A17: for r being real number st r in [#] QQ holds
IT <= r

proof

let r be real number ; :: thesis: ( r in [#] QQ implies IT <= r )
assume r in [#] QQ ; :: thesis: IT <= r
then r in f .: P by A7, WEIERSTR:def 1;
then r in f .: ([#] PP) by A2, WEIERSTR:def 1;
then consider x being set such that
A18: x in dom f and
A19: x in [#] PP and
A20: r = f . x by FUNCT_1:def 6;
reconsider x1 = x, x2 = lower_bound ([#] PP) as Point of (Closed-Interval-TSpace (a,b)) by A11, A18;
x1 in the carrier of (Closed-Interval-TSpace (a,b)) ;
then reconsider r1 = x, r2 = x2 as Real by A16, TOPMETR:17;
A21: r2 <= r1 by A9, A19, SEQ_4:def 2;
( f . x1 in the carrier of (Closed-Interval-TSpace (c,d)) & f . x2 in the carrier of (Closed-Interval-TSpace (c,d)) ) ;
then reconsider fr = f . x2, fx = f . x1 as Real by A15, TOPMETR:17;

per cases ( r2 <> r1 or r2 = r1 ) ;

suppose r2 <> r1 ; :: thesis: IT <= r

then r2 < r1 by A21, XXREAL_0:1;
then fr < fx by A1, A3, A4, A6, Th16;
hence IT <= r by A20; :: thesis: verum

end;

suppose r2 = r1 ; :: thesis: IT <= r

hence IT <= r by A20; :: thesis: verum

end;

end;

end;

[#] (Closed-Interval-TSpace (a,b)) = the carrier of (Closed-Interval-TSpace (a,b)) ;
then P is compact by A2, A5, COMPTS_1:2;
then for P1 being Subset of (Closed-Interval-TSpace (c,d)) st P1 = QQ holds
P1 is compact by A3, A7, WEIERSTR:8;
then QQ is compact by A7, A8, COMPTS_1:2;
then A22: [#] QQ is bounded by WEIERSTR:11;
lower_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10;
then lower_bound ([#] PP) in dom f by FUNCT_2:def 1;
then IT in QQ by A7, A11, FUNCT_1:def 6;
then A23: IT in [#] QQ by WEIERSTR:def 1;
for s being real number st 0 < s holds
ex r being real number st
( r in [#] QQ & r < IT + s )

proof

given s being real number such that A24: 0 < s and
A25: for r being real number holds
( not r in [#] QQ or not r < IT + s ) ; :: thesis: contradiction
IT + 0 < IT + s by A24, XREAL_1:8;
hence contradiction by A23, A25; :: thesis: verum

end;

hence f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) by A22, A23, A17, SEQ_4:def 2; :: thesis: verum