let n be Nat; :: thesis: for A, B being non empty compact Subset of (TOP-REAL n)
for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: for f being continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]
for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let f be continuous RealMap of [:(TOP-REAL n),(TOP-REAL n):]; :: thesis: for g being RealMap of (TOP-REAL n) st ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
let g be RealMap of (TOP-REAL n); :: thesis: ( ( for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ) implies lower_bound (f .: [:A,B:]) = lower_bound (g .: B) )
assume A1: for q being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where p is Point of (TOP-REAL n) : p in A } & g . q = lower_bound G ) ; :: thesis: lower_bound (f .: [:A,B:]) = lower_bound (g .: B)
A2: [:A,B:] is compact by BORSUK_3:23;
then A3: f .: [:A,B:] is compact by Th1;
A4: f .: [:A,B:] is real-bounded by A2, Th1, RCOMP_1:10;
A5: g .: B c= f .: [:A,B:]

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in g .: B or u in f .: [:A,B:] )
assume u in g .: B ; :: thesis: u in f .: [:A,B:]
then consider q being Point of (TOP-REAL n) such that
A6: q in B and
A7: u = g . q by FUNCT_2:65;
consider p being Point of (TOP-REAL n) such that
A8: p in A by SUBSET_1:4;
consider G being Subset of REAL such that
A9: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and
A10: u = lower_bound G by A1, A7;
A11: f . (p,q) in G by A8, A9;
G c= f .: [:A,B:]

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; :: thesis: u in f .: [:A,B:]
then consider p1 being Point of (TOP-REAL n) such that
A12: u = f . (p1,q) and
A13: p1 in A by A9;
[p1,q] in [:A,B:] by A6, A13, ZFMISC_1:87;
hence u in f .: [:A,B:] by A12, FUNCT_2:35; :: thesis: verum

end;

hence u in f .: [:A,B:] by A3, A10, A11, Th2; :: thesis: verum

end;

then A14: g .: B is bounded_below by A4, XXREAL_2:44;
A15: for r being Real st r in f .: [:A,B:] holds
lower_bound (g .: B) <= r

proof

let r be Real; :: thesis: ( r in f .: [:A,B:] implies lower_bound (g .: B) <= r )
assume r in f .: [:A,B:] ; :: thesis: lower_bound (g .: B) <= r
then consider pq being Point of [:(TOP-REAL n),(TOP-REAL n):] such that
A16: pq in [:A,B:] and
A17: r = f . pq by FUNCT_2:65;
pq in the carrier of [:(TOP-REAL n),(TOP-REAL n):] ;
then pq in [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):] by BORSUK_1:def 2;
then consider p, q being object such that
A18: p in the carrier of (TOP-REAL n) and
A19: q in the carrier of (TOP-REAL n) and
A20: pq = [p,q] by ZFMISC_1:84;
A21: p in A by A16, A20, ZFMISC_1:87;
reconsider p = p, q = q as Point of (TOP-REAL n) by A18, A19;
consider G being Subset of REAL such that
A22: G = { (f . (p1,q)) where p1 is Point of (TOP-REAL n) : p1 in A } and
A23: g . q = lower_bound G by A1;
A24: q in B by A16, A20, ZFMISC_1:87;
G c= f .: [:A,B:]

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in G or u in f .: [:A,B:] )
assume u in G ; :: thesis: u in f .: [:A,B:]
then consider p1 being Point of (TOP-REAL n) such that
A25: u = f . (p1,q) and
A26: p1 in A by A22;
[p1,q] in [:A,B:] by A24, A26, ZFMISC_1:87;
hence u in f .: [:A,B:] by A25, FUNCT_2:35; :: thesis: verum

end;

then A27: G is bounded_below by A4, XXREAL_2:44;
r = f . (p,q) by A17, A20;
then r in G by A21, A22;
then A28: g . q <= r by A23, A27, SEQ_4:def 2;
g . q in g .: B by A24, FUNCT_2:35;
then lower_bound (g .: B) <= g . q by A14, SEQ_4:def 2;
hence lower_bound (g .: B) <= r by A28, XXREAL_0:2; :: thesis: verum

end;

for s being Real st 0 < s holds
ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )

proof

let s be Real; :: thesis: ( 0 < s implies ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s ) )
assume 0 < s ; :: thesis: ex r being Real st
( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
then consider r being Real such that
A29: r in g .: B and
A30: r < (lower_bound (g .: B)) + s by A14, SEQ_4:def 2;
take r ; :: thesis: ( r in f .: [:A,B:] & r < (lower_bound (g .: B)) + s )
thus r in f .: [:A,B:] by A5, A29; :: thesis: r < (lower_bound (g .: B)) + s
thus r < (lower_bound (g .: B)) + s by A30; :: thesis: verum

end;

hence lower_bound (f .: [:A,B:]) = lower_bound (g .: B) by A4, A15, SEQ_4:def 2; :: thesis: verum