let k be Nat; 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; ( dom Fy is finite & k = 0 implies Card_Intersection (Fy,k) = card (union (rng Fy)) )
assume that
A1:
dom Fy is finite
and
A2:
k = 0
; Card_Intersection (Fy,k) = card (union (rng Fy))
reconsider X = dom Fy as finite set by A1;
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
A3:
P is one-to-one
by Lm2;
A4:
card (Choose (X,k,0,1)) = 1
by A2, Th10;
then A5:
dom P = 1
by CARD_1:27, FUNCT_2:def 1;
consider XFS being XFinSequence of NAT such that
A6:
dom XFS = dom P
and
A7:
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
A8:
Card_Intersection (Fy,k) = Sum XFS
by A3, Def3;
len XFS = 1
by A6, A4, CARD_1:27, FUNCT_2:def 1;
then
XFS = <%(XFS . 0)%>
by AFINSQ_1:34;
then A9:
addnat "**" XFS = XFS . 0
by AFINSQ_2:37;
A10:
0 in 1
by CARD_1:49, TARSKI:def 1;
then
P . 0 in rng P
by A5, FUNCT_1:def 3;
then consider P0 being Function of X,{0,1} such that
A11:
P0 = P . 0
and
A12:
card (P0 " {0}) = 0
by A2, Def1;
P0 " {0} = {}
by A12;
then A13:
Intersection (Fy,P0,0) = union (rng Fy)
by Th33;
XFS . 0 = card (Intersection (Fy,P0,0))
by A6, A7, A5, A10, A11;
hence
Card_Intersection (Fy,k) = card (union (rng Fy))
by A8, A13, A9, AFINSQ_2:51; verum