let n be non zero Nat; :: thesis: MeasurableRectangle (ProductRightOpenIntervals n) = Product (n,the_set_of_all_right_open_real_bounded_intervals)
thus MeasurableRectangle (ProductRightOpenIntervals n) c= Product (n,the_set_of_all_right_open_real_bounded_intervals) :: according to XBOOLE_0:def 10 :: thesis: Product (n,the_set_of_all_right_open_real_bounded_intervals) c= MeasurableRectangle (ProductRightOpenIntervals n)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in MeasurableRectangle (ProductRightOpenIntervals n) or x in Product (n,the_set_of_all_right_open_real_bounded_intervals) )
assume x in MeasurableRectangle (ProductRightOpenIntervals n) ; :: thesis: x in Product (n,the_set_of_all_right_open_real_bounded_intervals)
then consider y being Subset of (REAL n), a, b being Element of REAL n such that
A1: x = y and
A2: for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) ) by Th35;
now :: thesis: for t being Element of REAL n holds
( ( t in y implies for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) & ( ( for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) implies t in y ) )
let t be Element of REAL n; :: thesis: ( ( t in y implies for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) & ( ( for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) implies t in y ) )
hereby :: thesis: ( ( for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) implies t in y )
assume A3: t in y ; :: thesis: for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[
hereby :: thesis: verum
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).[
consider t0 being Element of REAL n such that
A5: t = t0 and
A6: for i being Nat st i in Seg n holds
t0 . i in [.(a . i),(b . i).[ by A3, A2;
thus t . i in [.(a . i),(b . i).[ by A6, A4, A5; :: thesis: verum
end;
end;
assume for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ; :: thesis: t in y
hence t in y by A2; :: thesis: verum
end;
then y is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) by Th45;
hence x in Product (n,the_set_of_all_right_open_real_bounded_intervals) by A1; :: thesis: verum
end;
thus Product (n,the_set_of_all_right_open_real_bounded_intervals) c= MeasurableRectangle (ProductRightOpenIntervals n) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Product (n,the_set_of_all_right_open_real_bounded_intervals) or x in MeasurableRectangle (ProductRightOpenIntervals n) )
assume x in Product (n,the_set_of_all_right_open_real_bounded_intervals) ; :: thesis: x in MeasurableRectangle (ProductRightOpenIntervals n)
then consider g being Function such that
A7: x = product g and
A8: g in product ((Seg n) --> the_set_of_all_right_open_real_bounded_intervals) by Def2;
thus x in MeasurableRectangle (ProductRightOpenIntervals n) by A7, A8, SRINGS_4:def 4; :: thesis: verum
end;