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 A1: { [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 object such that
A2: a in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } ;
consider x, y being Element of union X such that
a = {x,[y,(union X)]} and
A3: {x,y} in PairsOf X by A2;
[x,y] in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by A3;
hence contradiction by A1; :: 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 A1, Th15; :: thesis: verum

end;

suppose A4: 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 object such that
A5: b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } ;
consider x, y being Element of union X such that
b = [x,y] and
A6: {x,y} in PairsOf X by A5;
A7: x in {x,y} by TARSKI:def 2;
A8: union X <> {} by A6, A7, TARSKI:def 4;
defpred S₁[ object , object ] 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];
A9: for c being object st c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } holds
ex d being object 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 object ; :: thesis: ( c in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } implies ex d being object 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 object 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
A10: c = {x,[y,(union X)]} and
A11: {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 A11; :: 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 A12: ( 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 A10, A12, Th4;
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
A13: for c being object 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(A9);
A14: dom f = { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by A4, FUNCT_2:def 1;
A15: f is one-to-one

proof

let c1, c2 be object ; :: 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
A16: c1 in dom f and
A17: c2 in dom f and
A18: f . c1 = f . c2 ; :: thesis: c1 = c2
consider x1, y1 being Element of union X such that
A19: c1 = {x1,[y1,(union X)]} and
{x1,y1} in PairsOf X by A16, A14;
consider x2, y2 being Element of union X such that
A20: c2 = {x2,[y2,(union X)]} and
{x2,y2} in PairsOf X by A17, A14;
A21: f . c1 = [x1,y1] by A13, A16, A14, A8, A19;
A22: f . c2 = [x2,y2] by A13, A17, A14, A8, A20;
( x1 = x2 & y1 = y2 ) by A18, A21, A22, XTUPLE_0:1;
hence c1 = c2 by A19, A20; :: thesis: verum

end;

A23: 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 object ; :: 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 object such that
A24: a in dom f and
A25: b = f . a by FUNCT_1:def 3;
consider x, y being Element of union X such that
A26: a = {x,[y,(union X)]} and
A27: {x,y} in PairsOf X by A24, A14;
A28: b = [x,y] by A25, A24, A13, A14, A8, A26;
thus b in { [x,y] where x, y is Element of union X : {x,y} in PairsOf X } by A28, A27; :: 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 object ; :: 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 A29: 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
A30: b = [x,y] and
A31: {x,y} in PairsOf X by A29;
set a = {x,[y,(union X)]};
A32: {x,[y,(union X)]} in { {x,[y,(union X)]} where x, y is Element of union X : {x,y} in PairsOf X } by A31;
A33: f . {x,[y,(union X)]} = b by A32, A13, A30, A8;
thus b in rng f by A32, A33, A14, FUNCT_1:3; :: thesis: verum

end;

end;

A34: f is onto by A23, 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 A15, A34, A4, EULER_1:11
.= 2 * (card (PairsOf X)) by Th15 ; :: thesis: verum

end;

end;