let k be Element of NAT ; :: thesis: for Fy being finite-yielding Function st dom Fy is finite & k = 0 holds
Card_Intersection Fy,k = card (union (rng Fy))
let Fy be finite-yielding Function; :: thesis: ( dom Fy is finite & k = 0 implies Card_Intersection Fy,k = card (union (rng Fy)) )
assume A1: ( dom Fy is finite & k = 0 ) ; :: thesis: Card_Intersection Fy,k = card (union (rng Fy))
then reconsider X = dom Fy as finite set ;
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 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,0 ) and
A5: Card_Intersection Fy,k = Sum XFS by A2, Def4;
card (Choose X,k,0 ,1) = 1 by A1, Th11;
then A6: ( dom P = 1 & 0 in 1 ) by CARD_1:47, CARD_1:87, FUNCT_2:def 1, TARSKI:def 1;
then P . 0 in rng P by FUNCT_1:def 5;
then consider P0 being Function of X,{0 ,1} such that
A7: ( P0 = P . 0 & card (P0 " {0 }) = 0 ) by A1, Def1;
P0 " {0 } = {} by A7;
then A8: ( Intersection Fy,P0,0 = union (rng Fy) & XFS . 0 = card (Intersection Fy,P0,0 ) ) by A3, A4, A6, A7, Th36;
len XFS = 1 by A3, A6;
then ( XFS = <%(XFS . 0 )%> & XFS . 0 = card (Intersection Fy,P0,0 ) ) by A4, A6, A7, AFINSQ_1:38;
then addnat "**" XFS = XFS . 0 by STIRL2_1:44;
hence Card_Intersection Fy,k = card (union (rng Fy)) by A5, A8, STIRL2_1:def 4; :: thesis: verum