let X be finite set ; :: thesis: card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))
set Y = union X;
set B = { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } ;
set A = { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } ;

per cases ( { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty or not { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty ) ;

suppose S1: { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty ; :: thesis: card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))

now :: thesis: { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } is empty

assume not { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } is empty ; :: thesis: contradiction
then consider a being set such that
A1: a in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by XBOOLE_0:def 1;
consider x, y being Element of union X such that
a = {x,[y,(union X)]} and
C1: {x,y} in PairsOf X by A1;
[x,y] in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by C1;
hence contradiction by S1; :: thesis: verum

end;

hence card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X)) by S1, MnewE; :: thesis: verum

end;

suppose S1: not { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } is empty ; :: thesis: card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = 2 * (card (PairsOf X))

then consider b being set such that
Aa1: b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by XBOOLE_0:def 1;
consider x, y being Element of union X such that
b = [x,y] and
Ca1: {x,y} in PairsOf X by Aa1;
Ea1: x in {x,y} by TARSKI:def 2;
S1a: union X <> {} by Ca1, Ea1, TARSKI:def 4;
defpred S₁[ set , set ] means for a, b being Element of union X st a in union X & b in union X & $1 = {a,[b,(union X)]} holds
$2 = [a,b];
P: for c being set st c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } holds
ex d being set st
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S₁[c,d] )

proof

let c be set ; :: thesis: ( c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } implies ex d being set st
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S₁[c,d] ) )
assume c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } ; :: thesis: ex d being set st
( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S₁[c,d] )
then consider x, y being Element of union X such that
B2: c = {x,[y,(union X)]} and
C2: {x,y} in PairsOf X ;
take d = [x,y]; :: thesis: ( d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } & S₁[c,d] )
thus d in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by C2; :: thesis: S₁[c,d]
thus S₁[c,d] :: thesis: verum

proof

let a, b be Element of union X; :: thesis: ( a in union X & b in union X & c = {a,[b,(union X)]} implies d = [a,b] )
assume A3: ( a in union X & b in union X ) ; :: thesis: ( not c = {a,[b,(union X)]} or d = [a,b] )
assume c = {a,[b,(union X)]} ; :: thesis: d = [a,b]
then ( a = x & b = y ) by B2, A3, Aux4;
hence d = [a,b] ; :: thesis: verum

end;

end;

consider f being Function of { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } , { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } such that
A1: for c being set st c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } holds
S₁[c,f . c] from FUNCT_2:sch 1(P);
domf: dom f = { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by S1, FUNCT_2:def 1;
B1: f is one-to-one

proof

let c1, c2 be set ; :: according to FUNCT_1:def 4 :: thesis: ( not c1 in dom f or not c2 in dom f or not f . c1 = f . c2 or c1 = c2 )
assume that
A2: c1 in dom f and
B2: c2 in dom f and
C2: f . c1 = f . c2 ; :: thesis: c1 = c2
consider x1, y1 being Element of union X such that
E2: c1 = {x1,[y1,(union X)]} and
{x1,y1} in PairsOf X by A2, domf;
consider x2, y2 being Element of union X such that
G2: c2 = {x2,[y2,(union X)]} and
{x2,y2} in PairsOf X by B2, domf;
I2: f . c1 = [x1,y1] by A1, A2, domf, S1a, E2;
J2: f . c2 = [x2,y2] by A1, B2, domf, S1a, G2;
( x1 = x2 & y1 = y2 ) by C2, I2, J2, XTUPLE_0:1;
hence c1 = c2 by E2, G2; :: thesis: verum

end;

C1a: rng f = { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }

proof

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

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in rng f or b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } )
assume b in rng f ; :: thesis: b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X }
then consider a being set such that
A2: a in dom f and
B2: b = f . a by FUNCT_1:def 3;
consider x, y being Element of union X such that
C2: a = {x,[y,(union X)]} and
D2: {x,y} in PairsOf X by A2, domf;
F2: b = [x,y] by B2, A2, A1, domf, S1a, C2;
thus b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by F2, D2; :: thesis: verum

end;

thus { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } c= rng f :: thesis: verum

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } or b in rng f )
assume A2: b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } ; :: thesis: b in rng f
consider x, y being Element of union X such that
B2: b = [x,y] and
C2: {x,y} in PairsOf X by A2;
set a = {x,[y,(union X)]};
D2: {x,[y,(union X)]} in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by C2;
F2: f . {x,[y,(union X)]} = b by D2, A1, B2, S1a;
thus b in rng f by D2, F2, domf, FUNCT_1:3; :: thesis: verum

end;

end;

C1: f is onto by C1a, FUNCT_2:def 3;
thus card { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } = card { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by B1, C1, S1, EULER_1:11
.= 2 * (card (PairsOf X)) by MnewE ; :: thesis: verum

end;

end;