theorem Th20: :: SIMPLEX2:20

for i, j being Element of NAT
for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds
for r being Real
for fi being Point of (Euclid i)
for fj being Point of (Euclid j)
for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)