let X be finite set ; :: thesis: for Fy being finite-yielding Function
for x being object st dom Fy = X holds
Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))
let Fy be finite-yielding Function; :: thesis: for x being object st dom Fy = X holds
Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))
let x be object ; :: 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 Lm2;
S: x in {x} by TARSKI:def 1;
then reconsider x = x as set ;
not x in x ;
then A2: x <> {x} by S;
assume dom Fy = X ; :: thesis: Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x))
then consider XFS being XFinSequence of NAT 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, Def3;
A5: card (Choose (X,(card X),x,{x})) = 1 by Th11;
then consider ch being object such that
A6: Choose (X,(card X),x,{x}) = {ch} by CARD_2:42;
x in {x} by TARSKI:def 1;
then ( X \/ {} = X & {x} <> x ) ;
then ({} --> {x}) +* (X --> x) in Choose (X,(card X),x,{x}) by Th16;
then {} +* (X --> x) in Choose (X,(card X),x,{x}) ;
then X --> x in Choose (X,(card X),x,{x}) ;
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:49, TARSKI:def 1;
then P . 0 in rng P by FUNCT_1:def 3;
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:34;
then addnat "**" XFS = XFS . 0 by AFINSQ_2:37;
then A11: Sum XFS = XFS . 0 by AFINSQ_2:51;
0 in dom XFS by A3, A5, A9, CARD_1:49, TARSKI:def 1;
hence Card_Intersection (Fy,(card X)) = card (Intersection (Fy,(X --> x),x)) by A4, A11, A10, A7; :: thesis: verum