let n be non zero Nat; :: thesis: for x being Element of Product (n,the_set_of_all_left_open_real_bounded_intervals) ex 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).] )
let x be Element of Product (n,the_set_of_all_left_open_real_bounded_intervals); :: thesis: ex 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).] )
consider s being Tuple of n, the_set_of_all_left_open_real_bounded_intervals such that
A1: for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) by Th42;
consider a, b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).] by Th46;
take a ; :: thesis: ex 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).] )
take b ; :: thesis: 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).] )
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).] )

proof

let t be Element of REAL n; :: thesis: ( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] )

hereby :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) implies t in x )

assume A3: t in x ; :: thesis: for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).]
thus for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] :: thesis: verum

proof

let i be Nat; :: thesis: ( i in Seg n implies t . i in ].(a . i),(b . i).] )
assume A4: i in Seg n ; :: thesis: t . i in ].(a . i),(b . i).]
then s . i = ].(a . i),(b . i).] by A2;
hence t . i in ].(a . i),(b . i).] by A1, A3, A4; :: thesis: verum

end;

end;

assume A5: for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ; :: thesis: t in x
for i being Nat st i in Seg n holds
t . i in s . i

proof

let i be Nat; :: thesis: ( i in Seg n implies t . i in s . i )
assume A6: i in Seg n ; :: thesis: t . i in s . i
then s . i = ].(a . i),(b . i).] by A2;
hence t . i in s . i by A6, A5; :: thesis: verum

end;

hence t in x by A1; :: thesis: verum

end;

hence 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).] ) ; :: thesis: verum