reconsider D = dom F as finite set by A1;
let n1, n2 be Element of NAT ; :: 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)) ) & n1 = Sum XFS ) ) & ( 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)) ) & n2 = Sum XFS ) ) implies n1 = n2 )
assume that
A62: 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)) ) & n1 = Sum XFS ) and
A63: 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)) ) & n2 = Sum XFS ) ; :: thesis: n1 = n2
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 P being Function such that
A64: P is one-to-one and
A65: ( dom P = card (Choose (D,k,0,1)) & rng P = Choose (D,k,0,1) ) by WELLORD2:def 4;
reconsider P = P as Function of (card (Choose (D,k,0,1))),(Choose (D,k,0,1)) by A65, FUNCT_2:1;
consider XFS1 being XFinSequence of NAT such that
A66: dom XFS1 = dom P and
A67: for z being set
for f being Function st z in dom XFS1 & f = P . z holds
XFS1 . z = card (Intersection (F,f,0)) and
A68: n1 = Sum XFS1 by A62, A64;
consider XFS2 being XFinSequence of NAT such that
A69: dom XFS2 = dom P and
A70: for z being set
for f being Function st z in dom XFS2 & f = P . z holds
XFS2 . z = card (Intersection (F,f,0)) and
A71: n2 = Sum XFS2 by A63, A64;
now :: thesis: for z being object st z in dom XFS1 holds
XFS2 . z = XFS1 . z
let z be object ; :: thesis: ( z in dom XFS1 implies XFS2 . z = XFS1 . z )
assume A72: z in dom XFS1 ; :: thesis: XFS2 . z = XFS1 . z
P . z in rng P by A66, A72, FUNCT_1:def 3;
then consider Pz being Function of D,{0,1} such that
A73: Pz = P . z and
card (Pz " {0}) = k by Def1;
XFS2 . z = card (Intersection (F,Pz,0)) by A66, A69, A70, A72, A73;
hence XFS2 . z = XFS1 . z by A67, A72, A73; :: thesis: verum
end;
hence n1 = n2 by A66, A68, A69, A71, FUNCT_1:2; :: thesis: verum