reconsider G0 = NAT --> X as Set_Sequence of F by Lm1;
reconsider G = G0 as Element of Funcs NAT ,(bool X) by FUNCT_2:11;
reconsider H = NAT --> G as Function of NAT ,(Funcs NAT ,(bool X)) ;
take H ; :: thesis: for n being Nat holds H . n is Covering of Sets . n,F

hereby :: thesis: verum

let n be Nat; :: thesis: H . n is Covering of Sets . n,F
rng (NAT --> X) = {X} by FUNCOP_1:14;
then X c= union (rng (NAT --> X)) by ZFMISC_1:31;
then A1: Sets . n c= union (rng (NAT --> X)) by XBOOLE_1:1;
n in NAT by ORDINAL1:def 13;
then H . n = NAT --> X by FUNCOP_1:13;
hence H . n is Covering of Sets . n,F by A1, Def3; :: thesis: verum

end;