let A be Subset of [:RNS_Real,RNS_Real:]; :: thesis:
assume A1: A is open ; :: thesis:

hence A in sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:4; :: thesis:

end;

suppose ex a, b being Real st
( [a,b] in A & ( for Rx being real-membered set holds
( Rx is empty or not Rx is bounded_above or not Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ) ) ; :: thesis:

then consider a, b being Real such that
A3: ( [a,b] in A & ( for Rx being real-membered set holds
( Rx is empty or not Rx is bounded_above or not Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ) ) ;
set Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ;

now :: thesis:

let z be object ; :: thesis:
assume z in { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ; :: thesis:
then ex r being Real st
( z = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) ;
hence z is real ; :: thesis:

end;

then reconsider Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } as real-membered set by MEMBERED:def 3;
reconsider a1 = a, b1 = b as Point of RNS_Real by XREAL_0:def 1;
reconsider x = [a1,b1] as Point of [:RNS_Real,RNS_Real:] ;
consider r0 being Real such that
A4: ( r0 > 0 & Ball (x,r0) c= A ) by A1, A3, NDIFF_8:20;
consider s, aa, bb being Real such that
A5: ( 0 < s & s < r0 & x = [aa,bb] & [:].(aa - s),(aa + s).[,].(bb - s),(bb + s).[:] c= Ball (x,r0) ) by A4, Th13;
A6: [:].(aa - s),(aa + s).[,].(bb - s),(bb + s).[:] c= A by A5, A4;
( a = aa & b = bb ) by A5, XTUPLE_0:1;
then s in Rx by A5, A6;
then A7: not Rx is bounded_above by A3;

now :: thesis:

let z be object ; :: thesis:
assume z in [:REAL,REAL:] ; :: thesis:
then consider x1, y1 being object such that
A8: ( x1 in REAL & y1 in REAL & z = [x1,y1] ) by ZFMISC_1:def 2;
reconsider x1 = x1, y1 = y1 as Real by A8;
consider r1 being Real such that
A9: ( 0 < r1 & x1 in ].(a - r1),(a + r1).[ ) by Lm1;
consider r2 being Real such that
A10: ( 0 < r2 & y1 in ].(b - r2),(b + r2).[ ) by Lm1;
reconsider r = max (r1,r2) as Real ;
( ].(a - r1),(a + r1).[ c= ].(a - r),(a + r).[ & ].(b - r2),(b + r2).[ c= ].(b - r),(b + r).[ ) by Lm2, XXREAL_0:25;
then A11: z in [:].(a - r),(a + r).[,].(b - r),(b + r).[:] by A8, A9, A10, ZFMISC_1:87;
r is not UpperBound of Rx by A7, XXREAL_2:def 10;
then consider s being ExtReal such that
A12: ( s in Rx & r < s ) by XXREAL_2:def 1;
consider s0 being Real such that
A13: ( s = s0 & 0 < s0 & [:].(a - s0),(a + s0).[,].(b - s0),(b + s0).[:] c= A ) by A12;
( ].(a - r),(a + r).[ c= ].(a - s0),(a + s0).[ & ].(b - r),(b + r).[ c= ].(b - s0),(b + s0).[ ) by A12, A13, Lm2;
then [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= [:].(a - s0),(a + s0).[,].(b - s0),(b + s0).[:] by ZFMISC_1:96;
hence z in A by A11, A13; :: thesis:

end;

then [:REAL,REAL:] c= A ;
then A14: A = [:REAL,REAL:] ;
REAL in L-Field by PROB_1:5;
then A15: [:REAL,REAL:] in measurable_rectangles (L-Field,L-Field) ;
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
hence A in sigma (measurable_rectangles (L-Field,L-Field)) by A15, A14; :: thesis:

end;

suppose for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } ) ; :: thesis:

then consider F being Function of A,REAL such that
A16: for a, b being Real st [a,b] in A holds
ex Rx being real-membered set st
( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) by Th14;
A /\ [:RAT,RAT:] <> {}

proof

consider z being object such that
A17: z in A by A2, XBOOLE_0:def 1;
reconsider u = z as Point of [:RNS_Real,RNS_Real:] by A17;
consider e0 being Real such that
A18: ( e0 > 0 & Ball (u,e0) c= A ) by A17, A1, NDIFF_8:20;
set e = e0 / 4;
A19: ( 0 < e0 / 4 & e0 / 4 < e0 ) by A18, XREAL_1:223, XREAL_1:224;
then A20: Ball (u,(e0 / 4)) c= Ball (u,e0) by NDIFF_8:15;
A21: (e0 / 4) / 2 < e0 / 4 by A18, XREAL_1:216, XREAL_1:224;
consider x1, y1 being Point of RNS_Real such that
A22: u = [x1,y1] by PRVECT_3:18;
reconsider xx1 = x1, yy1 = y1 as Real ;
( xx1 - ((e0 / 4) / 4) < xx1 & xx1 < xx1 + ((e0 / 4) / 4) ) by A19, XREAL_1:29, XREAL_1:44, XREAL_1:224;
then xx1 - ((e0 / 4) / 4) < xx1 + ((e0 / 4) / 4) by XXREAL_0:2;
then consider qx1 being Rational such that
A23: ( xx1 - ((e0 / 4) / 4) < qx1 & qx1 < xx1 + ((e0 / 4) / 4) ) by RAT_1:7;
( yy1 - ((e0 / 4) / 4) < yy1 & yy1 < yy1 + ((e0 / 4) / 4) ) by A19, XREAL_1:29, XREAL_1:44, XREAL_1:224;
then yy1 - ((e0 / 4) / 4) < yy1 + ((e0 / 4) / 4) by XXREAL_0:2;
then consider qy1 being Rational such that
A24: ( yy1 - ((e0 / 4) / 4) < qy1 & qy1 < yy1 + ((e0 / 4) / 4) ) by RAT_1:7;
( qx1 in ].(xx1 - ((e0 / 4) / 4)),(xx1 + ((e0 / 4) / 4)).[ & qy1 in ].(yy1 - ((e0 / 4) / 4)),(yy1 + ((e0 / 4) / 4)).[ ) by A23, A24;
then A25: ( |.(qx1 - xx1).| < (e0 / 4) / 4 & |.(qy1 - yy1).| < (e0 / 4) / 4 ) by RCOMP_1:1;
reconsider dx1 = qx1, dy1 = qy1 as Point of RNS_Real by XREAL_0:def 1;
reconsider v = [dx1,dy1] as Point of [:RNS_Real,RNS_Real:] ;
- v = [(- dx1),(- dy1)] by PRVECT_3:18;
then u - v = [(x1 + (- dx1)),(y1 + (- dy1))] by A22, PRVECT_3:18;
then ||.(u - v).|| <= ||.(x1 - dx1).|| + ||.(y1 - dy1).|| by NDIFF_9:6;
then ||.(u - v).|| <= ||.(dx1 - x1).|| + ||.(y1 - dy1).|| by NORMSP_1:7;
then A26: ||.(u - v).|| <= ||.(dx1 - x1).|| + ||.(dy1 - y1).|| by NORMSP_1:7;
( dx1 - x1 = qx1 - xx1 & dy1 - y1 = qy1 - yy1 ) by DUALSP03:4;
then ( ||.(dx1 - x1).|| < (e0 / 4) / 4 & ||.(dy1 - y1).|| < (e0 / 4) / 4 ) by A25, EUCLID:def 2;
then ||.(dx1 - x1).|| + ||.(dy1 - y1).|| <= ((e0 / 4) / 4) + ((e0 / 4) / 4) by XREAL_1:7;
then ||.(u - v).|| <= (e0 / 4) / 2 by A26, XXREAL_0:2;
then ||.(u - v).|| < e0 / 4 by XXREAL_0:2, A21;
then v in Ball (u,(e0 / 4)) ;
then A27: [qx1,qy1] in A by A18, A20;
( qx1 in RAT & qy1 in RAT ) by RAT_1:def 2;
then [qx1,qy1] in [:RAT,RAT:] by ZFMISC_1:87;
hence A /\ [:RAT,RAT:] <> {} by A27, XBOOLE_0:def 4; :: thesis:

end;

then consider p being sequence of [:REAL,REAL:] such that
A28: rng p = A /\ [:RAT,RAT:] by Lm3;
A29: for a, b being Real st [a,b] in A holds
ex r being Real st
( 0 < r & r = F . [a,b] & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A )

proof

let a, b be Real; :: thesis:
assume [a,b] in A ; :: thesis:
then consider Rx being real-membered set such that
A30: ( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) } & F . [a,b] = (upper_bound Rx) / 2 ) by A16;
take r0 = F . [a,b]; :: thesis:
consider r1 being Real such that
A31: r1 in Rx by A30;
A32: r1 <= upper_bound Rx by SEQ_4:def 1, A30, A31;
A33: ex r being Real st
( r1 = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) by A30, A31;
then ( 0 < r0 & r0 < upper_bound Rx ) by A30, A32, XREAL_1:215, XREAL_1:216;
then consider s being Real such that
A34: ( s in Rx & (upper_bound Rx) - r0 < s ) by A30, SEQ_4:def 1;
A35: ex r being Real st
( s = r & 0 < r & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) by A34, A30;
( ].(a - r0),(a + r0).[ c= ].(a - s),(a + s).[ & ].(b - r0),(b + r0).[ c= ].(b - s),(b + s).[ ) by A34, A30, Lm2;
then [:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[:] c= [:].(a - s),(a + s).[,].(b - s),(b + s).[:] by ZFMISC_1:96;
hence ( 0 < r0 & r0 = F . [a,b] & [:].(a - r0),(a + r0).[,].(b - r0),(b + r0).[:] c= A ) by A32, A35, A30, A33, XREAL_1:215; :: thesis:

end;

defpred S₁[ object , object ] means ex a, b, r being Real ex E being set st
( p . $1 = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & E = $2 & E = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & E c= A );
A36: for i being object st i in NAT holds
ex y being object st
( y in bool [:REAL,REAL:] & S₁[i,y] )

proof

let i be object ; :: thesis:
assume i in NAT ; :: thesis:
then i in dom p by FUNCT_2:def 1;
then p . i in rng p by FUNCT_1:3;
then A37: ( p . i in A & p . i in [:RAT,RAT:] ) by A28, XBOOLE_0:def 4;
then consider a, b being object such that
A38: ( a in RAT & b in RAT & p . i = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as Real by A38;
consider r being Real such that
A39: ( 0 < r & r = F . [a,b] & [:].(a - r),(a + r).[,].(b - r),(b + r).[:] c= A ) by A29, A37, A38;
set E = [:].(a - r),(a + r).[,].(b - r),(b + r).[:];
take y = [:].(a - r),(a + r).[,].(b - r),(b + r).[:]; :: thesis:
thus y in bool [:REAL,REAL:] ; :: thesis:
thus S₁[i,y] by A38, A39; :: thesis:

end;

consider B being Function of NAT,(bool [:REAL,REAL:]) such that
A40: for i being object st i in NAT holds
S₁[i,B . i] from FUNCT_2:sch 1(A36);
reconsider B = B as SetSequence of [:REAL,REAL:] ;
A41: for i being Element of NAT ex a, b, r being Real st
( p . i = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & B . i c= A )

proof

let i be Element of NAT ; :: thesis:
ex a, b, r being Real ex E being set st
( p . i = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & E = B . i & E = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & E c= A ) by A40;
hence ex a, b, r being Real st
( p . i = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & B . i c= A ) ; :: thesis:

end;

now :: thesis:

let z be object ; :: thesis:
assume z in rng B ; :: thesis:
then consider i being Element of NAT such that
A42: ( i in dom B & z = B . i ) by PARTFUN1:3;
consider a, b, r being Real such that
A43: ( p . i = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & B . i c= A ) by A41;
( ].(a - r),(a + r).[ in L-Field & ].(b - r),(b + r).[ in L-Field ) by MEASUR10:5, MEASUR12:75;
then A44: B . i in measurable_rectangles (L-Field,L-Field) by A43;
measurable_rectangles (L-Field,L-Field) c= sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:def 9;
hence z in sigma (measurable_rectangles (L-Field,L-Field)) by A44, A42; :: thesis:

end;

then rng B c= sigma (measurable_rectangles (L-Field,L-Field)) ;
then reconsider B = B as SetSequence of sigma (measurable_rectangles (L-Field,L-Field)) by RELAT_1:def 19;

now :: thesis:

let z be object ; :: thesis:
assume z in union (rng B) ; :: thesis:
then consider Y being set such that
A45: ( z in Y & Y in rng B ) by TARSKI:def 4;
consider i being Element of NAT such that
A46: ( i in dom B & Y = B . i ) by A45, PARTFUN1:3;
ex a, b, r being Real st
( p . i = [a,b] & a in RAT & b in RAT & 0 < r & r = F . [a,b] & B . i = [:].(a - r),(a + r).[,].(b - r),(b + r).[:] & B . i c= A ) by A41;
hence z in A by A45, A46; :: thesis:

end;

then A47: union (rng B) c= A ;

now :: thesis:

let z be object ; :: thesis:
assume A48: z in A ; :: thesis:
then reconsider u = z as Point of [:RNS_Real,RNS_Real:] ;
consider e0 being Real such that
A49: ( e0 > 0 & Ball (u,e0) c= A ) by A48, A1, NDIFF_8:20;
set e = e0 / 4;
A50: ( 0 < e0 / 4 & e0 / 4 < e0 ) by A49, XREAL_1:223, XREAL_1:224;
then A51: Ball (u,(e0 / 4)) c= Ball (u,e0) by NDIFF_8:15;
consider x1, y1 being Point of RNS_Real such that
A52: u = [x1,y1] by PRVECT_3:18;
reconsider xx1 = x1, yy1 = y1 as Real ;
A53: ( 0 < (e0 / 4) / 2 & (e0 / 4) / 2 < e0 / 4 ) by A50, XREAL_1:215, XREAL_1:216;
( xx1 - ((e0 / 4) / 4) < xx1 & xx1 < xx1 + ((e0 / 4) / 4) ) by A50, XREAL_1:224, XREAL_1:29, XREAL_1:44;
then xx1 - ((e0 / 4) / 4) < xx1 + ((e0 / 4) / 4) by XXREAL_0:2;
then consider qx1 being Rational such that
A54: ( xx1 - ((e0 / 4) / 4) < qx1 & qx1 < xx1 + ((e0 / 4) / 4) ) by RAT_1:7;
qx1 in ].(xx1 - ((e0 / 4) / 4)),(xx1 + ((e0 / 4) / 4)).[ by A54;
then A55: |.(qx1 - xx1).| < (e0 / 4) / 4 by RCOMP_1:1;
( yy1 - ((e0 / 4) / 4) < yy1 & yy1 < yy1 + ((e0 / 4) / 4) ) by A50, XREAL_1:224, XREAL_1:29, XREAL_1:44;
then yy1 - ((e0 / 4) / 4) < yy1 + ((e0 / 4) / 4) by XXREAL_0:2;
then consider qy1 being Rational such that
A56: ( yy1 - ((e0 / 4) / 4) < qy1 & qy1 < yy1 + ((e0 / 4) / 4) ) by RAT_1:7;
qy1 in ].(yy1 - ((e0 / 4) / 4)),(yy1 + ((e0 / 4) / 4)).[ by A56;
then A57: |.(qy1 - yy1).| < (e0 / 4) / 4 by RCOMP_1:1;
reconsider dx1 = qx1, dy1 = qy1 as Point of RNS_Real by XREAL_0:def 1;
reconsider v = [dx1,dy1] as Point of [:RNS_Real,RNS_Real:] ;
- v = [(- dx1),(- dy1)] by PRVECT_3:18;
then u - v = [(x1 + (- dx1)),(y1 + (- dy1))] by A52, PRVECT_3:18;
then ||.(u - v).|| <= ||.(x1 - dx1).|| + ||.(y1 - dy1).|| by NDIFF_9:6;
then ||.(u - v).|| <= ||.(dx1 - x1).|| + ||.(y1 - dy1).|| by NORMSP_1:7;
then A58: ||.(u - v).|| <= ||.(dx1 - x1).|| + ||.(dy1 - y1).|| by NORMSP_1:7;
( dx1 - x1 = qx1 - xx1 & dy1 - y1 = qy1 - yy1 ) by DUALSP03:4;
then ( ||.(dx1 - x1).|| < (e0 / 4) / 4 & ||.(dy1 - y1).|| < (e0 / 4) / 4 ) by A55, A57, EUCLID:def 2;
then ||.(dx1 - x1).|| + ||.(dy1 - y1).|| <= ((e0 / 4) / 4) + ((e0 / 4) / 4) by XREAL_1:7;
then ||.(u - v).|| <= (e0 / 4) / 2 by A58, XXREAL_0:2;
then ||.(u - v).|| < e0 / 4 by XXREAL_0:2, A53;
then A59: v in Ball (u,(e0 / 4)) ;
then A60: [qx1,qy1] in A by A49, A51;
( qx1 in RAT & qy1 in RAT ) by RAT_1:def 2;
then [qx1,qy1] in [:RAT,RAT:] by ZFMISC_1:87;
then [qx1,qy1] in rng p by A28, A60, XBOOLE_0:def 4;
then consider k being Element of NAT such that
A61: ( k in dom p & p . k = [qx1,qy1] ) by PARTFUN1:3;
consider Rx being real-membered set such that
A62: ( not Rx is empty & Rx is bounded_above & Rx = { r where r is Real : ( 0 < r & [:].(qx1 - r),(qx1 + r).[,].(qy1 - r),(qy1 + r).[:] c= A ) } & F . [qx1,qy1] = (upper_bound Rx) / 2 ) by A49, A51, A59, A16;
consider ak, bk, rk being Real such that
A63: ( p . k = [ak,bk] & ak in RAT & bk in RAT & 0 < rk & rk = F . [ak,bk] & B . k = [:].(ak - rk),(ak + rk).[,].(bk - rk),(bk + rk).[:] & B . k c= A ) by A41;
set d = (e0 / 4) / 4;
A64: ( ak = qx1 & bk = qy1 ) by A61, A63, XTUPLE_0:1;
then A65: ( |.(xx1 - ak).| < (e0 / 4) / 4 & |.(yy1 - bk).| < (e0 / 4) / 4 ) by A55, A57, COMPLEX1:60;
then A66: ( x1 in ].(ak - ((e0 / 4) / 4)),(ak + ((e0 / 4) / 4)).[ & y1 in ].(bk - ((e0 / 4) / 4)),(bk + ((e0 / 4) / 4)).[ ) by RCOMP_1:1;

now :: thesis:

let z be object ; :: thesis:
assume z in [:].(ak - ((e0 / 4) / 2)),(ak + ((e0 / 4) / 2)).[,].(bk - ((e0 / 4) / 2)),(bk + ((e0 / 4) / 2)).[:] ; :: thesis:
then consider s, t being object such that
A67: ( s in ].(ak - ((e0 / 4) / 2)),(ak + ((e0 / 4) / 2)).[ & t in ].(bk - ((e0 / 4) / 2)),(bk + ((e0 / 4) / 2)).[ & z = [s,t] ) by ZFMISC_1:def 2;
reconsider s = s, t = t as Real by A67;
reconsider ss = s, tt = t as Point of RNS_Real by XREAL_0:def 1;
reconsider v = [ss,tt] as Point of [:RNS_Real,RNS_Real:] ;
( |.(s - ak).| < (e0 / 4) / 2 & |.(t - bk).| < (e0 / 4) / 2 ) by A67, RCOMP_1:1;
then A68: ( |.(ak - s).| < (e0 / 4) / 2 & |.(bk - t).| < (e0 / 4) / 2 ) by COMPLEX1:60;
((e0 / 4) / 2) / 2 < (e0 / 4) / 2 by A50, XREAL_1:215, XREAL_1:216;
then ( |.(xx1 - ak).| < (e0 / 4) / 2 & |.(yy1 - bk).| < (e0 / 4) / 2 ) by A65, XXREAL_0:2;
then A69: ( |.(xx1 - ak).| + |.(ak - s).| <= ((e0 / 4) / 2) + ((e0 / 4) / 2) & |.(yy1 - bk).| + |.(bk - t).| <= ((e0 / 4) / 2) + ((e0 / 4) / 2) ) by A68, XREAL_1:7;
( |.(xx1 - s).| <= |.(xx1 - ak).| + |.(ak - s).| & |.(yy1 - t).| <= |.(yy1 - bk).| + |.(bk - t).| ) by COMPLEX1:63;
then A70: ( |.(xx1 - s).| <= e0 / 4 & |.(yy1 - t).| <= e0 / 4 ) by A69, XXREAL_0:2;
( x1 - ss = xx1 - s & y1 - tt = yy1 - t ) by DUALSP03:4;
then ( ||.(x1 - ss).|| <= e0 / 4 & ||.(y1 - tt).|| <= e0 / 4 ) by A70, EUCLID:def 2;
then A71: ||.(x1 - ss).|| + ||.(y1 - tt).|| <= (e0 / 4) + (e0 / 4) by XREAL_1:7;
- v = [(- ss),(- tt)] by PRVECT_3:18;
then u - v = [(x1 + (- ss)),(y1 + (- tt))] by A52, PRVECT_3:18;
then ||.(u - v).|| <= ||.(x1 - ss).|| + ||.(y1 - tt).|| by NDIFF_9:6;
then A72: ||.(u - v).|| <= e0 / 2 by A71, XXREAL_0:2;
e0 / 2 < e0 by A49, XREAL_1:216;
then ||.(u - v).|| < e0 by A72, XXREAL_0:2;
then v in Ball (u,e0) ;
hence z in A by A67, A49; :: thesis:

end;

then [:].(ak - ((e0 / 4) / 2)),(ak + ((e0 / 4) / 2)).[,].(bk - ((e0 / 4) / 2)),(bk + ((e0 / 4) / 2)).[:] c= A ;
then (e0 / 4) / 2 in Rx by A53, A62, A64;
then (e0 / 4) / 2 <= upper_bound Rx by A62, SEQ_4:def 1;
then ((e0 / 4) / 2) / 2 <= (upper_bound Rx) / 2 by XREAL_1:72;
then ( ].(ak - ((e0 / 4) / 4)),(ak + ((e0 / 4) / 4)).[ c= ].(ak - rk),(ak + rk).[ & ].(bk - ((e0 / 4) / 4)),(bk + ((e0 / 4) / 4)).[ c= ].(bk - rk),(bk + rk).[ ) by A62, A63, A61, Lm2;
then A73: [x1,y1] in [:].(ak - rk),(ak + rk).[,].(bk - rk),(bk + rk).[:] by A66, ZFMISC_1:87;
k in NAT ;
then k in dom B by FUNCT_2:def 1;
then B . k in rng B by FUNCT_1:3;
hence z in union (rng B) by A63, A52, A73, TARSKI:def 4; :: thesis:

end;

then A c= union (rng B) ;
then Union B = A by A47, CARD_3:def 4;
hence A in sigma (measurable_rectangles (L-Field,L-Field)) by PROB_1:17; :: thesis:

end;