let G be finite set ; :: thesis: card { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } = 2 * (card (PairsOf G))
set Y = union G;
set A = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } ;
set EG = PairsOf G;
set uG = union G;
set s = canFS (PairsOf G);
Aa: len (canFS (PairsOf G)) = card (PairsOf G) by UPROOTS:3;
Ac: rng (canFS (PairsOf G)) = PairsOf G by FUNCT_2:def 3;
defpred S₁[ set , set ] means for a, b being set st $1 = {a,b} holds
$2 = {{a,[b,(union G)]},{b,[a,(union G)]}};
P0: for x, y1, y2 being set st x in PairsOf G & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, v1, v2 be set ; :: thesis: ( x in PairsOf G & S₁[x,v1] & S₁[x,v2] implies v1 = v2 )
assume that
A1: x in PairsOf G and
B1: S₁[x,v1] and
C1: S₁[x,v2] ; :: thesis: v1 = v2
consider x1, y1 being set such that
x1 <> y1 and
x1 in union G and
y1 in union G and
F1: x = {x1,y1} by A1, SG4;
v2 = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by F1, C1;
hence v1 = v2 by F1, B1; :: thesis: verum

end;

P1: for x being set st x in PairsOf G holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in PairsOf G implies ex y being set st S₁[x,y] )
assume x in PairsOf G ; :: thesis: ex y being set st S₁[x,y]
then consider x1, y1 being set such that
x1 <> y1 and
x1 in union G and
y1 in union G and
F1: x = {x1,y1} by SG4;
take y = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}}; :: thesis: S₁[x,y]
let a, b be set ; :: thesis: ( x = {a,b} implies y = {{a,[b,(union G)]},{b,[a,(union G)]}} )
assume x = {a,b} ; :: thesis: y = {{a,[b,(union G)]},{b,[a,(union G)]}}
then ( ( a = x1 & b = y1 ) or ( a = y1 & b = x1 ) ) by F1, ZFMISC_1:6;
hence y = {{a,[b,(union G)]},{b,[a,(union G)]}} ; :: thesis: verum

end;

consider f being Function such that
A: dom f = PairsOf G and
B: for x being set st x in PairsOf G holds
S₁[x,f . x] from FUNCT_1:sch 2(P0, P1);

now :: thesis: for y being set st y in rng (f * (canFS (PairsOf G))) holds
y is finite

let y be set ; :: thesis: ( y in rng (f * (canFS (PairsOf G))) implies y is finite )
assume y in rng (f * (canFS (PairsOf G))) ; :: thesis: y is finite
then y in rng f by FUNCT_1:14;
then consider x being set such that
A1: x in dom f and
B1: y = f . x by FUNCT_1:def 3;
consider x1, y1 being set such that
x1 <> y1 and
x1 in union G and
y1 in union G and
F1: x = {x1,y1} by A1, A, SG4;
y = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by F1, B1, A1, A, B;
hence y is finite ; :: thesis: verum

end;

then reconsider S = f * (canFS (PairsOf G)) as V37() FinSequence by Ac, A, FINSEQ_1:16, FINSET_1:def 2;
Ca: dom S = dom (canFS (PairsOf G)) by Ac, A, RELAT_1:27;
deffunc H₁( set ) -> Element of omega = card (S . $1);
consider L being FinSequence of NAT such that
C: len L = len S and
D: for j being Nat st j in dom L holds
L . j = H₁(j) from FINSEQ_2:sch 1();
Ea: dom S = dom L by C, FINSEQ_3:29;
Eb: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by Ea, D;

now :: thesis: for x, y being set st x <> y holds
not S . x meets S . y

let x, y be set ; :: thesis: ( x <> y implies not S . b₁ meets S . b₂ )
assume A11: x <> y ; :: thesis: not S . b₁ meets S . b₂

per cases ( ( x in dom S & y in dom S ) or not x in dom S or not y in dom S ) ;

suppose that S1x: x in dom S and
S1y: y in dom S ; :: thesis: not S . b₁ meets S . b₂

A1: ( x in dom (canFS (PairsOf G)) & (canFS (PairsOf G)) . x in dom f ) by S1x, FUNCT_1:11;
B1: ( y in dom (canFS (PairsOf G)) & (canFS (PairsOf G)) . y in dom f ) by S1y, FUNCT_1:11;
consider x1, y1 being set such that
x1 <> y1 and
D1x: ( x1 in union G & y1 in union G ) and
E1x: (canFS (PairsOf G)) . x = {x1,y1} by A1, A, SG4;
consider x2, y2 being set such that
x2 <> y2 and
D1y: ( x2 in union G & y2 in union G ) and
E1y: (canFS (PairsOf G)) . y = {x2,y2} by B1, A, SG4;
F1x: S . x = f . ((canFS (PairsOf G)) . x) by S1x, FUNCT_1:12;
F1y: S . y = f . ((canFS (PairsOf G)) . y) by S1y, FUNCT_1:12;
G1x: S . x = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by E1x, F1x, A1, A, B;
G1y: S . y = {{x2,[y2,(union G)]},{y2,[x2,(union G)]}} by E1y, F1y, B1, A, B;
assume S . x meets S . y ; :: thesis: contradiction
then consider a being set such that
Jx: a in S . x and
Jy: a in S . y by XBOOLE_0:3;
Kx: ( a = {x1,[y1,(union G)]} or a = {y1,[x1,(union G)]} ) by Jx, G1x, TARSKI:def 2;
Ky: ( a = {x2,[y2,(union G)]} or a = {y2,[x2,(union G)]} ) by Jy, G1y, TARSKI:def 2;
( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) or ( y1 = x2 & x1 = y2 ) ) by D1x, D1y, Kx, Ky, Aux4;
hence contradiction by E1x, E1y, A11, A1, B1, FUNCT_1:def 4; :: thesis: verum

end;

suppose ( not x in dom S or not y in dom S ) ; :: thesis: S . b₁ misses S . b₂

then ( S . x = {} or S . y = {} ) by FUNCT_1:def 2;
hence S . x misses S . y by XBOOLE_1:65; :: thesis: verum

end;

end;

end;

then Ec: S is disjoint_valued by PROB_2:def 2;
Union S = union (rng S) ;
then E: card (union (rng S)) = Sum L by Ea, Eb, Ec, DIST_1:17;
Fa: dom ((len L) |-> 2) = Seg (len L) by FUNCOP_1:13
.= dom L by FINSEQ_1:def 3 ;

now :: thesis: for j being Nat st j in dom L holds
L . j = ((len L) |-> 2) . j

let j be Nat; :: thesis: ( j in dom L implies L . j = ((len L) |-> 2) . j )
assume A1: j in dom L ; :: thesis: L . j = ((len L) |-> 2) . j
C1: S . j = f . ((canFS (PairsOf G)) . j) by A1, Ea, FUNCT_1:12;
consider x, y being set such that
D1: x <> y and
x in union G and
y in union G and
G1: (canFS (PairsOf G)) . j = {x,y} by SG4, A1, Ea, Ca, Ac, FUNCT_1:3;
H1: f . ((canFS (PairsOf G)) . j) = {{x,[y,(union G)]},{y,[x,(union G)]}} by G1, B, A1, Ea, Ca, Ac, FUNCT_1:3;

I1: now :: thesis: not {x,[y,(union G)]} = {y,[x,(union G)]}

assume {x,[y,(union G)]} = {y,[x,(union G)]} ; :: thesis: contradiction
then ( x = y or x = [x,(union G)] ) by ZFMISC_1:6;
hence contradiction by D1, Aux3; :: thesis: verum

end;

J1: j in Seg (len L) by A1, FINSEQ_1:def 3;
thus L . j = card (S . j) by A1, D
.= 2 by I1, H1, C1, CARD_2:57
.= ((len L) |-> 2) . j by J1, FINSEQ_2:57 ; :: thesis: verum

end;

then F: L = (len L) |-> 2 by Fa, FINSEQ_1:13;
G: len L = card (PairsOf G) by C, Ca, Aa, FINSEQ_3:29;
union (rng S) = { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }

proof

thus union (rng S) c= { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } :: according to XBOOLE_0:def 10 :: thesis: { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } c= union (rng S)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in union (rng S) or a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } )
assume a in union (rng S) ; :: thesis: a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G }
then consider YY being set such that
A1: a in YY and
B1: YY in rng S by TARSKI:def 4;
consider b being set such that
C1: b in dom S and
D1a: YY = S . b by B1, FUNCT_1:def 3;
D1b: S . b = f . ((canFS (PairsOf G)) . b) by C1, FUNCT_1:12;
C1a: (canFS (PairsOf G)) . b in PairsOf G by C1, Ca, Ac, FUNCT_1:3;
consider x, y being set such that
x <> y and
E1: x in union G and
F1: y in union G and
G1: (canFS (PairsOf G)) . b = {x,y} by SG4, C1, Ca, Ac, FUNCT_1:3;
f . ((canFS (PairsOf G)) . b) = {{x,[y,(union G)]},{y,[x,(union G)]}} by G1, B, C1, Ca, Ac, FUNCT_1:3;
then ( a = {x,[y,(union G)]} or a = {y,[x,(union G)]} ) by A1, D1a, D1b, TARSKI:def 2;
hence a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } by G1, C1a, E1, F1; :: thesis: verum

end;

thus { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } c= union (rng S) :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } or a in union (rng S) )
assume a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } ; :: thesis: a in union (rng S)
then consider x, y being Element of union G such that
A1: a = {x,[y,(union G)]} and
B1: {x,y} in PairsOf G ;
consider c being set such that
c in dom (canFS (PairsOf G)) and
D1: (canFS (PairsOf G)) . c = {x,y} by B1, Ac, FUNCT_1:def 3;
rng S = rng f by A, Ac, RELAT_1:28;
then E1: f . ((canFS (PairsOf G)) . c) in rng S by A, D1, B1, FUNCT_1:3;
f . ((canFS (PairsOf G)) . c) = {{x,[y,(union G)]},{y,[x,(union G)]}} by D1, B1, B;
then a in f . ((canFS (PairsOf G)) . c) by A1, TARSKI:def 2;
hence a in union (rng S) by E1, TARSKI:def 4; :: thesis: verum

end;

end;

hence card { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } = 2 * (card (PairsOf G)) by E, F, G, RVSUM_1:80; :: thesis: verum