reconsider D = dom F as finite set by A1;
set Ch1 = Choose D,k,0 ,1;
card (Choose D,k,0 ,1), Choose D,k,0 ,1 are_equipotent by CARD_1:def 5;
then consider P1 being Function such that
A2: P1 is one-to-one and
A3: dom P1 = card (Choose D,k,0 ,1) and
A4: rng P1 = Choose D,k,0 ,1 by WELLORD2:def 4;
reconsider P1 = P1 as Function of (card (Choose D,k,0 ,1)),(Choose D,k,0 ,1) by A3, A4, FUNCT_2:3;
defpred S₁[ set , set ] means for f being Function st f = P1 . $1 holds
$2 = card (Intersection F,f,0 );
A5: for x being set st x in card (Choose D,k,0 ,1) holds
ex y being set st
( y in NAT & S₁[x,y] )

let x be set ; :: thesis:
assume x in card (Choose D,k,0 ,1) ; :: thesis:
then x in dom P1 by CARD_1:47, FUNCT_2:def 1;
then P1 . x in rng P1 by FUNCT_1:def 5;
then consider f being Function of D,{0 ,1} such that
A6: f = P1 . x and
card (f " {0 }) = k by Def1;
union (rng F) is finite by A1, Th41;
then reconsider I = Intersection F,f,0 as finite set ;
take card I ; :: thesis:
thus ( card I in NAT & S₁[x, card I] ) by A6; :: thesis:

end;

consider XFS1 being Function of (card (Choose D,k,0 ,1)),NAT such that
A7: for x being set st x in card (Choose D,k,0 ,1) holds
S₁[x,XFS1 . x] from FUNCT_2:sch 1(A5);
A8: dom XFS1 = card (Choose D,k,0 ,1) by FUNCT_2:def 1;
then reconsider XFS1 = XFS1 as XFinSequence by AFINSQ_1:7;
reconsider XFS1 = XFS1 as XFinSequence of ;
reconsider S = Sum XFS1 as Element of NAT by ORDINAL1:def 13;
take S ; :: thesis:
let x, y be set ; :: thesis:
let X be finite set ; :: thesis:
let P be Function of (card (Choose X,k,x,y)),(Choose X,k,x,y); :: thesis:
assume that
A9: dom F = X and
A10: P is one-to-one and
A11: x <> y ; :: thesis:
defpred S₂[ set , set ] means for f1 being Function of D,{0 ,1}
for f being Function of X,{x,y} st f1 = P1 . $1 & f = P . $2 holds
( f1 " {0 } = f " {x} & ( for z being set st z in X holds
( ( f1 . z = 0 implies f . z = x ) & ( f . z = x implies f1 . z = 0 ) & ( f1 . z = 1 implies f . z = y ) & ( f . z = y implies f1 . z = 1 ) ) ) );
set Ch = Choose X,k,x,y;
A12: for x1 being set st x1 in card (Choose D,k,0 ,1) holds
ex x2 being set st
( x2 in card (Choose D,k,0 ,1) & S₂[x1,x2] )

proof

card (card (Choose X,k,x,y)) = card (Choose X,k,x,y) ;
then P is onto by A10, STIRL2_1:70;
then A13: rng P = Choose X,k,x,y by FUNCT_2:def 3;
let x1 be set ; :: thesis:
assume x1 in card (Choose D,k,0 ,1) ; :: thesis:
then P1 . x1 in rng P1 by A3, FUNCT_1:def 5;
then consider f1 being Function of D,{0 ,1} such that
A14: f1 = P1 . x1 and
A15: card (f1 " {0 }) = k by Def1;
defpred S₃[ set , set ] means ( ( f1 . $1 = 0 implies $2 = x ) & ( $2 = x implies f1 . $1 = 0 ) & ( f1 . $1 = 1 implies $2 = y ) & ( $2 = y implies f1 . $1 = 1 ) );
A16: for d being set st d in X holds
ex fd being set st
( fd in {x,y} & S₃[d,fd] )

proof

let d be set ; :: thesis:
assume d in X ; :: thesis:
then d in dom f1 by A9, FUNCT_2:def 1;
then f1 . d in rng f1 by FUNCT_1:def 5;
then A17: ( f1 . d = 0 or f1 . d = 1 ) by TARSKI:def 2;
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
hence ex fd being set st
( fd in {x,y} & S₃[d,fd] ) by A11, A17; :: thesis:

end;

consider f being Function of X,{x,y} such that
A18: for d being set st d in X holds
S₃[d,f . d] from FUNCT_2:sch 1(A16);
A19: dom f1 = D by FUNCT_2:def 1;
A20: f1 " {0 } c= f " {x}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: z in f1 " {0 } ; :: thesis:
then f1 . z in {0 } by FUNCT_1:def 13;
then A22: f1 . z = 0 by TARSKI:def 1;
A23: dom f1 = dom f by A9, A19, FUNCT_2:def 1;
then z in dom f by A19, A21;
then f . z = x by A18, A22;
then f . z in {x} by TARSKI:def 1;
hence z in f " {x} by A19, A21, A23, FUNCT_1:def 13; :: thesis:

end;

A24: f " {x} c= f1 " {0 }

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A25: z in f " {x} ; :: thesis:
then f . z in {x} by FUNCT_1:def 13;
then f . z = x by TARSKI:def 1;
then f1 . z = 0 by A18, A25;
then f1 . z in {0 } by TARSKI:def 1;
hence z in f1 " {0 } by A9, A19, A25, FUNCT_1:def 13; :: thesis:

end;

then f " {x} = f1 " {0 } by A20, XBOOLE_0:def 10;
then f in Choose X,k,x,y by A15, Def1;
then consider x2 being set such that
A26: x2 in dom P and
A27: P . x2 = f by A13, FUNCT_1:def 5;
take x2 ; :: thesis:
( card (Choose X,k,x,y) = (card X) choose k & card (Choose D,k,0 ,1) = (card D) choose k ) by A11, Th18;
hence x2 in card (Choose D,k,0 ,1) by A9, A26; :: thesis:
let f19 be Function of D,{0 ,1}; :: thesis:
let f9 be Function of X,{x,y}; :: thesis:
assume A28: ( f19 = P1 . x1 & f9 = P . x2 ) ; :: thesis:
thus f9 " {x} = f19 " {0 } by A14, A24, A20, A27, A28, XBOOLE_0:def 10; :: thesis:
let z be set ; :: thesis:
assume z in X ; :: thesis:
hence ( ( f19 . z = 0 implies f9 . z = x ) & ( f9 . z = x implies f19 . z = 0 ) & ( f19 . z = 1 implies f9 . z = y ) & ( f9 . z = y implies f19 . z = 1 ) ) by A14, A18, A27, A28; :: thesis:

end;

consider Perm being Function of (card (Choose D,k,0 ,1)),(card (Choose D,k,0 ,1)) such that
A29: for x1 being set st x1 in card (Choose D,k,0 ,1) holds
S₂[x1,Perm . x1] from FUNCT_2:sch 1(A12);

now

A30: ( Choose X,k,x,y = {} implies card (Choose X,k,x,y) = {} ) ;
let z1, z2 be set ; :: thesis:
assume that
A31: z1 in dom Perm and
A32: z2 in dom Perm and
A33: Perm . z1 = Perm . z2 ; :: thesis:
( card (Choose X,k,x,y) = (card X) choose k & card (Choose D,k,0 ,1) = (card D) choose k ) by A11, Th18;
then Perm . z1 in card (Choose X,k,x,y) by A9, A31;
then Perm . z1 in dom P by A30, FUNCT_2:def 1;
then P . (Perm . z1) in rng P by FUNCT_1:def 5;
then consider PPermz1 being Function of X,{x,y} such that
A34: PPermz1 = P . (Perm . z1) and
card (PPermz1 " {x}) = k by Def1;
P1 . z2 in rng P1 by A3, A32, FUNCT_1:def 5;
then consider P1z2 being Function of D,{0 ,1} such that
A35: P1 . z2 = P1z2 and
card (P1z2 " {0 }) = k by Def1;
P1 . z1 in rng P1 by A3, A31, FUNCT_1:def 5;
then consider P1z1 being Function of D,{0 ,1} such that
A36: P1 . z1 = P1z1 and
card (P1z1 " {0 }) = k by Def1;
A37: for z being set st z in dom P1z1 holds
P1z1 . z = P1z2 . z

proof

let z be set ; :: thesis:
assume A38: z in dom P1z1 ; :: thesis:
A39: P1z1 . z in rng P1z1 by A38, FUNCT_1:def 5;

per cases by A39, TARSKI:def 2;

suppose A40: P1z1 . z = 0 ; :: thesis:

then PPermz1 . z = x by A9, A29, A31, A36, A34, A38;
hence P1z1 . z = P1z2 . z by A9, A29, A32, A33, A35, A34, A38, A40; :: thesis:

end;

suppose A41: P1z1 . z = 1 ; :: thesis:

then PPermz1 . z = y by A9, A29, A31, A36, A34, A38;
hence P1z1 . z = P1z2 . z by A9, A29, A32, A33, A35, A34, A38, A41; :: thesis:

end;

( dom P1z1 = D & dom P1z2 = D ) by FUNCT_2:def 1;
then P1z1 = P1z2 by A37, FUNCT_1:def 17;
hence z1 = z2 by A2, A3, A31, A32, A36, A35, FUNCT_1:def 8; :: thesis:

end;

then A42: Perm is one-to-one by FUNCT_1:def 8;
card (card (Choose D,k,0 ,1)) = card (card (Choose D,k,0 ,1)) ;
then A43: ( Perm is one-to-one & Perm is onto ) by A42, STIRL2_1:70;
defpred S₃[ set , set ] means for f being Function st f = P . $1 holds
$2 = card (Intersection F,f,x);
A44: for x1 being set st x1 in card (Choose X,k,x,y) holds
ex x2 being set st
( x2 in NAT & S₃[x1,x2] )

proof

let x1 be set ; :: thesis:
assume x1 in card (Choose X,k,x,y) ; :: thesis:
then x1 in dom P by CARD_1:47, FUNCT_2:def 1;
then P . x1 in rng P by FUNCT_1:def 5;
then consider f being Function of X,{x,y} such that
A45: f = P . x1 and
card (f " {x}) = k by Def1;
union (rng F) is finite by A1, Th41;
then reconsider I = Intersection F,f,x as finite set ;
take card I ; :: thesis:
thus ( card I in NAT & S₃[x1, card I] ) by A45; :: thesis:

end;

consider XFS being Function of (card (Choose X,k,x,y)),NAT such that
A46: for x1 being set st x1 in card (Choose X,k,x,y) holds
S₃[x1,XFS . x1] from FUNCT_2:sch 1(A44);
A47: dom XFS = card (Choose X,k,x,y) by FUNCT_2:def 1;
then reconsider XFS = XFS as XFinSequence by AFINSQ_1:7;
reconsider XFS = XFS as XFinSequence of ;
take XFS ; :: thesis:
( Choose X,k,x,y = {} implies card (Choose X,k,x,y) = {} ) ;
then dom P = card (Choose X,k,x,y) by FUNCT_2:def 1;
hence A48: dom XFS = dom P by FUNCT_2:def 1; :: thesis:
hence for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection F,f,x) by A46; :: thesis:
A49: card (Choose D,k,0 ,1) = (card D) choose k by Th18;
A50: card (Choose X,k,x,y) = (card X) choose k by A11, Th18;
then card (Choose D,k,0 ,1) = dom XFS by A9, A49, FUNCT_2:def 1;
then reconsider Perm = Perm as Permutation of (dom XFS) by A43;
A51: dom XFS = dom XFS1 by A9, A47, A49, A50, FUNCT_2:def 1;
A52: for z being set st z in dom XFS1 holds
XFS1 . z = (XFS * Perm) . z

proof

let z be set ; :: thesis:
assume A53: z in dom XFS1 ; :: thesis:
A54: z in dom Perm by A8, A53, FUNCT_2:67;
P . (Perm . z) in rng P by A48, A51, A53, FUNCT_1:def 5;
then consider p being Function of X,{x,y} such that
A56: p = P . (Perm . z) and
card (p " {x}) = k by Def1;
A57: XFS . (Perm . z) = card (Intersection F,p,x) by A46, A47, A51, A53, A56;
P1 . z in rng P1 by A3, A8, A53, FUNCT_1:def 5;
then consider p1 being Function of D,{0 ,1} such that
A58: p1 = P1 . z and
card (p1 " {0 }) = k by Def1;
p1 " {0 } = p " {x} by A8, A29, A53, A56, A58;
then A59: Intersection F,p1,0 = Intersection F,p,x by Th35;
XFS1 . z = card (Intersection F,p1,0 ) by A7, A8, A53, A58;
hence XFS1 . z = (XFS * Perm) . z by A59, A57, A54, FUNCT_1:23; :: thesis:

end;

( rng Perm c= dom XFS & dom Perm = dom XFS ) by FUNCT_2:67;
then dom XFS1 = dom (XFS * Perm) by A51, RELAT_1:46;
then XFS1 = XFS * Perm by A52, FUNCT_1:def 17;
then A60: addnat "**" XFS = addnat "**" XFS1 by AFINSQ_2:57;
addnat "**" XFS1 = Sum XFS1 by AFINSQ_2:63;
hence S = Sum XFS by A60, AFINSQ_2:63; :: thesis: