1 in Seg 1
;
then A1:
(L-Field 1) . 1 = L-Field
by FUNCOP_1:7;
hence
Prod_Field (L-Field 1) = L-Field
by MEASUR13:def 11; ( Borel_Sets c= Prod_Field (L-Field 1) & ( for I being Subset of REAL st I is Interval holds
I in Prod_Field (L-Field 1) ) )
thus
Borel_Sets c= Prod_Field (L-Field 1)
by A1, MEASUR12:75, MEASUR13:def 11; for I being Subset of REAL st I is Interval holds
I in Prod_Field (L-Field 1)
hence
for I being Subset of REAL st I is Interval holds
I in Prod_Field (L-Field 1)
by MEASUR10:5; verum