defpred S_{1}[ 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_{1}[n,y]
;

consider Seq0 being sequence of (bool X) such that

A2: for n being Element of NAT holds S_{1}[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

union (rng Sets) c= union (rng Seq0)

take Seq0 ; :: thesis: for n being Nat holds Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n)

A1: for n being Element of NAT ex y being Subset of X st S

consider Seq0 being sequence of (bool X) such that

A2: for n being Element of NAT holds S

reconsider Seq0 = Seq0 as SetSequence of X ;

for n being Nat holds Seq0 . n in F

proof

then reconsider Seq0 = Seq0 as Set_Sequence of F by Def2;
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;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

union (rng Sets) c= union (rng Seq0)

proof

then reconsider Seq0 = Seq0 as Covering of union (rng Sets),F by Def3;
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;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

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;n in NAT by ORDINAL1:def 12;

hence Seq0 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A2; :: thesis: verum