for n being Nat
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 p being Point of (TOP-REAL n) ex G being Subset of REAL st
( G = { (f . (p,q)) where q is Point of (TOP-REAL n) : q in B } & g . p = lower_bound G ) ) holds
lower_bound (f .: [:A,B:]) = lower_bound (g .: A)