let i, j be 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)
let f be Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)); ( ( 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
; 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; 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); 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); 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)); ( fij = fi ^ fj implies f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) )
assume A2:
fij = fi ^ fj
; 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 ;
TARSKI:def 3 ( 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))):]
;
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;
verum
end;
A14:
product (Intervals (fij,r)) c= f .: [:(product (Intervals (fi,r))),(product (Intervals (fj,r))):]
proof
let y be
object ;
TARSKI:def 3 ( 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))
;
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;
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; verum