defpred S₁[ Element of NAT , Subset of X] means $2 = (Cvr . ((pr1 InvPairFunc) . $1)) . ((pr2 InvPairFunc) . $1);
A1: for n being Element of NAT ex y being Subset of X st S₁[n,y] ;
consider Seq0 being sequence of (bool X) such that
A2: for n being Element of NAT holds S₁[n,Seq0 . n] from FUNCT_2:sch 3(A1);
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 12;
then Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2;
hence Seq0 . n in F ; :: thesis: verum

end;

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

proof

let x be object ; :: 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
A3: x in A and
A4: A in rng Sets by TARSKI:def 4;
consider n1 being Element of NAT such that
A5: A = Sets . n1 by A4, FUNCT_2:113;
Sets . n1 c= union (rng (Cvr . n1)) by Def3;
then consider AA being set such that
A6: x in AA and
A7: AA in rng (Cvr . n1) by A3, A5, TARSKI:def 4;
consider n2 being Element of NAT such that
A8: AA = (Cvr . n1) . n2 by A7, FUNCT_2:113;
dom PairFunc = rng InvPairFunc by FUNCT_1:33, NAGATA_2:2;
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:113;
[((pr1 InvPairFunc) . n),((pr2 InvPairFunc) . n)] = [n1,n2] by A9, FUNCT_2:119;
then ( (pr1 InvPairFunc) . n = n1 & (pr2 InvPairFunc) . n = n2 ) by XTUPLE_0:1;
then A10: x in Seq0 . n by A2, A6, A8;
Seq0 . n in rng Seq0 by FUNCT_2:4;
hence x in union (rng Seq0) by A10, TARSKI:def 4; :: thesis: verum

end;

then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def3;
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 12;
hence Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2; :: thesis: verum

end;