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);
A1: len (canFS (PairsOf G)) = card (PairsOf G) by FINSEQ_1:93;
A2: rng (canFS (PairsOf G)) = PairsOf G by FUNCT_2:def 3;
defpred S₁[ object , object ] means for a, b being set st $1 = {a,b} holds
$2 = {{a,[b,(union G)]},{b,[a,(union G)]}};
A3: for x, y1, y2 being object st x in PairsOf G & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, v1, v2 be object ; :: thesis: ( x in PairsOf G & S₁[x,v1] & S₁[x,v2] implies v1 = v2 )
assume that
A4: x in PairsOf G and
A5: S₁[x,v1] and
A6: 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
A7: x = {x1,y1} by A4, Th11;
v2 = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by A7, A6;
hence v1 = v2 by A7, A5; :: thesis: verum

end;

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

proof

let x be object ; :: thesis: ( x in PairsOf G implies ex y being object st S₁[x,y] )
assume x in PairsOf G ; :: thesis: ex y being object 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
A9: x = {x1,y1} by Th11;
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 A9, ZFMISC_1:6;
hence y = {{a,[b,(union G)]},{b,[a,(union G)]}} ; :: thesis: verum

end;

consider f being Function such that
A10: dom f = PairsOf G and
A11: for x being object st x in PairsOf G holds
S₁[x,f . x] from FUNCT_1:sch 2(A3, A8);

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 object such that
A12: x in dom f and
A13: 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
A14: x = {x1,y1} by A12, A10, Th11;
y = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by A14, A13, A12, A10, A11;
hence y is finite ; :: thesis: verum

end;

then reconsider S = f * (canFS (PairsOf G)) as finite-yielding FinSequence by A2, A10, FINSEQ_1:16, FINSET_1:def 2;
A15: dom S = dom (canFS (PairsOf G)) by A2, A10, RELAT_1:27;
deffunc H₁( set ) -> Element of NAT = card (S . $1);
consider L being FinSequence of NAT such that
A16: len L = len S and
A17: for j being Nat st j in dom L holds
L . j = H₁(j) from FINSEQ_2:sch 1();
A18: dom S = dom L by A16, FINSEQ_3:29;
A19: for i being Nat st i in dom S holds
( S . i is finite & L . i = card (S . i) ) by A18, A17;

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

let x, y be object ; :: thesis: ( x <> y implies not S . b₁ meets S . b₂ )
assume A20: 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 A21: x in dom S and
A22: y in dom S ; :: thesis: not S . b₁ meets S . b₂

A23: ( x in dom (canFS (PairsOf G)) & (canFS (PairsOf G)) . x in dom f ) by A21, FUNCT_1:11;
A24: ( y in dom (canFS (PairsOf G)) & (canFS (PairsOf G)) . y in dom f ) by A22, FUNCT_1:11;
consider x1, y1 being set such that
x1 <> y1 and
A25: ( x1 in union G & y1 in union G ) and
A26: (canFS (PairsOf G)) . x = {x1,y1} by A23, A10, Th11;
consider x2, y2 being set such that
x2 <> y2 and
A27: ( x2 in union G & y2 in union G ) and
A28: (canFS (PairsOf G)) . y = {x2,y2} by A24, A10, Th11;
A29: S . x = f . ((canFS (PairsOf G)) . x) by A21, FUNCT_1:12;
A30: S . y = f . ((canFS (PairsOf G)) . y) by A22, FUNCT_1:12;
A31: S . x = {{x1,[y1,(union G)]},{y1,[x1,(union G)]}} by A26, A29, A23, A10, A11;
A32: S . y = {{x2,[y2,(union G)]},{y2,[x2,(union G)]}} by A28, A30, A24, A10, A11;
assume S . x meets S . y ; :: thesis: contradiction
then consider a being object such that
A33: a in S . x and
A34: a in S . y by XBOOLE_0:3;
A35: ( a = {x1,[y1,(union G)]} or a = {y1,[x1,(union G)]} ) by A33, A31, TARSKI:def 2;
A36: ( a = {x2,[y2,(union G)]} or a = {y2,[x2,(union G)]} ) by A34, A32, TARSKI:def 2;
( ( x1 = x2 & y1 = y2 ) or ( x1 = y2 & y1 = x2 ) or ( y1 = x2 & x1 = y2 ) ) by A25, A27, A35, A36, Th4;
hence contradiction by A26, A28, A20, A23, A24, 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 ; :: thesis: verum

end;

end;

end;

then A37: S is disjoint_valued by PROB_2:def 2;
Union S = union (rng S) ;
then A38: card (union (rng S)) = Sum L by A18, A19, A37, DIST_1:17;
A39: 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 A40: j in dom L ; :: thesis: L . j = ((len L) |-> 2) . j
A41: S . j = f . ((canFS (PairsOf G)) . j) by A40, A18, FUNCT_1:12;
consider x, y being set such that
A42: x <> y and
x in union G and
y in union G and
A43: (canFS (PairsOf G)) . j = {x,y} by Th11, A40, A18, A15, A2, FUNCT_1:3;
A44: f . ((canFS (PairsOf G)) . j) = {{x,[y,(union G)]},{y,[x,(union G)]}} by A43, A11, A40, A18, A15, A2, FUNCT_1:3;

A45: 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 A42, Th3; :: thesis: verum

end;

A46: j in Seg (len L) by A40, FINSEQ_1:def 3;
thus L . j = card (S . j) by A40, A17
.= 2 by A45, A44, A41, CARD_2:57
.= ((len L) |-> 2) . j by A46, FINSEQ_2:57 ; :: thesis: verum

end;

then A47: L = (len L) |-> 2 by A39;
A48: len L = card (PairsOf G) by A16, A15, A1, 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 object ; :: 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
A49: a in YY and
A50: YY in rng S by TARSKI:def 4;
consider b being object such that
A51: b in dom S and
A52: YY = S . b by A50, FUNCT_1:def 3;
A53: S . b = f . ((canFS (PairsOf G)) . b) by A51, FUNCT_1:12;
A54: (canFS (PairsOf G)) . b in PairsOf G by A51, A15, A2, FUNCT_1:3;
consider x, y being set such that
x <> y and
A55: x in union G and
A56: y in union G and
A57: (canFS (PairsOf G)) . b = {x,y} by Th11, A51, A15, A2, FUNCT_1:3;
f . ((canFS (PairsOf G)) . b) = {{x,[y,(union G)]},{y,[x,(union G)]}} by A57, A11, A51, A15, A2, FUNCT_1:3;
then ( a = {x,[y,(union G)]} or a = {y,[x,(union G)]} ) by A49, A52, A53, TARSKI:def 2;
hence a in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in PairsOf G } by A57, A54, A55, A56; :: 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 object ; :: 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
A58: a = {x,[y,(union G)]} and
A59: {x,y} in PairsOf G ;
consider c being object such that
c in dom (canFS (PairsOf G)) and
A60: (canFS (PairsOf G)) . c = {x,y} by A59, A2, FUNCT_1:def 3;
rng S = rng f by A10, A2, RELAT_1:28;
then A61: f . ((canFS (PairsOf G)) . c) in rng S by A10, A60, A59, FUNCT_1:3;
f . ((canFS (PairsOf G)) . c) = {{x,[y,(union G)]},{y,[x,(union G)]}} by A60, A59, A11;
then a in f . ((canFS (PairsOf G)) . c) by A58, TARSKI:def 2;
hence a in union (rng S) by A61, 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 A38, A47, A48, RVSUM_1:80; :: thesis: verum