defpred S1[ 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 S1[n,y]
;
consider Seq0 being sequence of (bool X) such that
A2:
for n being Element of NAT holds S1[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
then reconsider Seq0 = Seq0 as Set_Sequence of F by Def2;
union (rng Sets) c= union (rng Seq0)
proof
let x be
object ;
TARSKI:def 3 ( not x in union (rng Sets) or x in union (rng Seq0) )
assume
x in union (rng Sets)
;
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;
verum
end;
then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def3;
take
Seq0
; for n being Nat holds Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)