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 ; :: according to TARSKI:def 3 :: thesis: ( not x in product (Intervals (e,r)) or x in the carrier of (TopSpaceMetr (Euclid n)) )
assume x in product (Intervals (e,r)) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( not b in rng x or b in REAL )
assume b in rng x ; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;

hence product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n)) ; :: thesis: verum