let Fy be finite-yielding Function; :: thesis:
let X be finite set ; :: thesis:
let n, k be Nat; :: thesis:
assume A1: X = dom Fy ; :: thesis:
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:
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 Lm2;
consider XFS being XFinSequence of NAT 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, Def3;
for z being object st z in dom XFS holds
XFS . z = n

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

end;