let Fy be finite-yielding Function; :: thesis: for X being finite set
for n, k being Element of NAT st dom Fy = X & ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,k,x,y holds
card (Intersection Fy,f,x) = n ) ) holds
Card_Intersection Fy,k = n * ((card X) choose k)
let X be finite set ; :: thesis: for n, k being Element of NAT st dom Fy = X & ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,k,x,y holds
card (Intersection Fy,f,x) = n ) ) holds
Card_Intersection Fy,k = n * ((card X) choose k)
let n, k be Element of NAT ; :: thesis: ( dom Fy = X & ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,k,x,y holds
card (Intersection Fy,f,x) = n ) ) implies Card_Intersection Fy,k = n * ((card X) choose k) )
assume A1: X = dom Fy ; :: thesis: ( for x, y being set holds
( not x <> y or ex f being Function st
( f in Choose X,k,x,y & not card (Intersection Fy,f,x) = n ) ) or Card_Intersection Fy,k = n * ((card X) choose k) )
assume ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,k,x,y holds
card (Intersection Fy,f,x) = n ) ) ; :: thesis: Card_Intersection Fy,k = n * ((card X) choose k)
then consider x, y being set such that
A2: x <> y and
A3: for f being Function st f in Choose X,k,x,y holds
card (Intersection Fy,f,x) = n ;
set Ch = Choose X,k,x,y;
consider P being Function of (card (Choose X,k,x,y)),(Choose X,k,x,y) such that
A4: P is one-to-one by Lm3;
consider XFS being XFinSequence of such that
A5: dom XFS = dom P and
A6: for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection Fy,f,x) and
A7: Card_Intersection Fy,k = Sum XFS by A1, A2, A4, Def4;
for z being set st z in dom XFS holds
XFS . z = n

proof

let z be set ; :: thesis: ( z in dom XFS implies XFS . z = n )
assume A8: z in dom XFS ; :: thesis: XFS . z = n
A9: P . z in rng P by A5, A8, FUNCT_1:def 5;
then consider f being Function of X,{x,y} such that
A10: ( f = P . z & card (f " {x}) = k ) by Def1;
( XFS . z = card (Intersection Fy,f,x) & card (Intersection Fy,f,x) = n ) by A3, A6, A8, A9, A10;
hence XFS . z = n ; :: thesis: verum

end;

then ( XFS = (dom XFS) --> n & n in {n} ) by FUNCOP_1:17, TARSKI:def 1;
then ( XFS " {n} = dom XFS & rng XFS c= {n} & {n} c= {0 ,n} & ( Choose X,k,x,y = {} implies card (Choose X,k,x,y) = {} ) ) by FUNCOP_1:19, FUNCOP_1:20, ZFMISC_1:12;
then ( XFS " {n} = dom P & rng XFS c= {0 ,n} & dom P = card (Choose X,k,x,y) ) by A5, FUNCT_2:def 1, XBOOLE_1:1;
then ( Sum XFS = n * (card (card (Choose X,k,x,y))) & card (Choose X,k,x,y) = (card X) choose k ) by A2, Th18, Th45;
hence Card_Intersection Fy,k = n * ((card X) choose k) by A7; :: thesis: verum