let n be non zero Nat; for x being Subset of (REAL n)
for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
let x be Subset of (REAL n); for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
let a, b be Element of REAL n; ( ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) implies x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) )
assume A1:
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
; x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
defpred S1[ object , object ] means ex n being Nat st
( $1 = n & $2 = [.(a . n),(b . n).[ );
A2:
for i being Nat st i in Seg n holds
ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S1[i,d]
proof
let i be
Nat;
( i in Seg n implies ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S1[i,d] )
assume
i in Seg n
;
ex d being Element of the_set_of_all_right_open_real_bounded_intervals st S1[i,d]
set d =
[.(a . i),(b . i).[;
take
[.(a . i),(b . i).[
;
( [.(a . i),(b . i).[ is Element of the_set_of_all_right_open_real_bounded_intervals & S1[i,[.(a . i),(b . i).[] )
[.(a . i),(b . i).[ in { [.a,b.[ where a, b is Real : verum }
;
hence
[.(a . i),(b . i).[ is
Element of
the_set_of_all_right_open_real_bounded_intervals
;
S1[i,[.(a . i),(b . i).[]
thus
S1[
i,
[.(a . i),(b . i).[]
;
verum
end;
ex g being FinSequence of the_set_of_all_right_open_real_bounded_intervals st
( len g = n & ( for i being Nat st i in Seg n holds
S1[i,g /. i] ) )
from FINSEQ_4:sch 1(A2);
then consider g being FinSequence of the_set_of_all_right_open_real_bounded_intervals such that
A3:
len g = n
and
A4:
for i being Nat st i in Seg n holds
S1[i,g /. i]
;
A5:
for i being Nat st i in Seg n holds
g . i = [.(a . i),(b . i).[
ex g being Function st
( x = product g & g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) )
hence
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
by Def2; verum