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

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;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