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 real-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;
reconsider IT = f . (lower_bound ([#] PP)) as Real ;
A13: for r being Real st r in [#] QQ holds
IT <= r

proof

let r be Real; :: 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 object such that
A14: x in dom f and
A15: x in [#] PP and
A16: 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, A14;
x1 in the carrier of (Closed-Interval-TSpace (a,b)) ;
then reconsider r1 = x, r2 = x2 as Real ;
A17: r2 <= r1 by A9, A15, SEQ_4:def 2;
reconsider fr = f . x2, fx = f . x1 as Real ;

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

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

then r2 < r1 by A17, XXREAL_0:1;
then fr < fx by A1, A3, A4, A6, Th15;
hence IT <= r by A16; :: thesis: verum

end;

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

hence IT <= r by A16; :: 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 A18: [#] QQ is real-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 A19: IT in [#] QQ by WEIERSTR:def 1;
for s being Real st 0 < s holds
ex r being Real st
( r in [#] QQ & r < IT + s )

proof

given s being Real such that A20: 0 < s and
A21: for r being Real holds
( not r in [#] QQ or not r < IT + s ) ; :: thesis: contradiction
IT + 0 < IT + s by A20, XREAL_1:8;
hence contradiction by A19, A21; :: thesis: verum

end;

hence f . (lower_bound ([#] PP)) = lower_bound ([#] QQ) by A18, A19, A13, SEQ_4:def 2; :: thesis: verum