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 set ; :: 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 set 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;
A5: dom e = Seg n by EUCLID:3;
reconsider x = x as FinSequence by A1, A2, A4, A5, FINSEQ_1:def 2;
rng x c= REAL

proof

let b be set ; :: 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 set such that
A6: a in dom x and
A7: x . a = b by FUNCT_1:def 5;
A8: g . a in (Intervals e,r) . a by A1, A2, A3, A6;
(Intervals e,r) . a = ].((e . a) - r),((e . a) + r).[ by A1, A2, A4, A6, Def3;
hence b in REAL by A1, A7, A8; :: thesis: verum

end;

then x is FinSequence of REAL by FINSEQ_1:def 4;
then A9: x in REAL * by FINSEQ_1:def 11;
len e = n by FINSEQ_1:def 18;
then len x = n by A1, A2, A4, FINSEQ_3:31;
hence x in the carrier of (TopSpaceMetr (Euclid n)) by A9; :: thesis: verum

end;

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