let X be finite set ; :: thesis: for k being Element of NAT
for Fy being finite-yielding Function st dom Fy = X & k > card X holds
Card_Intersection Fy,k = 0
let k be Element of 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 A1: ( dom Fy = X & 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
A2: P is one-to-one by Lm3;
consider XFS being XFinSequence of NAT such that
A3: 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
A4: Card_Intersection Fy,k = Sum XFS by A1, A2, Def4;
Choose X,k,0 ,1 is empty by A1, Th10;
then dom P = {} by CARD_1:47;
then XFS = 0 by A3;
hence Card_Intersection Fy,k = 0 by A4, CARD_1:47, STIRL2_1:53; :: thesis: verum