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))) ;
take H ; :: thesis: for n being Element of NAT holds H . n is Interval_Covering of F . n
A1: for n being Element of NAT holds G0 is Interval_Covering of F . n by Lm2, XBOOLE_1:1, Def2, Lm3;
for n being Element of NAT holds H . n is Interval_Covering of F . n
proof
let n be Element of NAT ; :: thesis: H . n is Interval_Covering of F . n
H . n = G by FUNCOP_1:7;
hence H . n is Interval_Covering of F . n by A1; :: thesis: verum
end;
hence for n being Element of NAT holds H . n is Interval_Covering of F . n ; :: thesis: verum