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 2;
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:1;
defpred S1[ object , object ] means for f being Function st f = P1 . $1 holds
$2 = card (Intersection (F,f,0));
A5: for x being object st x in card (Choose (D,k,0,1)) holds
ex y being object st
( y in NAT & S1[x,y] )
proof
let x be object ; :: thesis: ( x in card (Choose (D,k,0,1)) implies ex y being object st
( y in NAT & S1[x,y] ) )
assume x in card (Choose (D,k,0,1)) ; :: thesis: ex y being object st
( y in NAT & S1[x,y] )
then x in dom P1 by CARD_1:27, FUNCT_2:def 1;
then P1 . x in rng P1 by FUNCT_1:def 3;
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, Th38;
then reconsider I = Intersection (F,f,0) as finite set ;
take card I ; :: thesis: ( card I in NAT & S1[x, card I] )
thus ( card I in NAT & S1[x, card I] ) by A6; :: thesis: verum
end;
consider XFS1 being Function of (card (Choose (D,k,0,1))),NAT such that
A7: for x being object st x in card (Choose (D,k,0,1)) holds
S1[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:5;
reconsider XFS1 = XFS1 as XFinSequence of NAT ;
reconsider S = Sum XFS1 as Element of NAT by ORDINAL1:def 12;
take S ; :: thesis: for x, y being object
for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
let x, y be object ; :: thesis: for X being finite set
for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
let X be finite set ; :: thesis: for P being Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)) st dom F = X & P is one-to-one & x <> y holds
ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
let P be Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)); :: thesis: ( dom F = X & P is one-to-one & x <> y implies ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS ) )
assume that
A9: dom F = X and
A10: P is one-to-one and
A11: x <> y ; :: thesis: ex XFS being XFinSequence of NAT st
( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
defpred S2[ object , object ] 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 object st x1 in card (Choose (D,k,0,1)) holds
ex x2 being object st
( x2 in card (Choose (D,k,0,1)) & S2[x1,x2] )
proof
card (card (Choose (X,k,x,y))) = card (Choose (X,k,x,y)) ;
then P is onto by A10, FINSEQ_4:63;
then A13: rng P = Choose (X,k,x,y) by FUNCT_2:def 3;
let x1 be object ; :: thesis: ( x1 in card (Choose (D,k,0,1)) implies ex x2 being object st
( x2 in card (Choose (D,k,0,1)) & S2[x1,x2] ) )
assume x1 in card (Choose (D,k,0,1)) ; :: thesis: ex x2 being object st
( x2 in card (Choose (D,k,0,1)) & S2[x1,x2] )
then P1 . x1 in rng P1 by A3, FUNCT_1:def 3;
then consider f1 being Function of D,{0,1} such that
A14: f1 = P1 . x1 and
A15: card (f1 " {0}) = k by Def1;
defpred S3[ object , object ] 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 object st d in X holds
ex fd being object st
( fd in {x,y} & S3[d,fd] )
proof
let d be object ; :: thesis: ( d in X implies ex fd being object st
( fd in {x,y} & S3[d,fd] ) )
assume d in X ; :: thesis: ex fd being object st
( fd in {x,y} & S3[d,fd] )
then d in dom f1 by A9, FUNCT_2:def 1;
then f1 . d in rng f1 by FUNCT_1:def 3;
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 object st
( fd in {x,y} & S3[d,fd] ) by A11, A17; :: thesis: verum
end;
consider f being Function of X,{x,y} such that
A18: for d being object st d in X holds
S3[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 object ; :: according to TARSKI:def 3 :: thesis: ( not z in f1 " {0} or z in f " {x} )
assume A21: z in f1 " {0} ; :: thesis: z in f " {x}
then f1 . z in {0} by FUNCT_1:def 7;
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 7; :: thesis: verum
end;
A24: f " {x} c= f1 " {0}
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in f " {x} or z in f1 " {0} )
assume A25: z in f " {x} ; :: thesis: z in f1 " {0}
then f . z in {x} by FUNCT_1:def 7;
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 7; :: thesis: verum
end;
then f " {x} = f1 " {0} by A20;
then f in Choose (X,k,x,y) by A15, Def1;
then consider x2 being object such that
A26: x2 in dom P and
A27: P . x2 = f by A13, FUNCT_1:def 3;
reconsider x2 = x2 as set by TARSKI:1;
take x2 ; :: thesis: ( x2 in card (Choose (D,k,0,1)) & S2[x1,x2] )
( card (Choose (X,k,x,y)) = (card X) choose k & card (Choose (D,k,0,1)) = (card D) choose k ) by A11, Th15;
hence x2 in card (Choose (D,k,0,1)) by A9, A26; :: thesis: S2[x1,x2]
let f19 be Function of D,{0,1}; :: thesis: for f being Function of X,{x,y} st f19 = P1 . x1 & f = P . x2 holds
( f19 " {0} = f " {x} & ( for z being set st z in X holds
( ( f19 . z = 0 implies f . z = x ) & ( f . z = x implies f19 . z = 0 ) & ( f19 . z = 1 implies f . z = y ) & ( f . z = y implies f19 . z = 1 ) ) ) )
let f9 be Function of X,{x,y}; :: thesis: ( f19 = P1 . x1 & f9 = P . x2 implies ( f19 " {0} = f9 " {x} & ( for z being set st z in X holds
( ( 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 ) ) ) ) )
assume A28: ( f19 = P1 . x1 & f9 = P . x2 ) ; :: thesis: ( f19 " {0} = f9 " {x} & ( for z being set st z in X holds
( ( 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 ) ) ) )
thus f9 " {x} = f19 " {0} by A14, A24, A20, A27, A28; :: thesis: for z being set st z in X holds
( ( 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 ) )
let z be set ; :: thesis: ( z in X implies ( ( 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 ) ) )
assume z in X ; :: thesis: ( ( 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 ) )
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: verum
end;
consider Perm being Function of (card (Choose (D,k,0,1))),(card (Choose (D,k,0,1))) such that
A29: for x1 being object st x1 in card (Choose (D,k,0,1)) holds
S2[x1,Perm . x1] from FUNCT_2:sch 1(A12);
now :: thesis: for z1, z2 being object st z1 in dom Perm & z2 in dom Perm & Perm . z1 = Perm . z2 holds
z1 = z2
A30: ( Choose (X,k,x,y) = {} implies card (Choose (X,k,x,y)) = {} ) ;
let z1, z2 be object ; :: thesis: ( z1 in dom Perm & z2 in dom Perm & Perm . z1 = Perm . z2 implies z1 = z2 )
assume that
A31: z1 in dom Perm and
A32: z2 in dom Perm and
A33: Perm . z1 = Perm . z2 ; :: thesis: z1 = z2
A34: card X = card D by A9;
( card (Choose (X,k,x,y)) = (card X) choose k & card (Choose (D,k,0,1)) = (card D) choose k ) by A11, Th15;
then card (Choose (D,k,0,1)) = card (Choose (X,k,x,y)) by A34;
then Perm . z1 in card (Choose (X,k,x,y)) by A31, FUNCT_2:5;
then Perm . z1 in dom P by A30, FUNCT_2:def 1;
then P . (Perm . z1) in rng P by FUNCT_1:def 3;
then consider PPermz1 being Function of X,{x,y} such that
A35: PPermz1 = P . (Perm . z1) and
card (PPermz1 " {x}) = k by Def1;
P1 . z2 in rng P1 by A3, A32, FUNCT_1:def 3;
then consider P1z2 being Function of D,{0,1} such that
A36: P1 . z2 = P1z2 and
card (P1z2 " {0}) = k by Def1;
P1 . z1 in rng P1 by A3, A31, FUNCT_1:def 3;
then consider P1z1 being Function of D,{0,1} such that
A37: P1 . z1 = P1z1 and
card (P1z1 " {0}) = k by Def1;
A38: for z being object st z in dom P1z1 holds
P1z1 . z = P1z2 . z
proof
let z be object ; :: thesis: ( z in dom P1z1 implies P1z1 . z = P1z2 . z )
assume A39: z in dom P1z1 ; :: thesis: P1z1 . z = P1z2 . z
A40: P1z1 . z in rng P1z1 by A39, FUNCT_1:def 3;
per cases ( P1z1 . z = 0 or P1z1 . z = 1 ) by A40, TARSKI:def 2;
suppose A41: P1z1 . z = 0 ; :: thesis: P1z1 . z = P1z2 . z
then PPermz1 . z = x by A9, A29, A31, A37, A35, A39;
hence P1z1 . z = P1z2 . z by A9, A29, A32, A33, A36, A35, A39, A41; :: thesis: verum
end;
suppose A42: P1z1 . z = 1 ; :: thesis: P1z1 . z = P1z2 . z
then PPermz1 . z = y by A9, A29, A31, A37, A35, A39;
hence P1z1 . z = P1z2 . z by A9, A29, A32, A33, A36, A35, A39, A42; :: thesis: verum
end;
end;
end;
( dom P1z1 = D & dom P1z2 = D ) by FUNCT_2:def 1;
then P1z1 = P1z2 by A38;
hence z1 = z2 by A2, A3, A31, A32, A37, A36; :: thesis: verum
end;
then A43: Perm is one-to-one ;
card (card (Choose (D,k,0,1))) = card (card (Choose (D,k,0,1))) ;
then A44: ( Perm is one-to-one & Perm is onto ) by A43, FINSEQ_4:63;
defpred S3[ object , object ] means for f being Function st f = P . $1 holds
$2 = card (Intersection (F,f,x));
A45: for x1 being object st x1 in card (Choose (X,k,x,y)) holds
ex x2 being object st
( x2 in NAT & S3[x1,x2] )
proof
let x1 be object ; :: thesis: ( x1 in card (Choose (X,k,x,y)) implies ex x2 being object st
( x2 in NAT & S3[x1,x2] ) )
assume x1 in card (Choose (X,k,x,y)) ; :: thesis: ex x2 being object st
( x2 in NAT & S3[x1,x2] )
then x1 in dom P by CARD_1:27, FUNCT_2:def 1;
then P . x1 in rng P by FUNCT_1:def 3;
then consider f being Function of X,{x,y} such that
A46: f = P . x1 and
card (f " {x}) = k by Def1;
union (rng F) is finite by A1, Th38;
then reconsider I = Intersection (F,f,x) as finite set ;
take card I ; :: thesis: ( card I in NAT & S3[x1, card I] )
thus ( card I in NAT & S3[x1, card I] ) by A46; :: thesis: verum
end;
consider XFS being Function of (card (Choose (X,k,x,y))),NAT such that
A47: for x1 being object st x1 in card (Choose (X,k,x,y)) holds
S3[x1,XFS . x1] from FUNCT_2:sch 1(A45);
 A48: dom XFS = card (Choose (X,k,x,y)) by FUNCT_2:def 1;
then reconsider XFS = XFS as XFinSequence by AFINSQ_1:5;
reconsider XFS = XFS as XFinSequence of NAT ;
take XFS ; :: thesis: ( dom XFS = dom P & ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
( 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 A49: dom XFS = dom P by FUNCT_2:def 1; :: thesis: ( ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection (F,f,x)) ) & S = Sum XFS )
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 A47; :: thesis: S = Sum XFS
A50: card (Choose (D,k,0,1)) = (card D) choose k by Th15;
A51: card (Choose (X,k,x,y)) = (card X) choose k by A11, Th15;
then card (Choose (D,k,0,1)) = dom XFS by A9, A50, FUNCT_2:def 1;
then reconsider Perm = Perm as Permutation of (dom XFS) by A44;
A52: dom XFS = dom XFS1 by A9, A48, A50, A51, FUNCT_2:def 1;
A53: for z being object st z in dom XFS1 holds
XFS1 . z = (XFS * Perm) . z
proof
let z be object ; :: thesis: ( z in dom XFS1 implies XFS1 . z = (XFS * Perm) . z )
assume A54: z in dom XFS1 ; :: thesis: XFS1 . z = (XFS * Perm) . z
A55: z in dom Perm by A8, A54, FUNCT_2:52;
A56: Perm . z in dom XFS by A52, A54, FUNCT_2:5;
then P . (Perm . z) in rng P by A49, FUNCT_1:def 3;
then consider p being Function of X,{x,y} such that
A57: p = P . (Perm . z) and
card (p " {x}) = k by Def1;
A58: XFS . (Perm . z) = card (Intersection (F,p,x)) by A47, A48, A57, A56;
P1 . z in rng P1 by A3, A8, A54, FUNCT_1:def 3;
then consider p1 being Function of D,{0,1} such that
A59: p1 = P1 . z and
card (p1 " {0}) = k by Def1;
p1 " {0} = p " {x} by A8, A29, A54, A57, A59;
then A60: Intersection (F,p1,0) = Intersection (F,p,x) by Th32;
XFS1 . z = card (Intersection (F,p1,0)) by A7, A8, A54, A59;
hence XFS1 . z = (XFS * Perm) . z by A60, A58, A55, FUNCT_1:13; :: thesis: verum
end;
( rng Perm c= dom XFS & dom Perm = dom XFS ) by FUNCT_2:52;
then dom XFS1 = dom (XFS * Perm) by A52, RELAT_1:27;
then XFS1 = XFS * Perm by A53;
then A61: addnat "**" XFS = addnat "**" XFS1 by AFINSQ_2:45;
addnat "**" XFS1 = Sum XFS1 by AFINSQ_2:51;
hence S = Sum XFS by A61, AFINSQ_2:51; :: thesis: verum