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 Lm2;
consider XFS being XFinSequence of NAT 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, Def3;
Choose (X,k,0,1) is empty by A2, Th9;
then XFS = 0 by A4;
hence Card_Intersection (Fy,k) = 0 by A5; :: thesis: verum