set T = TopSpaceMetr ();
set f = Intervals (e,r);
product (Intervals (e,r)) c= the carrier of ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (Intervals (e,r)) or x in the carrier of () )
assume x in product (Intervals (e,r)) ; :: thesis: x in the carrier of ()
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 ;
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:
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 ;
hence x in the carrier of () by A8; :: thesis: verum
end;
hence product (Intervals (e,r)) is Subset of () ; :: thesis: verum