let X be finite set ; :: thesis: for k being Nat
for Fy being finite-yielding Function st dom Fy = X & k > card X holds
Card_Intersection Fy,k = 0
let k be Nat; :: thesis: for Fy being finite-yielding Function st dom Fy = X & k > card X holds
Card_Intersection Fy,k = 0
let Fy be finite-yielding Function; :: thesis: ( dom Fy = X & k > card X implies Card_Intersection Fy,k = 0 )
assume that
A1: dom Fy = X and
A2: k > card X ; :: thesis: Card_Intersection Fy,k = 0
set Ch = Choose X,k,0 ,1;
consider P being Function of (card (Choose X,k,0 ,1)),(Choose X,k,0 ,1) such that
A3: P is one-to-one by Lm3;
consider XFS being XFinSequence of such that
A4: dom XFS = dom P and
for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection Fy,f,0 ) and
A5: Card_Intersection Fy,k = Sum XFS by A1, A3, Def4;
Choose X,k,0 ,1 is empty by A2, Th10;
then XFS = 0 by A4;
hence Card_Intersection Fy,k = 0 by A5; :: thesis: verum