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) )
assume A1: dom Fy = X ; :: thesis: 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
A2: P is one-to-one by Lm3;
x in {x} by TARSKI:def 1;
then 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) and
A5: Card_Intersection Fy,(card X) = Sum XFS by A1, A2, Def4;
( Choose X,(card X),x,{x} = {} implies card (Choose X,(card X),x,{x}) = {} ) ;
then A6: ( card (Choose X,(card X),x,{x}) = 1 & dom P = card (Choose X,(card X),x,{x}) ) by Th12, FUNCT_2:def 1;
then len XFS = 1 by A3;
then XFS = <%(XFS . 0 )%> by AFINSQ_1:38;
then addnat "**" XFS = XFS . 0 by STIRL2_1:44;
then A7: Sum XFS = XFS . 0 by STIRL2_1:def 4;
consider ch being set such that
A8: Choose X,(card X),x,{x} = {ch} by A6, CARD_2:60;
x in {x} by TARSKI:def 1;
then ( X \/ {} = X & 0 in {0 } & 1 = {0 } & {x} <> x ) by CARD_1:87, TARSKI:def 1;
then ( ({} --> {x}) +* (X --> x) in Choose X,(card X),x,{x} & 0 in dom P ) by A6, Th19;
then ( X --> x in Choose X,(card X),x,{x} & P . 0 in rng P ) by FUNCT_1:def 5, FUNCT_4:21;
then ( P . 0 = ch & X --> x = ch & 0 in dom XFS ) by A3, A6, A8, CARD_1:87, TARSKI:def 1;
hence Card_Intersection Fy,(card X) = card (Intersection Fy,(X --> x),x) by A4, A5, A7; :: thesis: verum