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

now

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

end;

hence Card_Intersection Fy,k = Sum XFS1 by A4, A6, A8, FUNCT_1:9; :: thesis: verum