let k be Nat; for Fy being finite-yielding Function
for X being finite set
for x being set
for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
let Fy be finite-yielding Function; for X being finite set
for x being set
for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
let X be finite set ; for x being set
for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
let x be set ; for n being Nat st dom Fy = X & x in dom Fy & k > 0 holds
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
let n be Nat; ( dom Fy = X & x in dom Fy & k > 0 implies Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k)) )
assume that
A1:
dom Fy = X
and
A2:
x in dom Fy
and
A3:
k > 0
; Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
set Xx = X \ {x};
A4:
(X \ {x}) \/ {x} = X
by A1, A2, ZFMISC_1:116;
set I = Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)));
set X1 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 1 ) } ;
set X0 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 0 ) } ;
{ f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 0 ) } \/ { f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 1 ) } = Choose (((X \ {x}) \/ {x}),(k + 1),1,0)
by Lm1;
then reconsider X0 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 0 ) } , X1 = { f where f is Function of ((X \ {x}) \/ {x}),{1,0} : ( card (f " {1}) = k + 1 & f . x = 1 ) } as finite set by FINSET_1:1, XBOOLE_1:7;
consider P1 being Function of (card X1),X1 such that
A5:
P1 is one-to-one
by Lm2;
not x in X \ {x}
by ZFMISC_1:56;
then A6:
card (Choose ((X \ {x}),k,1,0)) = card X1
by Th12;
defpred S1[ object , object ] means ex f being Function st
( f = P1 . $1 & f in X1 & $2 = f | (X \ {x}) );
A7:
for x1 being object st x1 in card X1 holds
ex P1x1 being object st
( P1x1 in Choose ((X \ {x}),k,1,0) & S1[x1,P1x1] )
proof
not
x in X \ {x}
by ZFMISC_1:56;
then A8:
((X \ {x}) \/ {x}) \ {x} = X \ {x}
by ZFMISC_1:117;
let x1 be
object ;
( x1 in card X1 implies ex P1x1 being object st
( P1x1 in Choose ((X \ {x}),k,1,0) & S1[x1,P1x1] ) )
assume
x1 in card X1
;
ex P1x1 being object st
( P1x1 in Choose ((X \ {x}),k,1,0) & S1[x1,P1x1] )
then
x1 in dom P1
by CARD_1:27, FUNCT_2:def 1;
then A9:
P1 . x1 in rng P1
by FUNCT_1:def 3;
then
P1 . x1 in X1
;
then consider P1x1 being
Function of
((X \ {x}) \/ {x}),
{1,0} such that A10:
P1 . x1 = P1x1
and A11:
card (P1x1 " {1}) = k + 1
and A12:
P1x1 . x = 1
;
A13:
dom P1x1 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
A14:
rng (P1x1 | (X \ {x})) c= {1,0}
;
((X \ {x}) \/ {x}) /\ (X \ {x}) = X \ {x}
by XBOOLE_1:7, XBOOLE_1:28;
then
dom (P1x1 | (X \ {x})) = X \ {x}
by A13, RELAT_1:61;
then reconsider Px =
P1x1 | (X \ {x}) as
Function of
(X \ {x}),
{1,0} by A14, FUNCT_2:2;
A15:
not
x in Px " {1}
by ZFMISC_1:56;
(
x in {x} &
dom P1x1 = (X \ {x}) \/ {x} )
by FUNCT_2:def 1, TARSKI:def 1;
then
x in dom P1x1
by XBOOLE_0:def 3;
then
P1x1 " {1} = (Px " {1}) \/ {x}
by A12, A13, A8, AFINSQ_2:66;
then
k + 1
= (card (Px " {1})) + 1
by A11, A15, CARD_2:41;
then
Px in Choose (
(X \ {x}),
k,1,
0)
by Def1;
hence
ex
P1x1 being
object st
(
P1x1 in Choose (
(X \ {x}),
k,1,
0) &
S1[
x1,
P1x1] )
by A9, A10;
verum
end;
consider P1x being Function of (card X1),(Choose ((X \ {x}),k,1,0)) such that
A16:
for x1 being object st x1 in card X1 holds
S1[x1,P1x . x1]
from FUNCT_2:sch 1(A7);
for x1, x2 being object st x1 in dom P1x & x2 in dom P1x & P1x . x1 = P1x . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom P1x & x2 in dom P1x & P1x . x1 = P1x . x2 implies x1 = x2 )
assume that A17:
x1 in dom P1x
and A18:
x2 in dom P1x
and A19:
P1x . x1 = P1x . x2
;
x1 = x2
consider f2 being
Function such that A20:
f2 = P1 . x2
and A21:
f2 in X1
and A22:
P1x . x2 = f2 | (X \ {x})
by A16, A18;
consider f1 being
Function such that A23:
f1 = P1 . x1
and A24:
f1 in X1
and A25:
P1x . x1 = f1 | (X \ {x})
by A16, A17;
A26:
ex
F being
Function of
((X \ {x}) \/ {x}),
{1,0} st
(
f1 = F &
card (F " {1}) = k + 1 &
F . x = 1 )
by A24;
then A27:
dom f1 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
A28:
ex
F being
Function of
((X \ {x}) \/ {x}),
{1,0} st
(
f2 = F &
card (F " {1}) = k + 1 &
F . x = 1 )
by A21;
then A29:
dom f2 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
for
z being
object st
z in dom f1 holds
f1 . z = f2 . z
then A33:
f1 = f2
by A27, A29;
(
X1 = {} implies
card X1 = {} )
;
then
dom P1 = card X1
by FUNCT_2:def 1;
hence
x1 = x2
by A5, A17, A18, A23, A20, A33;
verum
end;
then A34:
P1x is one-to-one
;
(X \ {x}) /\ X = X \ {x}
by XBOOLE_1:28;
then A35:
dom (Fy | ((dom Fy) \ {x})) = X \ {x}
by A1, RELAT_1:61;
then
dom (Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))) = X \ {x}
by A1, Th48;
then consider XFS1 being XFinSequence of NAT such that
A36:
dom XFS1 = dom P1x
and
A37:
for z being set
for f being Function st z in dom XFS1 & f = P1x . z holds
XFS1 . z = card (Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),f,1))
and
A38:
Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k) = Sum XFS1
by A6, A34, Def3;
A39:
addnat "**" XFS1 = Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k)
by A38, AFINSQ_2:51;
not x in X \ {x}
by ZFMISC_1:56;
then A40:
card (Choose ((X \ {x}),(k + 1),1,0)) = card X0
by Th13;
set Ch = Choose (X,(k + 1),1,0);
consider P0 being Function of (card X0),X0 such that
A41:
P0 is one-to-one
by Lm2;
A42:
( X1 = {} implies card X1 = {} )
;
then A43:
dom P1 = card X1
by FUNCT_2:def 1;
A44:
( X0 = {} implies card X0 = {} )
;
then
dom P0 = card X0
by FUNCT_2:def 1;
then reconsider XP0 = P0, XP1 = P1 as XFinSequence by A43, AFINSQ_1:5;
A45:
card X0 = len XP0
by A44, FUNCT_2:def 1;
defpred S2[ object , object ] means ex f being Function st
( f = P0 . $1 & f in X0 & $2 = f | (X \ {x}) );
A46:
for x0 being object st x0 in card X0 holds
ex P0x0 being object st
( P0x0 in Choose ((X \ {x}),(k + 1),1,0) & S2[x0,P0x0] )
proof
let x0 be
object ;
( x0 in card X0 implies ex P0x0 being object st
( P0x0 in Choose ((X \ {x}),(k + 1),1,0) & S2[x0,P0x0] ) )
assume
x0 in card X0
;
ex P0x0 being object st
( P0x0 in Choose ((X \ {x}),(k + 1),1,0) & S2[x0,P0x0] )
then
x0 in dom P0
by CARD_1:27, FUNCT_2:def 1;
then A47:
P0 . x0 in rng P0
by FUNCT_1:def 3;
then
P0 . x0 in X0
;
then consider P0x0 being
Function of
((X \ {x}) \/ {x}),
{1,0} such that A48:
P0 . x0 = P0x0
and A49:
card (P0x0 " {1}) = k + 1
and A50:
P0x0 . x = 0
;
A51:
dom P0x0 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
A52:
rng (P0x0 | (X \ {x})) c= {1,0}
;
((X \ {x}) \/ {x}) /\ (X \ {x}) = X \ {x}
by XBOOLE_1:7, XBOOLE_1:28;
then
dom (P0x0 | (X \ {x})) = X \ {x}
by A51, RELAT_1:61;
then reconsider Px =
P0x0 | (X \ {x}) as
Function of
(X \ {x}),
{1,0} by A52, FUNCT_2:2;
not
x in X \ {x}
by ZFMISC_1:56;
then
((X \ {x}) \/ {x}) \ {x} = X \ {x}
by ZFMISC_1:117;
then
P0x0 " {1} = Px " {1}
by A50, A51, AFINSQ_2:67;
then
Px in Choose (
(X \ {x}),
(k + 1),1,
0)
by A49, Def1;
hence
ex
P0x0 being
object st
(
P0x0 in Choose (
(X \ {x}),
(k + 1),1,
0) &
S2[
x0,
P0x0] )
by A47, A48;
verum
end;
consider P0x being Function of (card X0),(Choose ((X \ {x}),(k + 1),1,0)) such that
A53:
for x1 being object st x1 in card X0 holds
S2[x1,P0x . x1]
from FUNCT_2:sch 1(A46);
(rng P0) \/ (rng P1) c= X0 \/ X1
by XBOOLE_1:13;
then
rng (XP0 ^ XP1) c= X0 \/ X1
by AFINSQ_1:26;
then A54:
rng (XP0 ^ XP1) c= Choose (X,(k + 1),1,0)
by A4, Lm1;
A55:
card X1 = len XP1
by A42, FUNCT_2:def 1;
for x1, x2 being object st x1 in dom P0x & x2 in dom P0x & P0x . x1 = P0x . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in dom P0x & x2 in dom P0x & P0x . x1 = P0x . x2 implies x1 = x2 )
assume that A56:
x1 in dom P0x
and A57:
x2 in dom P0x
and A58:
P0x . x1 = P0x . x2
;
x1 = x2
consider f2 being
Function such that A59:
f2 = P0 . x2
and A60:
f2 in X0
and A61:
P0x . x2 = f2 | (X \ {x})
by A53, A57;
consider f1 being
Function such that A62:
f1 = P0 . x1
and A63:
f1 in X0
and A64:
P0x . x1 = f1 | (X \ {x})
by A53, A56;
A65:
ex
F being
Function of
((X \ {x}) \/ {x}),
{1,0} st
(
f1 = F &
card (F " {1}) = k + 1 &
F . x = 0 )
by A63;
then A66:
dom f1 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
A67:
ex
F being
Function of
((X \ {x}) \/ {x}),
{1,0} st
(
f2 = F &
card (F " {1}) = k + 1 &
F . x = 0 )
by A60;
then A68:
dom f2 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
for
z being
object st
z in dom f1 holds
f1 . z = f2 . z
then A72:
f1 = f2
by A66, A68;
(
X0 = {} implies
card X0 = {} )
;
then
dom P0 = card X0
by FUNCT_2:def 1;
hence
x1 = x2
by A41, A56, A57, A62, A59, A72;
verum
end;
then
P0x is one-to-one
;
then consider XFS0 being XFinSequence of NAT such that
A73:
dom XFS0 = dom P0x
and
A74:
for z being set
for f being Function st z in dom XFS0 & f = P0x . z holds
XFS0 . z = card (Intersection ((Fy | ((dom Fy) \ {x})),f,1))
and
A75:
Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1)) = Sum XFS0
by A40, A35, Def3;
( Choose ((X \ {x}),(k + 1),1,0) = {} implies card (Choose ((X \ {x}),(k + 1),1,0)) = {} )
;
then A76:
dom P0x = card X0
by A40, FUNCT_2:def 1;
not x in X \ {x}
by ZFMISC_1:56;
then
(card X0) + (card X1) = card (Choose (X,(k + 1),1,0))
by A40, A6, A4, Th14;
then
dom (XP0 ^ XP1) = card (Choose (X,(k + 1),1,0))
by A45, A55, AFINSQ_1:def 3;
then reconsider XP01 = XP0 ^ XP1 as Function of (card (Choose (X,(k + 1),1,0))),(Choose (X,(k + 1),1,0)) by A54, FUNCT_2:2;
rng P0 misses rng P1
by Lm1, XBOOLE_1:64;
then
XP01 is one-to-one
by A41, A5, Th51;
then consider XFS being XFinSequence of NAT such that
A77:
dom XFS = dom XP01
and
A78:
for z being set
for f being Function st z in dom XFS & f = XP01 . z holds
XFS . z = card (Intersection (Fy,f,1))
and
A79:
Card_Intersection (Fy,(k + 1)) = Sum XFS
by A1, Def3;
A80:
addnat "**" XFS = Card_Intersection (Fy,(k + 1))
by A79, AFINSQ_2:51;
( Choose ((X \ {x}),k,1,0) = {} implies card (Choose ((X \ {x}),k,1,0)) = {} )
;
then A81:
dom P1x = card X1
by A6, FUNCT_2:def 1;
A82:
for n being Nat st n in dom XFS0 holds
XFS . n = XFS0 . n
proof
let n be
Nat;
( n in dom XFS0 implies XFS . n = XFS0 . n )
assume A83:
n in dom XFS0
;
XFS . n = XFS0 . n
consider fx being
Function such that A84:
fx = P0 . n
and A85:
fx in X0
and A86:
P0x . n = fx | (X \ {x})
by A53, A73, A83;
A87:
XFS0 . n = card (Intersection ((Fy | (X \ {x})),(fx | (X \ {x})),1))
by A1, A74, A83, A86;
A88:
ex
fx9 being
Function of
((X \ {x}) \/ {x}),
{1,0} st
(
fx = fx9 &
card (fx9 " {1}) = k + 1 &
fx9 . x = 0 )
by A85;
then consider x1 being
object such that A89:
x1 in fx " {1}
by CARD_1:27, XBOOLE_0:def 1;
fx . x1 in {1}
by A89, FUNCT_1:def 7;
then A90:
fx . x1 = 1
by TARSKI:def 1;
x1 in dom fx
by A89, FUNCT_1:def 7;
then A91:
1
in rng fx
by A90, FUNCT_1:def 3;
A92:
(X \ {x}) \/ {x} = X
by A1, A2, ZFMISC_1:116;
A93:
(dom XFS0) + 0 <= (dom XFS0) + (dom XFS1)
by XREAL_1:7;
dom fx = (X \ {x}) \/ {x}
by A88, FUNCT_2:def 1;
then A94:
fx " {1} = (fx | (X \ {x})) " {1}
by A88, A92, AFINSQ_2:67;
n < len XFS0
by A83, AFINSQ_1:86;
then
n < (len XFS0) + (dom XFS1)
by A93, XXREAL_0:2;
then
n < len XFS
by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;
then A95:
n in dom XFS
by AFINSQ_1:86;
XP01 . n = XP0 . n
by A73, A45, A83, AFINSQ_1:def 3;
then A96:
XFS . n = card (Intersection (Fy,fx,1))
by A78, A84, A95;
(
(fx | (X \ {x})) " {1} c= dom (fx | (X \ {x})) &
dom (fx | (X \ {x})) c= X \ {x} )
by RELAT_1:58, RELAT_1:132;
then
Intersection (
(Fy | (X \ {x})),
fx,1)
= Intersection (
Fy,
fx,1)
by A94, A91, Th29, XBOOLE_1:1;
hence
XFS . n = XFS0 . n
by A94, A96, A87, Th27;
verum
end;
( X1 = {} implies card X1 = {} )
;
then A97:
dom P1 = card X1
by FUNCT_2:def 1;
A98:
for n being Nat st n in dom XFS1 holds
XFS . ((len XFS0) + n) = XFS1 . n
proof
A99:
(X \ {x}) \/ {x} = X
by A1, A2, ZFMISC_1:116;
let n be
Nat;
( n in dom XFS1 implies XFS . ((len XFS0) + n) = XFS1 . n )
assume A100:
n in dom XFS1
;
XFS . ((len XFS0) + n) = XFS1 . n
consider fx being
Function such that A101:
fx = P1 . n
and A102:
fx in X1
and A103:
P1x . n = fx | (X \ {x})
by A16, A36, A100;
consider fx9 being
Function of
((X \ {x}) \/ {x}),
{1,0} such that A104:
fx = fx9
and A105:
card (fx9 " {1}) = k + 1
and A106:
fx9 . x = 1
by A102;
A107:
Intersection (
(Intersect ((Fy | (X \ {x})),((X \ {x}) --> (Fy . x)))),
(fx | (X \ {x})),1)
= (Intersection ((Fy | (X \ {x})),(fx | (X \ {x})),1)) /\ (Fy . x)
by A1, A35, Th50;
A108:
dom fx9 = (X \ {x}) \/ {x}
by FUNCT_2:def 1;
then A109:
dom fx = X
by A1, A2, A104, ZFMISC_1:116;
A110:
( 1
in rng (fx | (X \ {x})) &
(fx | (X \ {x})) " {1} c= X \ {x} )
proof
A111:
(
(fx | (X \ {x})) " {1} c= dom (fx | (X \ {x})) &
dom (fx | (X \ {x})) = (dom fx) /\ (X \ {x}) )
by RELAT_1:61, RELAT_1:132;
reconsider fx1 =
(fx | (X \ {x})) " {1} as
finite set ;
not
x in X \ {x}
by ZFMISC_1:56;
then
not
x in (dom fx) /\ (X \ {x})
by XBOOLE_0:def 4;
then
not
x in dom (fx | (X \ {x}))
by RELAT_1:61;
then A112:
not
x in fx1
by FUNCT_1:def 7;
{x} \/ fx1 = fx " {1}
by A1, A2, A104, A106, A109, AFINSQ_2:66;
then
(card fx1) + 1
= k + 1
by A104, A105, A112, CARD_2:41;
then consider y being
object such that A113:
y in fx1
by A3, CARD_1:27, XBOOLE_0:def 1;
y in dom (fx | (X \ {x}))
by A113, FUNCT_1:def 7;
then A114:
(fx | (X \ {x})) . y in rng (fx | (X \ {x}))
by FUNCT_1:def 3;
(
(dom fx) /\ (X \ {x}) c= X \ {x} &
(fx | (X \ {x})) . y in {1} )
by A113, FUNCT_1:def 7, XBOOLE_1:17;
hence
( 1
in rng (fx | (X \ {x})) &
(fx | (X \ {x})) " {1} c= X \ {x} )
by A111, A114, TARSKI:def 1;
verum
end;
n < len XFS1
by A100, AFINSQ_1:86;
then
(len XFS0) + n < (dom XFS0) + (dom XFS1)
by XREAL_1:8;
then
(dom XFS0) + n < len XFS
by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;
then A115:
(dom XFS0) + n in dom XFS
by AFINSQ_1:86;
XP01 . (n + (len XP0)) = fx
by A36, A97, A100, A101, AFINSQ_1:def 3;
then A116:
XFS . ((dom XFS0) + n) = card (Intersection (Fy,fx,1))
by A73, A45, A78, A76, A115;
fx . x in {1}
by A104, A106, TARSKI:def 1;
then A117:
x in fx " {1}
by A1, A2, A104, A108, A99, FUNCT_1:def 7;
XFS1 . n = card (Intersection ((Intersect ((Fy | (X \ {x})),((X \ {x}) --> (Fy . x)))),(fx | (X \ {x})),1))
by A1, A37, A100, A103;
then
XFS1 . n = card ((Intersection (Fy,(fx | (X \ {x})),1)) /\ (Fy . x))
by A110, A107, Th29;
hence
XFS . ((len XFS0) + n) = XFS1 . n
by A117, A109, A116, Th31;
verum
end;
dom XFS = (len XFS0) + (len XFS1)
by A73, A36, A45, A55, A77, A76, A81, AFINSQ_1:def 3;
then
XFS = XFS0 ^ XFS1
by A82, A98, AFINSQ_1:def 3;
then A118:
addnat "**" XFS = addnat . ((addnat "**" XFS0),(addnat "**" XFS1))
by AFINSQ_2:42;
addnat "**" XFS0 = Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))
by A75, AFINSQ_2:51;
hence
Card_Intersection (Fy,(k + 1)) = (Card_Intersection ((Fy | ((dom Fy) \ {x})),(k + 1))) + (Card_Intersection ((Intersect ((Fy | ((dom Fy) \ {x})),(((dom Fy) \ {x}) --> (Fy . x)))),k))
by A118, A39, A80, BINOP_2:def 23; verum