let k be Nat; :: thesis:
let Fy be finite-yielding Function; :: thesis:
let x, y be set ; :: thesis:
let X be finite set ; :: thesis:
let P be Function of (card (Choose (X,k,x,y))),(Choose (X,k,x,y)); :: thesis:
assume ( dom Fy = X & P is one-to-one & x <> y ) ; :: thesis:
then consider XFS being XFinSequence of NAT such that
A1: dom XFS = dom P and
A2: 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
A3: Card_Intersection (Fy,k) = Sum XFS by Def3;
let XFS1 be XFinSequence of NAT ; :: thesis:
assume that
A4: dom XFS1 = dom P and
A5: for z being set
for f being Function st z in dom XFS1 & f = P . z holds
XFS1 . z = card (Intersection (Fy,f,x)) ; :: thesis:

let z be object ; :: thesis:
assume A6: z in dom XFS ; :: thesis:
P . z in rng P by A1, A6, FUNCT_1:def 3;
then consider Pz being Function of X,{x,y} such that
A7: Pz = P . z and
card (Pz " {x}) = k by Def1;
XFS1 . z = card (Intersection (Fy,Pz,x)) by A4, A5, A1, A6, A7;
hence XFS1 . z = XFS . z by A2, A6, A7; :: thesis:

end;