let n1, n2 be Element of NAT ; :: thesis:
assume that
A43: for x, y being set
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 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
A44: for x, y being set
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 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:
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 P being Function such that
A45: ( P is one-to-one & 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 A45, FUNCT_2:3;
consider XFS1 being XFinSequence of such that
A46: dom XFS1 = dom P and
A47: 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
A48: n1 = Sum XFS1 by A43, A45;
consider XFS2 being XFinSequence of such that
A49: dom XFS2 = dom P and
A50: 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
A51: n2 = Sum XFS2 by A44, A45;

now

let z be set ; :: thesis:
assume A52: z in dom XFS1 ; :: thesis:
P . z in rng P by A46, A52, FUNCT_1:def 5;
then consider Pz being Function of D,{0 ,1} such that
A53: ( Pz = P . z & card (Pz " {0 }) = k ) by Def1;
( XFS2 . z = card (Intersection F,Pz,0 ) & XFS1 . z = card (Intersection F,Pz,0 ) ) by A46, A47, A49, A50, A52, A53;
hence XFS2 . z = XFS1 . z ; :: thesis:

end;

hence n1 = n2 by A46, A48, A49, A51, FUNCT_1:9; :: thesis: