set T = TopSpaceMetr (Euclid n);

set f = Intervals (e,r);

product (Intervals (e,r)) c= the carrier of (TopSpaceMetr (Euclid n))

set f = Intervals (e,r);

product (Intervals (e,r)) c= the carrier of (TopSpaceMetr (Euclid n))

proof

hence
product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n))
; :: thesis: verum
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

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;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

then
x is FinSequence of REAL
by FINSEQ_1:def 4;
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;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

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