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, Q 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 & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let f be Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)); :: thesis: for P, Q 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 & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let P, Q 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 & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q holds
f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
let PP, QQ be Subset of R^1; :: thesis: ( a < b & c < d & PP = P & QQ = Q & f is continuous & f is one-to-one & PP is compact & f . a = c & f . b = d & f .: P = Q implies f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) )
assume that
A1: ( a < b & c < d ) and
A2: PP = P and
A3: QQ = Q and
A4: ( f is continuous & f is one-to-one ) and
A5: PP is compact and
A6: ( f . a = c & f . b = d ) and
A7: f .: P = Q ; :: thesis: f . (upper_bound ([#] PP)) = upper_bound ([#] QQ)
A8: [#] (Closed-Interval-TSpace (c,d)) = the carrier of (Closed-Interval-TSpace (c,d)) ;
set IT = f . (upper_bound ([#] PP));
A9: [#] PP is real-bounded by A5, WEIERSTR:11;
[#] PP <> {} by A2, WEIERSTR:def 1;
then A10: upper_bound ([#] PP) in [#] PP by A5, A9, RCOMP_1:12, WEIERSTR:12;
then A11: upper_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 . (upper_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 A3, 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 = upper_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 1;
reconsider fr = f . x2, fx = f . x1 as Real ;
per cases ( r2 <> r1 or r2 = r1 ) ;
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, A4, A7, WEIERSTR:8;
then QQ is compact by A3, A7, A8, COMPTS_1:2;
then A18: [#] QQ is real-bounded by WEIERSTR:11;
upper_bound ([#] PP) in the carrier of (Closed-Interval-TSpace (a,b)) by A12, A10;
then upper_bound ([#] PP) in dom f by FUNCT_2:def 1;
then IT in QQ by A3, 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 - s < IT - 0 by A20, XREAL_1:15;
hence contradiction by A19, A21; :: thesis: verum
end;
hence f . (upper_bound ([#] PP)) = upper_bound ([#] QQ) by A18, A19, A13, SEQ_4:def 1; :: thesis: verum