set T = TopSpaceMetr (Euclid n);
set f = Intervals (e,r);
product (Intervals (e,r)) c= the carrier of (TopSpaceMetr (Euclid n))
proof
let x be
object ;
TARSKI:def 3 ( not x in product (Intervals (e,r)) or x in the carrier of (TopSpaceMetr (Euclid n)) )
assume
x in product (Intervals (e,r))
;
x in the carrier of (TopSpaceMetr (Euclid n))
then consider g being
Function such that A1:
x = g
and A2:
dom g = dom (Intervals (e,r))
and A3:
for
y being
object st
y in dom (Intervals (e,r)) holds
g . y in (Intervals (e,r)) . y
by CARD_3:def 5;
A4:
dom (Intervals (e,r)) = dom e
by Def3;
dom e = Seg n
by FINSEQ_1:89;
then reconsider x =
x as
FinSequence by A1, A2, A4, FINSEQ_1:def 2;
rng x c= REAL
proof
let b be
object ;
TARSKI:def 3 ( not b in rng x or b in REAL )
assume
b in rng x
;
b in REAL
then consider a being
object such that A5:
a in dom x
and A6:
x . a = b
by FUNCT_1:def 3;
A7:
g . a in (Intervals (e,r)) . a
by A1, A2, A3, A5;
(Intervals (e,r)) . a = ].((e . a) - r),((e . a) + r).[
by A1, A2, A4, A5, Def3;
hence
b in REAL
by A1, A6, A7;
verum
end;
then
x is
FinSequence of
REAL
by FINSEQ_1:def 4;
then A8:
x in REAL *
by FINSEQ_1:def 11;
len e = n
by CARD_1:def 7;
then
len x = n
by A1, A2, A4, FINSEQ_3:29;
hence
x in the
carrier of
(TopSpaceMetr (Euclid n))
by A8;
verum
end;
hence
product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n))
; verum