let i, j be Element of NAT ; :: thesis: 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)
let f be Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)); :: thesis: ( ( for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) implies 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) )
assume A1: for fi being Element of (TOP-REAL i)
for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ; :: thesis: 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)
let r be Real; :: thesis: 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)
let fi be Point of (Euclid i); :: thesis: 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)
let fj be Point of (Euclid j); :: thesis: for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds
f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
let fij be Point of (Euclid (i + j)); :: thesis: ( fij = fi ^ fj implies f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) )
assume A2: fij = fi ^ fj ; :: thesis: f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r)
set Ii = Intervals (fi,r);
set Ij = Intervals (fj,r);
set Iij = Intervals (fij,r);
A3: OpenHypercube (fi,r) = product (Intervals (fi,r)) by EUCLID_9:def 4;
A4: [#] (TOP-REAL i) = [#] (TopSpaceMetr (Euclid i)) by Lm3;
A5: [#] (TOP-REAL j) = [#] (TopSpaceMetr (Euclid j)) by Lm3;
A6: OpenHypercube (fj,r) = product (Intervals (fj,r)) by EUCLID_9:def 4;
A7: (Intervals (fi,r)) ^ (Intervals (fj,r)) = Intervals (fij,r) by A2, RLAFFIN3:1;
A8: f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] c= product (Intervals (fij,r))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] or y in product (Intervals (fij,r)) )
assume y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] ; :: thesis: y in product (Intervals (fij,r))
then consider x being object such that
x in dom f and
A9: x in [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] and
A10: f . x = y by FUNCT_1:def 6;
consider xi, xj being object such that
A11: xi in product (Intervals (fi,r)) and
A12: xj in product (Intervals (fj,r)) and
A13: x = [xi,xj] by A9, ZFMISC_1:def 2;
reconsider xi = xi as Element of (TOP-REAL i) by A3, A4, A11;
reconsider xj = xj as Element of (TOP-REAL j) by A5, A6, A12;
y = f . (xi,xj) by A10, A13, BINOP_1:def 1
.= xi ^ xj by A1 ;
hence y in product (Intervals (fij,r)) by A7, A11, A12, RLAFFIN3:2; :: thesis: verum

end;

A14: product (Intervals (fij,r)) c= f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in product (Intervals (fij,r)) or y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] )
assume y in product (Intervals (fij,r)) ; :: thesis: y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):]
then consider p1, p2 being FinSequence such that
A15: y = p1 ^ p2 and
A16: ( p1 in product (Intervals (fi,r)) & p2 in product (Intervals (fj,r)) ) by A7, RLAFFIN3:2;
A17: [p1,p2] in [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] by A16, ZFMISC_1:87;
[p1,p2] in [:([#] (TOP-REAL i)),([#] (TOP-REAL j)):] by A3, A5, A4, A6, A16, ZFMISC_1:87;
then [p1,p2] in [#] [:(TOP-REAL i),(TOP-REAL j):] ;
then A18: [p1,p2] in dom f by FUNCT_2:def 1;
y = f . (p1,p2) by A1, A3, A5, A4, A6, A15, A16
.= f . [p1,p2] by BINOP_1:def 1 ;
hence y in f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):] by A17, A18, FUNCT_1:def 6; :: thesis: verum

end;

OpenHypercube (fij,r) = product (Intervals (fij,r)) by EUCLID_9:def 4;
hence f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) by A3, A6, A8, A14, XBOOLE_0:def 10; :: thesis: verum