reconsider G = G0 as Element of Funcs (NAT,(bool REAL)) by FUNCT_2:8;
reconsider H = NAT --> G as sequence of (Funcs (NAT,(bool REAL))) ;
for n being Element of NAT holds H . n is Interval_Covering of F . n by Lm8;
then reconsider H = H as Interval_Covering of F by MEASURE7:def 3;
take H ; :: thesis: for n being Element of NAT holds H . n is Open_Interval_Covering of F . n
thus for n being Element of NAT holds H . n is Open_Interval_Covering of F . n by Lm8; :: thesis: verum