reconsider G0 = NAT --> X as Set_Sequence of F by Lm1;
reconsider G = G0 as Element of Funcs (NAT,(bool X)) by FUNCT_2:8;
reconsider H = NAT --> G as sequence of (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:8;
then X c= union (rng (NAT --> X)) by ZFMISC_1:25;
then A1: Sets . n c= union (rng (NAT --> X)) ;
n in NAT by ORDINAL1:def 12;
then H . n = NAT --> X by FUNCOP_1:7;
hence H . n is Covering of Sets . n,F by A1, Def3; :: thesis: verum
end;