defpred S₁[ Element of NAT , Subset of X] means $2 = (Cvr . ((pr1 InvPairFunc ) . $1)) . ((pr2 InvPairFunc ) . $1);
A2: for n being Element of NAT ex y being Subset of X st S₁[n,y] ;
consider Seq0 being Function of NAT ,(bool X) such that
A3: for n being Element of NAT holds S₁[n,Seq0 . n] from FUNCT_2:sch 3(A2);
reconsider Seq0 = Seq0 as SetSequence of X ;
for n being Nat holds Seq0 . n in F

proof

let n be Nat; :: thesis: Seq0 . n in F
n in NAT by ORDINAL1:def 13;
then Seq0 . n = (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by A3;
hence Seq0 . n in F ; :: thesis: verum

end;

then reconsider Seq0 = Seq0 as Set_Sequence of F by DDef4;
union (rng Sets) c= union (rng Seq0)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng Sets) or x in union (rng Seq0) )
assume x in union (rng Sets) ; :: thesis: x in union (rng Seq0)
then consider A being set such that
A5: ( x in A & A in rng Sets ) by TARSKI:def 4;
consider n1 being Element of NAT such that
A6: A = Sets . n1 by A5, FUNCT_2:190;
Sets . n1 c= union (rng (Cvr . n1)) by Def2;
then consider AA being set such that
A7: ( x in AA & AA in rng (Cvr . n1) ) by A5, A6, TARSKI:def 4;
consider n2 being Element of NAT such that
A8: AA = (Cvr . n1) . n2 by A7, FUNCT_2:190;
dom PairFunc = rng InvPairFunc by NAGATA_2:2, FUNCT_1:55;
then rng InvPairFunc = [:NAT ,NAT :] by FUNCT_2:def 1;
then [n1,n2] in rng InvPairFunc by ZFMISC_1:def 2;
then consider n being Element of NAT such that
A9: [n1,n2] = InvPairFunc . n by FUNCT_2:190;
[((pr1 InvPairFunc ) . n),((pr2 InvPairFunc ) . n)] = [n1,n2] by A9, FUNCT_2:196;
then ( (pr1 InvPairFunc ) . n = n1 & (pr2 InvPairFunc ) . n = n2 ) by ZFMISC_1:33;
then ( x in Seq0 . n & Seq0 . n in rng Seq0 ) by A3, A7, A8, FUNCT_2:6;
hence x in union (rng Seq0) by TARSKI:def 4; :: thesis: verum

end;

then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def2;
take Seq0 ; :: thesis: for n being Nat holds Seq0 . n = (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n)

hereby :: thesis: verum

let n be Nat; :: thesis: Seq0 . n = (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n)
n in NAT by ORDINAL1:def 13;
hence Seq0 . n = (Cvr . ((pr1 InvPairFunc ) . n)) . ((pr2 InvPairFunc ) . n) by A3; :: thesis: verum

end;