let Fy be finite-yielding Function; for x being set st dom Fy is finite & x in dom Fy holds
Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))
let x be set ; ( dom Fy is finite & x in dom Fy implies Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x)) )
assume that
A1:
dom Fy is finite
and
A2:
x in dom Fy
; Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))
reconsider X = dom Fy as finite set by A1;
card X > 0
by A2;
then reconsider k = (card X) - 1 as Element of NAT by NAT_1:20;
set Xx = X \ {x};
A3:
( X \ {x} = {} implies card (X \ {x}) = {} )
;
consider Px being Function of (card (X \ {x})),(X \ {x}) such that
A4:
Px is one-to-one
by Lm2;
not card (X \ {x}) in card (X \ {x})
;
then consider P being Function of ((card (X \ {x})) \/ {(card (X \ {x}))}),((X \ {x}) \/ {x}) such that
A5:
P | (card (X \ {x})) = Px
and
A6:
P . (card (X \ {x})) = x
by A3, STIRL2_1:57;
not x in X \ {x}
by ZFMISC_1:56;
then A7:
P is one-to-one
by A4, A3, A5, A6, STIRL2_1:58;
A8:
card X = Segm (k + 1)
;
then A9:
card (X \ {x}) = Segm k
by A2, STIRL2_1:55;
then
card X = (card (X \ {x})) \/ {(card (X \ {x}))}
by A8, AFINSQ_1:2;
then reconsider P = P as Function of (card X),X by A2, ZFMISC_1:116;
consider XFS being XFinSequence of NAT such that
A10:
dom XFS = card X
and
A11:
for z being set st z in dom XFS holds
XFS . z = card ((Fy * P) . z)
and
A12:
Card_Intersection (Fy,1) = Sum XFS
by A7, Th43;
A13:
P . k = x
by A2, A6, A8, STIRL2_1:55;
X /\ (X \ {x}) = X \ {x}
by XBOOLE_1:28;
then
dom (Fy | (X \ {x})) = X \ {x}
by RELAT_1:61;
then consider XFSx being XFinSequence of NAT such that
A14:
dom XFSx = card (X \ {x})
and
A15:
for z being set st z in dom XFSx holds
XFSx . z = card (((Fy | (X \ {x})) * Px) . z)
and
A16:
Card_Intersection ((Fy | (X \ {x})),1) = Sum XFSx
by A4, Th43;
k < k + 1
by NAT_1:13;
then A17:
Segm k c= Segm (k + 1)
by NAT_1:39;
A18:
for y being object st y in dom XFSx holds
XFS . y = XFSx . y
proof
A19:
(
X \ {x} = X /\ (X \ {x}) &
X /\ (X \ {x}) = dom (Fy | (X \ {x})) )
by RELAT_1:61, XBOOLE_1:28;
let y be
object ;
( y in dom XFSx implies XFS . y = XFSx . y )
assume A20:
y in dom XFSx
;
XFS . y = XFSx . y
A21:
XFS . y = card ((Fy * P) . y)
by A14, A9, A10, A11, A17, A20;
A22:
dom Px = k
by A3, A9, FUNCT_2:def 1;
then
Px . y in rng Px
by A14, A9, A20, FUNCT_1:def 3;
then A23:
(Fy | (X \ {x})) . (Px . y) = Fy . (Px . y)
by A19, FUNCT_1:47;
dom P = k + 1
by CARD_1:27, FUNCT_2:def 1;
then A24:
(Fy * P) . y = Fy . (P . y)
by A14, A9, A17, A20, FUNCT_1:13;
Px . y = P . y
by A14, A5, A9, A20, A22, FUNCT_1:47;
then
(Fy * P) . y = ((Fy | (X \ {x})) * Px) . y
by A14, A9, A20, A22, A24, A23, FUNCT_1:13;
hence
XFS . y = XFSx . y
by A15, A20, A21;
verum
end;
k < k + 1
by NAT_1:13;
then A25:
k in Segm (k + 1)
by NAT_1:44;
then
k in dom P
by CARD_1:27, FUNCT_2:def 1;
then A26:
(Fy * P) . k = Fy . (P . k)
by FUNCT_1:13;
(dom XFS) /\ k = dom XFSx
by A14, A9, A10, A17, XBOOLE_1:28;
then
XFS | k = XFSx
by A18, FUNCT_1:46;
then A27:
(Sum XFSx) + (XFS . k) = Sum (XFS | (k + 1))
by A10, A25, AFINSQ_2:65;
XFS . k = card ((Fy * P) . k)
by A10, A11, A25;
hence
Card_Intersection (Fy,1) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),1)) + (card (Fy . x))
by A16, A10, A12, A27, A26, A13; verum