deffunc H₁( Nat) -> Element of bool REAL = In ([.(- $1),$1.],(bool REAL));
consider E being Function of NAT,(bool REAL) such that
A1: for i being Element of NAT holds E . i = H₁(i) from FUNCT_2:sch 4();
reconsider E = E as SetSequence of REAL ;
A2: for n being Nat holds E . n = [.(- n),n.]

proof

let n be Nat; :: thesis: E . n = [.(- n),n.]
n is Element of NAT by ORDINAL1:def 12;
then E . n = In ([.(- n),n.],(bool REAL)) by A1;
hence E . n = [.(- n),n.] ; :: thesis: verum

end;

for n being Nat holds E . n in Borel_Sets

proof

let n be Nat; :: thesis: E . n in Borel_Sets
E . n = [.(- n),n.] by A2;
hence E . n in Borel_Sets by MEASUR10:5; :: thesis: verum

end;

then reconsider E = E as Set_Sequence of Borel_Sets by MEASURE8:def 2;
A3: for n being Nat holds B-Meas . (E . n) < +infty

proof

let n be Nat; :: thesis: B-Meas . (E . n) < +infty
- n in INT by INT_1:def 1;
then ( - n in REAL & n in REAL ) by ORDINAL1:def 12, NUMBERS:15, NUMBERS:19;
then reconsider a = - n, b = n as R_eal by NUMBERS:31;
E . n = [.a,b.] by A2;
then B-Meas . (E . n) = diameter [.a,b.] by MEASUR12:71;
then B-Meas . (E . n) = b - a by MEASURE5:6;
hence B-Meas . (E . n) < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

now :: thesis: for z being object st z in REAL holds
z in union (rng E)

let z be object ; :: thesis: ( z in REAL implies z in union (rng E) )
assume z in REAL ; :: thesis: z in union (rng E)
then reconsider r = z as Real ;
consider n being Nat such that
A4: |.r.| < n by SEQ_4:3;
( - n <= r & r <= n ) by ABSVALUE:5, A4;
then r in [.(- n),n.] ;
then A5: r in E . n by A2;
dom E = NAT by FUNCT_2:def 1;
then E . n in rng E by FUNCT_1:3, ORDINAL1:def 12;
hence z in union (rng E) by A5, TARSKI:def 4; :: thesis: verum

end;

then REAL c= union (rng E) ;
then Union E = REAL by CARD_3:def 4;
hence B-Meas is sigma_finite by A3, MEASUR11:def 12; :: thesis: verum