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 & dom P1 = card (Choose D,k,0 ,1) & 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 A2, FUNCT_2:3;
defpred S₁[ set , set ] means for f being Function st f = P1 . $1 holds
$2 = card (Intersection F,f,0 );
A3: 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] )

proof

let x be set ; :: thesis:
assume A4: x in card (Choose D,k,0 ,1) ; :: thesis:
x in dom P1 by A4, 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
A5: ( f = P1 . x & 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 A5; :: thesis:

end;

consider XFS1 being Function of card (Choose D,k,0 ,1), NAT such that
A6: for x being set st x in card (Choose D,k,0 ,1) holds
S₁[x,XFS1 . x] from FUNCT_2:sch 1(A3);
A7: ( dom XFS1 = card (Choose D,k,0 ,1) & rng XFS1 c= NAT ) by FUNCT_2:def 1;
then reconsider XFS1 = XFS1 as XFinSequence by AFINSQ_1:7;
reconsider XFS1 = XFS1 as XFinSequence of NAT by A7, ORDINAL1:def 8;
take Sum XFS1 ; :: 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
A8: dom F = X and
A9: P is one-to-one and
A10: x <> y ; :: thesis:
set Ch = Choose X,k,x,y;
defpred S₂[ set , set ] means for f being Function st f = P . $1 holds
$2 = card (Intersection F,f,x);
A11: 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 A12: x1 in card (Choose X,k,x,y) ; :: thesis:
x1 in dom P by A12, 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
A13: ( f = P . x1 & 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 A13; :: thesis:

end;

consider XFS being Function of card (Choose X,k,x,y), NAT such that
A14: for x1 being set st x1 in card (Choose X,k,x,y) holds
S₂[x1,XFS . x1] from FUNCT_2:sch 1(A11);
A15: ( dom XFS = card (Choose X,k,x,y) & rng XFS c= NAT ) by FUNCT_2:def 1;
then reconsider XFS = XFS as XFinSequence by AFINSQ_1:7;
reconsider XFS = XFS as XFinSequence of NAT by A15, ORDINAL1:def 8;
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 A16: 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 A14; :: 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 ) ) ) );
A17: 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

let x1 be set ; :: thesis:
assume A18: x1 in card (Choose D,k,0 ,1) ; :: thesis:
P1 . x1 in rng P1 by A2, A18, FUNCT_1:def 5;
then consider f1 being Function of D,{0 ,1} such that
A19: ( f1 = P1 . x1 & 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 ) );
A20: 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 A21: d in X ; :: thesis:
d in dom f1 by A8, A21, FUNCT_2:def 1;
then f1 . d in rng f1 by FUNCT_1:def 5;
then ( ( f1 . d = 0 or f1 . d = 1 ) & 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 A10; :: thesis:

end;

consider f being Function of X,{x,y} such that
A22: for d being set st d in X holds
S₄[d,f . d] from FUNCT_2:sch 1(A20);
A23: f " {x} = f1 " {0 }

proof

A24: ( dom f1 = D & dom f = X ) by FUNCT_2:def 1;
thus f " {x} c= f1 " {0 } :: according to XBOOLE_0:def 10 :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in f " {x} ; :: thesis:
then ( z in dom f & f . z in {x} & dom f1 = dom f ) by A8, A24, FUNCT_1:def 13;
then ( z in dom f1 & f . z = x ) by TARSKI:def 1;
then ( z in dom f1 & f1 . z = 0 ) by A8, A22;
then ( z in dom f1 & f1 . z in {0 } ) by TARSKI:def 1;
hence z in f1 " {0 } by FUNCT_1:def 13; :: thesis:

end;

thus f1 " {0 } c= f " {x} :: thesis:

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in f1 " {0 } ; :: thesis:
then ( z in dom f1 & f1 . z in {0 } & dom f1 = dom f ) by A8, A24, FUNCT_1:def 13;
then ( z in dom f & f1 . z = 0 ) by TARSKI:def 1;
then ( z in dom f & f . z = x ) by A22;
then ( z in dom f & f . z in {x} ) by TARSKI:def 1;
hence z in f " {x} by FUNCT_1:def 13; :: thesis:

end;

card (card (Choose X,k,x,y)) = card (Choose X,k,x,y) ;
then P is onto by A9, STIRL2_1:70;
then ( f in Choose X,k,x,y & rng P = Choose X,k,x,y ) by A19, A23, Def1, FUNCT_2:def 3;
then consider x2 being set such that
A25: ( x2 in dom P & P . x2 = f ) by FUNCT_1:def 5;
take x2 ; :: thesis:
( Choose X,k,x,y = {} implies card (Choose X,k,x,y) = {} ) ;
then ( dom P = card (Choose X,k,x,y) & card (Choose X,k,x,y) = (card X) choose k & card (Choose D,k,0 ,1) = (card D) choose k ) by A10, Th18, FUNCT_2:def 1;
hence x2 in card (Choose D,k,0 ,1) by A8, A25; :: thesis:
let f1' be Function of D,{0 ,1}; :: thesis:
let f' be Function of X,{x,y}; :: thesis:
assume A26: ( f1' = P1 . x1 & f' = P . x2 ) ; :: thesis:
thus f' " {x} = f1' " {0 } by A19, A23, A25, A26; :: thesis:
let z be set ; :: thesis:
assume A27: z in X ; :: thesis:
thus ( ( 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 ) ) by A19, A22, A25, A26, A27; :: thesis:

end;

consider Perm being Function of card (Choose D,k,0 ,1), card (Choose D,k,0 ,1) such that
A28: for x1 being set st x1 in card (Choose D,k,0 ,1) holds
S₃[x1,Perm . x1] from FUNCT_2:sch 1(A17);
A29: ( card (Choose D,k,0 ,1) = (card D) choose k & card (Choose X,k,x,y) = (card X) choose k ) by A10, Th18;
then A30: dom XFS = dom XFS1 by A8, A15, FUNCT_2:def 1;

now

let z1, z2 be set ; :: thesis:
assume A31: ( z1 in dom Perm & z2 in dom Perm & Perm . z1 = Perm . z2 ) ; :: thesis:
P1 . z1 in rng P1 by A2, A31, FUNCT_1:def 5;
then consider P1z1 being Function of D,{0 ,1} such that
A32: ( P1 . z1 = P1z1 & card (P1z1 " {0 }) = k ) by Def1;
P1 . z2 in rng P1 by A2, A31, FUNCT_1:def 5;
then consider P1z2 being Function of D,{0 ,1} such that
A33: ( P1 . z2 = P1z2 & card (P1z2 " {0 }) = k ) by Def1;
( Perm . z1 in rng Perm & Perm . z2 in rng Perm & card (Choose X,k,x,y) = (card X) choose k & card (Choose D,k,0 ,1) = (card D) choose k ) by A10, A31, Th18, FUNCT_1:def 5;
then ( Perm . z1 in card (Choose X,k,x,y) & ( Choose X,k,x,y = {} implies card (Choose X,k,x,y) = {} ) ) by A8;
then Perm . z1 in dom P by 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) & card (PPermz1 " {x}) = k ) by Def1;
P1z1 = P1z2

proof

A35: for z being set st z in dom P1z1 holds
P1z1 . z = P1z2 . z

proof

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

per cases by A37, TARSKI:def 2;

suppose P1z1 . z = 0 ; :: thesis:

then ( P1z1 . z = 0 & PPermz1 . z = x & ( P1z2 . z = 0 implies PPermz1 . z = x ) & ( PPermz1 . z = x implies P1z2 . z = 0 ) ) by A8, A28, A31, A32, A33, A34, A36;
hence P1z1 . z = P1z2 . z ; :: thesis:

end;

suppose P1z1 . z = 1 ; :: thesis:

then ( P1z1 . z = 1 & PPermz1 . z = y & ( P1z2 . z = 1 implies PPermz1 . z = y ) & ( PPermz1 . z = y implies P1z2 . z = 1 ) ) by A8, A28, A31, A32, A33, A34, A36;
hence P1z1 . z = P1z2 . z ; :: thesis:

end;

( dom P1z1 = D & dom P1z2 = D ) by FUNCT_2:def 1;
hence P1z1 = P1z2 by A35, FUNCT_1:9; :: thesis:

end;

hence z1 = z2 by A2, A31, A32, A33, FUNCT_1:def 8; :: thesis:

end;

then ( Perm is one-to-one & card (card (Choose D,k,0 ,1)) = card (card (Choose D,k,0 ,1)) ) by FUNCT_1:def 8;
then ( Perm is one-to-one & Perm is onto & card (Choose D,k,0 ,1) = dom XFS ) by A8, A29, FUNCT_2:def 1, STIRL2_1:70;
then reconsider Perm = Perm as Permutation of dom XFS ;
XFS1 = XFS * Perm

proof

A38: for z being set st z in dom XFS1 holds
XFS1 . z = (XFS * Perm) . z

proof

let z be set ; :: thesis:
assume A39: z in dom XFS1 ; :: thesis:
z in dom Perm by A30, A39, FUNCT_2:67;
then A40: Perm . z in rng Perm by FUNCT_1:def 5;
then P . (Perm . z) in rng P by A16, FUNCT_1:def 5;
then consider p being Function of X,{x,y} such that
A41: ( p = P . (Perm . z) & card (p " {x}) = k ) by Def1;
P1 . z in rng P1 by A2, A7, A39, FUNCT_1:def 5;
then consider p1 being Function of D,{0 ,1} such that
A42: ( p1 = P1 . z & card (p1 " {0 }) = k ) by Def1;
p1 " {0 } = p " {x} by A7, A28, A39, A41, A42;
then ( Intersection F,p1,0 = Intersection F,p,x & XFS1 . z = card (Intersection F,p1,0 ) & XFS . (Perm . z) = card (Intersection F,p,x) & z in dom Perm ) by A6, A7, A14, A15, A39, A40, A41, A42, Th35, FUNCT_2:67;
hence XFS1 . z = (XFS * Perm) . z by 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 A30, RELAT_1:46;
hence XFS1 = XFS * Perm by A38, FUNCT_1:9; :: thesis:

end;

then ( addnat "**" XFS = addnat "**" XFS1 & addnat "**" XFS1 = Sum XFS1 ) by Th48, STIRL2_1:def 4;
hence Sum XFS1 = Sum XFS by STIRL2_1:def 4; :: thesis: