let x be set ; :: thesis: for X being finite set
for Fy being finite-yielding Function st dom Fy = X holds
Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x)
let X be finite set ; :: thesis: for Fy being finite-yielding Function st dom Fy = X holds
Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x)
let Fy be finite-yielding Function; :: thesis: ( dom Fy = X implies Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x) )
set Ch = Choose X,(card X),x,{x};
consider P being Function of (card (Choose X,(card X),x,{x})),(Choose X,(card X),x,{x}) such that
A1: P is one-to-one by Lm3;
x in {x} by TARSKI:def 1;
then A2: x <> {x} ;
assume dom Fy = X ; :: thesis: Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x)
then consider XFS being XFinSequence of such that
A3: dom XFS = dom P and
A4: ( ( for z being set
for f being Function st z in dom XFS & f = P . z holds
XFS . z = card (Intersection Fy,f,x) ) & Card_Intersection Fy,(card X) = Sum XFS ) by A1, A2, Def4;
A5: card (Choose X,(card X),x,{x}) = 1 by Th12;
then consider ch being set such that
A6: Choose X,(card X),x,{x} = {ch} by CARD_2:60;
x in {x} by TARSKI:def 1;
then ( X \/ {} = X & {x} <> x ) ;
then ({} --> {x}) +* (X --> x) in Choose X,(card X),x,{x} by Th19;
then X --> x in Choose X,(card X),x,{x} by FUNCT_4:21;
then A7: X --> x = ch by A6, TARSKI:def 1;
A8: ( Choose X,(card X),x,{x} = {} implies card (Choose X,(card X),x,{x}) = {} ) ;
then A9: dom P = card (Choose X,(card X),x,{x}) by FUNCT_2:def 1;
then 0 in dom P by A5, CARD_1:87, TARSKI:def 1;
then P . 0 in rng P by FUNCT_1:def 5;
then A10: P . 0 = ch by A6, TARSKI:def 1;
len XFS = 1 by A3, A8, A5, FUNCT_2:def 1;
then XFS = <%(XFS . 0 )%> by AFINSQ_1:38;
then addnat "**" XFS = XFS . 0 by AFINSQ_2:49;
then A11: Sum XFS = XFS . 0 by AFINSQ_2:63;
0 in dom XFS by A3, A5, A9, CARD_1:87, TARSKI:def 1;
hence Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x) by A4, A11, A10, A7; :: thesis: verum