defpred S1[ Element of NAT ] means for Fy being finite-yielding Function
for X being finite set st dom Fy = X & card X = $1 holds
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS;
A1:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
let Fy be
finite-yielding Function;
for X being finite set st dom Fy = X & card X = k + 1 holds
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFSlet X be
finite set ;
( dom Fy = X & card X = k + 1 implies for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS )
assume that A3:
dom Fy = X
and A4:
card X = k + 1
;
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS
(
rng Fy is
finite & ( for
x being
set st
x in rng Fy holds
x is
finite ) )
then reconsider urngFy =
union (rng Fy) as
finite set by FINSET_1:25;
let XFS be
XFinSequence of
INT ;
( dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) implies card (union (rng Fy)) = Sum XFS )
assume that A5:
dom XFS = card X
and A6:
for
n being
Element of
NAT st
n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1))
;
card (union (rng Fy)) = Sum XFS
per cases
( k = 0 or k > 0 )
;
suppose A7:
k = 0
;
card (union (rng Fy)) = Sum XFSthen
len XFS = 1
by A4, A5;
then A8:
XFS = <%(XFS . 0 )%>
by AFINSQ_1:38;
XFS . 0 is
Element of
INT
by INT_1:def 2;
then A9:
addint "**" XFS = XFS . 0
by A8, STIRL2_1:44;
0 in dom XFS
by A4, A5, A7, CARD_1:87, TARSKI:def 1;
then A10:
XFS . 0 = ((- 1) |^ 0 ) * (Card_Intersection Fy,(0 + 1))
by A6;
consider x being
set such that A11:
dom Fy = {x}
by A3, A4, A7, CARD_2:60;
A12:
rng Fy = {(Fy . x)}
by A11, FUNCT_1:14;
then A13:
union (rng Fy) = Fy . x
by ZFMISC_1:31;
(
(- 1) |^ 0 = 1 &
Fy = x .--> (Fy . x) )
by A11, A12, FUNCOP_1:15, NEWTON:9;
hence
card (union (rng Fy)) = Sum XFS
by A9, A10, A13, Th54;
verum end; suppose A14:
k > 0
;
card (union (rng Fy)) = Sum XFSconsider x being
set such that A15:
x in dom Fy
by A3, A4, CARD_1:47, XBOOLE_0:def 1;
set Xx =
X \ {x};
A16:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:65;
set FyX =
Fy | (X \ {x});
urngFy = (union (rng (Fy | (X \ {x})))) \/ (Fy . x)
by A3, A15, Th65;
then reconsider urngFyX =
union (rng (Fy | (X \ {x}))) as
finite set by FINSET_1:13, XBOOLE_1:7;
set Fyx =
Fy . x;
set I =
Intersect (Fy | (X \ {x})),
((dom (Fy | (X \ {x}))) --> (Fy . x));
consider XFyX being
XFinSequence of
INT such that A17:
dom XFyX = card (X \ {x})
and A18:
for
n being
Element of
NAT st
n in dom XFyX holds
XFyX . n = ((- 1) |^ n) * (Card_Intersection (Fy | (X \ {x})),(n + 1))
by Th66;
urngFyX /\ (Fy . x) = union (rng (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))))
by Th58;
then reconsider urngI =
union (rng (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))) as
finite set ;
consider XI being
XFinSequence of
INT such that A19:
dom XI = card (X \ {x})
and A20:
for
n being
Element of
NAT st
n in dom XI holds
XI . n = ((- 1) |^ n) * (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),(n + 1))
by Th66;
deffunc H1(
set )
-> Element of
INT =
(- 1) * (XI . $1);
A21:
for
x being
set st
x in card (X \ {x}) holds
H1(
x)
in INT
by INT_1:def 2;
consider XI1 being
Function of
card (X \ {x}),
INT such that A22:
for
x being
set st
x in card (X \ {x}) holds
XI1 . x = H1(
x)
from FUNCT_2:sch 2(A21);
A23:
dom XI1 = card (X \ {x})
by FUNCT_2:def 1;
then reconsider XI1 =
XI1 as
XFinSequence by AFINSQ_1:7;
reconsider XI1 =
XI1 as
XFinSequence of
INT ;
card (Fy . x) is
Element of
INT
by INT_1:def 2;
then A24:
(
rng <%(card (Fy . x))%> = {(card (Fy . x))} &
{(card (Fy . x))} is
Subset of )
by AFINSQ_1:36, SUBSET_1:55;
rng XI1 c= INT
by RELAT_1:def 19;
then
(rng <%(card (Fy . x))%>) \/ (rng XI1) c= INT
by A24, XBOOLE_1:8;
then A25:
rng (<%(card (Fy . x))%> ^ XI1) c= INT
by AFINSQ_1:29;
0 is
Element of
INT
by INT_1:def 2;
then A26:
(
rng <%0 %> = {0 } &
{0 } is
Subset of )
by AFINSQ_1:36, SUBSET_1:55;
then reconsider XcF =
<%(card (Fy . x))%>,
X0 =
<%0 %> as
XFinSequence of
INT by A24, RELAT_1:def 19;
rng XFyX c= INT
by RELAT_1:def 19;
then
(rng XFyX) \/ (rng <%0 %>) c= INT
by A26, XBOOLE_1:8;
then
rng (XFyX ^ <%0 %>) c= INT
by AFINSQ_1:29;
then reconsider F1 =
<%(card (Fy . x))%> ^ XI1,
F2 =
XFyX ^ <%0 %> as
XFinSequence of
INT by A25, RELAT_1:def 19;
A27:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:65;
0 is
Element of
INT
by INT_1:def 2;
then
addint "**" X0 = 0
by STIRL2_1:44;
then A28:
addint "**" F2 = addint . (addint "**" XFyX),
0
by STIRL2_1:47;
card (Fy . x) is
Element of
INT
by INT_1:def 2;
then
addint "**" XcF = card (Fy . x)
by STIRL2_1:44;
then A29:
addint "**" F1 = addint . (card (Fy . x)),
(addint "**" XI1)
by STIRL2_1:47;
for
n being
Element of
NAT st
n in dom XI holds
(- 1) * (XI . n) = XI1 . n
by A19, A22;
then A30:
(- 1) * (Sum XI) = Sum XI1
by A19, A23, Th64;
A31:
(addint "**" F1) + (addint "**" F2) = addint . (addint "**" F1),
(addint "**" F2)
by BINOP_2:def 20;
addint . (addint "**" XFyX),
0 = (addint "**" XFyX) + 0
by BINOP_2:def 20;
then
(addint "**" F1) + (addint "**" F2) = ((card (Fy . x)) + (addint "**" XI1)) + (addint "**" XFyX)
by A29, A28, BINOP_2:def 20;
then A32:
addint "**" (F1 ^ F2) = ((card (Fy . x)) + ((- 1) * (Sum XI))) + (Sum XFyX)
by A30, A31, STIRL2_1:47;
A33:
urngFyX \/ (Fy . x) = urngFy
by A3, A15, Th65;
A34:
urngFyX /\ (Fy . x) = urngI
by Th58;
A35:
dom (Fy | (X \ {x})) = X \ {x}
by A3, RELAT_1:91;
then
dom (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))) = X \ {x}
by Th57;
then A36:
card urngI = Sum XI
by A2, A19, A20, A27;
(
len <%(card (Fy . x))%> = 1 &
len XI1 = card (X \ {x}) )
by AFINSQ_1:36, FUNCT_2:def 1;
then A37:
len F1 = k + 1
by A16, AFINSQ_1:20;
A38:
for
n being
Element of
NAT st
n in dom XFS holds
XFS . n = addint . (F1 . n),
(F2 . n)
proof
let n be
Element of
NAT ;
( n in dom XFS implies XFS . n = addint . (F1 . n),(F2 . n) )
assume A39:
n in dom XFS
;
XFS . n = addint . (F1 . n),(F2 . n)
per cases
( n = 0 or n > 0 )
;
suppose A40:
n = 0
;
XFS . n = addint . (F1 . n),(F2 . n)
(
0 in k &
k = dom XFyX )
by A3, A4, A14, A15, A17, NAT_1:45, STIRL2_1:65;
then A41:
(
F2 . 0 = XFyX . 0 &
XFyX . 0 = ((- 1) |^ 0 ) * (Card_Intersection (Fy | (X \ {x})),(0 + 1)) )
by A18, AFINSQ_1:def 4;
(
F1 . 0 = card (Fy . x) &
(- 1) |^ 0 = 1 )
by AFINSQ_1:39, NEWTON:9;
then A42:
addint . (F1 . 0 ),
(F2 . 0 ) = (card (Fy . x)) + (Card_Intersection (Fy | (X \ {x})),(0 + 1))
by A41, BINOP_2:def 20;
A43:
(- 1) |^ 0 = 1
by NEWTON:9;
XFS . 0 = ((- 1) |^ 0 ) * (Card_Intersection Fy,(0 + 1))
by A6, A39, A40;
hence
XFS . n = addint . (F1 . n),
(F2 . n)
by A3, A15, A40, A42, A43, Th56;
verum suppose A44:
n > 0
;
XFS . n = addint . (F1 . n),(F2 . n)then reconsider n1 =
n - 1 as
Element of
NAT by NAT_1:20;
A45:
len <%(card (Fy . x))%> = 1
by AFINSQ_1:36;
A46:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:65;
A47:
n < k + 1
by A4, A5, A39, NAT_1:45;
then A48:
n <= k
by NAT_1:13;
A49:
n1 < n1 + 1
by NAT_1:13;
then
n1 < k
by A48, XXREAL_0:2;
then
n1 in card (X \ {x})
by A46, NAT_1:45;
then A50:
(
XI1 . n1 = (- 1) * (XI . n1) &
XI . n1 = ((- 1) |^ n1) * (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),(n1 + 1)) )
by A19, A20, A22;
0 + 1
<= n
by A49, NAT_1:13;
then
F1 . n = ((- 1) * ((- 1) |^ n1)) * (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),(n1 + 1))
by A37, A47, A45, A50, AFINSQ_1:22;
then A51:
F1 . n = ((- 1) |^ (n1 + 1)) * (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),(n1 + 1))
by NEWTON:11;
A52:
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1))
by A6, A39;
Card_Intersection Fy,
(n + 1) = (Card_Intersection (Fy | (X \ {x})),(n + 1)) + (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),n)
by A3, A15, A35, A44, Th61;
then A53:
XFS . n = (((- 1) |^ n) * (Card_Intersection (Fy | (X \ {x})),(n + 1))) + (((- 1) |^ n) * (Card_Intersection (Intersect (Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))),n))
by A52;
per cases
( n < k or n = k )
by A48, XXREAL_0:1;
suppose
n < k
;
XFS . n = addint . (F1 . n),(F2 . n)then A54:
n in k
by NAT_1:45;
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:65;
then
(
XFyX . n = ((- 1) |^ n) * (Card_Intersection (Fy | (X \ {x})),(n + 1)) &
F2 . n = XFyX . n )
by A17, A18, A54, AFINSQ_1:def 4;
hence
XFS . n = addint . (F1 . n),
(F2 . n)
by A53, A51, BINOP_2:def 20;
verum end; suppose A55:
n = k
;
XFS . n = addint . (F1 . n),(F2 . n)then
n = card (X \ {x})
by A3, A4, A15, STIRL2_1:65;
then
n + 1
> card (X \ {x})
by NAT_1:13;
then A56:
Card_Intersection (Fy | (X \ {x})),
(n + 1) = 0
by A35, Th51;
n = len XFyX
by A3, A4, A15, A17, A55, STIRL2_1:65;
then
F2 . n = 0
by AFINSQ_1:40;
hence
XFS . n = addint . (F1 . n),
(F2 . n)
by A53, A51, A56, BINOP_2:def 20;
verum end; end;
end;
card urngFyX = Sum XFyX
by A2, A35, A17, A18, A27;
then A57:
card urngFy = ((Sum XFyX) + (card (Fy . x))) - (Sum XI)
by A36, A33, A34, CARD_2:64;
A58:
len <%0 %> = 1
by AFINSQ_1:36;
len XFyX = card (X \ {x})
by A17;
then A59:
len F2 = k + 1
by A58, A16, AFINSQ_1:20;
len XFS = k + 1
by A4, A5;
hence
card (union (rng Fy)) = Sum XFS
by A37, A59, A38, A32, A57, Th62;
verum end;
end;
A60:
S1[ 0 ]
proof
let Fy be
finite-yielding Function;
for X being finite set st dom Fy = X & card X = 0 holds
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFSlet X be
finite set ;
( dom Fy = X & card X = 0 implies for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS )
assume that A61:
dom Fy = X
and A62:
card X = 0
;
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS
dom Fy = {}
by A61, A62;
then A63:
rng Fy = {}
by RELAT_1:65;
let XFS be
XFinSequence of
INT ;
( dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) implies card (union (rng Fy)) = Sum XFS )
assume that A64:
dom XFS = card X
and
for
n being
Element of
NAT st
n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1))
;
card (union (rng Fy)) = Sum XFS
len XFS = 0
by A62, A64;
hence
card (union (rng Fy)) = Sum XFS
by A63, BINOP_2:4, STIRL2_1:def 3, ZFMISC_1:2;
verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A60, A1);
hence
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XFS being XFinSequence of INT st dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS
; verum