defpred S1[ 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 st dom XFS = card X & ( for n being 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 Nat st S1[k] holds
S1[k + 1]
proof
let k be
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 st dom XFS = card X & ( for n being 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 st dom XFS = card X & ( for n being 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 st dom XFS = card X & ( for n being 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 ) )
by A3, FINSET_1:8;
then reconsider urngFy =
union (rng Fy) as
finite set ;
let XFS be
XFinSequence of ;
( dom XFS = card X & ( for n being 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
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:34;
XFS . 0 is
Element of
INT
by INT_1:def 2;
then A9:
addint "**" XFS = XFS . 0
by A8, AFINSQ_2:37;
0 in dom XFS
by A4, A5, A7, CARD_1:49, 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:42;
A12:
rng Fy = {(Fy . x)}
by A11, FUNCT_1:4;
then A13:
union (rng Fy) = Fy . x
by ZFMISC_1:25;
(
(- 1) |^ 0 = 1 &
Fy = x .--> (Fy . x) )
by A11, A12, FUNCOP_1:9, NEWTON:4;
then
XFS . 0 = card (union (rng Fy))
by Th46, A13, A10;
hence
card (union (rng Fy)) = Sum XFS
by A9, AFINSQ_2:50;
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:27, XBOOLE_0:def 1;
set Xx =
X \ {x};
A16:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:55;
set FyX =
Fy | (X \ {x});
reconsider urngFyX =
union (rng (Fy | (X \ {x}))) as
finite set ;
set Fyx =
Fy . x;
set I =
Intersect (
(Fy | (X \ {x})),
((dom (Fy | (X \ {x}))) --> (Fy . x)));
consider XFyX being
XFinSequence of
such that A17:
dom XFyX = card (X \ {x})
and A18:
for
n being
Nat st
n in dom XFyX holds
XFyX . n = ((- 1) |^ n) * (Card_Intersection ((Fy | (X \ {x})),(n + 1)))
by Th55;
urngFyX /\ (Fy . x) = union (rng (Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))))
by Th50;
then reconsider urngI =
union (rng (Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))))) as
finite set ;
consider XI being
XFinSequence of
such that A19:
dom XI = card (X \ {x})
and A20:
for
n being
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 Th55;
set XI1 =
(- 1) (#) XI;
reconsider XI1 =
(- 1) (#) XI as
XFinSequence of ;
reconsider XcF =
<%(card (Fy . x))%>,
X0 =
<%0%> as
XFinSequence of ;
reconsider F1 =
<%(card (Fy . x))%> ^ XI1,
F2 =
XFyX ^ <%0%> as
XFinSequence of ;
A21:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:55;
0 is
Element of
INT
by INT_1:def 2;
then A22:
addint "**" X0 = 0
by AFINSQ_2:37;
card (Fy . x) is
Element of
INT
by INT_1:def 2;
then A23:
addint "**" XcF = card (Fy . x)
by AFINSQ_2:37;
A24:
(- 1) * (Sum XI) = Sum XI1
by AFINSQ_2:64;
A25:
addint "**" F1 =
addint . (
(card (Fy . x)),
(addint "**" XI1))
by A23, AFINSQ_2:42
.=
(card (Fy . x)) + (addint "**" XI1)
by BINOP_2:def 20
.=
(card (Fy . x)) + (Sum XI1)
by AFINSQ_2:50
;
A26:
addint "**" F2 =
addint . (
(addint "**" XFyX),
0)
by A22, AFINSQ_2:42
.=
(addint "**" XFyX) + 0
by BINOP_2:def 20
.=
Sum XFyX
by AFINSQ_2:50
;
A27:
Sum (F1 ^ F2) =
(Sum F1) + (Sum F2)
by AFINSQ_2:55
.=
(addint "**" F1) + (Sum F2)
by AFINSQ_2:50
.=
((card (Fy . x)) + ((- 1) * (Sum XI))) + (Sum XFyX)
by A24, A25, A26, AFINSQ_2:50
;
A28:
urngFyX \/ (Fy . x) = urngFy
by A3, A15, Th54;
A29:
urngFyX /\ (Fy . x) = urngI
by Th50;
A30:
dom (Fy | (X \ {x})) = X \ {x}
by A3, RELAT_1:62;
then
dom (Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))) = X \ {x}
by Th49;
then A31:
card urngI = Sum XI
by A2, A19, A20, A21;
(
len <%(card (Fy . x))%> = 1 &
len XI1 = card (X \ {x}) )
by A19, AFINSQ_1:33, VALUED_1:def 5;
then A32:
len F1 = k + 1
by A16, AFINSQ_1:17;
A33:
for
n being
Nat st
n in dom XFS holds
XFS . n = addint . (
(F1 . n),
(F2 . n))
proof
let n be
Nat;
( n in dom XFS implies XFS . n = addint . ((F1 . n),(F2 . n)) )
assume A34:
n in dom XFS
;
XFS . n = addint . ((F1 . n),(F2 . n))
reconsider N =
n as
Element of
NAT by ORDINAL1:def 12;
per cases
( n = 0 or n > 0 )
;
suppose A35:
n = 0
;
XFS . n = addint . ((F1 . n),(F2 . n))
(
0 in k &
k = dom XFyX )
by A3, A4, A14, A15, A17, NAT_1:44, STIRL2_1:55;
then A36:
(
F2 . 0 = XFyX . 0 &
XFyX . 0 = ((- 1) |^ 0) * (Card_Intersection ((Fy | (X \ {x})),(0 + 1))) )
by A18, AFINSQ_1:def 3;
(
F1 . 0 = card (Fy . x) &
(- 1) |^ 0 = 1 )
by AFINSQ_1:35, NEWTON:4;
then A37:
addint . (
(F1 . 0),
(F2 . 0))
= (card (Fy . x)) + (Card_Intersection ((Fy | (X \ {x})),(0 + 1)))
by A36, BINOP_2:def 20;
A38:
(- 1) |^ 0 = 1
by NEWTON:4;
XFS . 0 = ((- 1) |^ 0) * (Card_Intersection (Fy,(0 + 1)))
by A6, A34, A35;
hence
XFS . n = addint . (
(F1 . n),
(F2 . n))
by A3, A15, A35, A37, A38, Th48;
verum suppose A39:
n > 0
;
XFS . n = addint . ((F1 . n),(F2 . n))then reconsider n1 =
n - 1 as
Element of
NAT by NAT_1:20;
A40:
len <%(card (Fy . x))%> = 1
by AFINSQ_1:33;
A41:
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:55;
A42:
n < k + 1
by A4, A5, A34, NAT_1:44;
then A43:
n <= k
by NAT_1:13;
A44:
n1 < n1 + 1
by NAT_1:13;
then
n1 < k
by A43, XXREAL_0:2;
then
n1 in dom XI
by A19, A41, NAT_1:44;
then A45:
(
XI1 . n1 = (- 1) * (XI . n1) &
XI . n1 = ((- 1) |^ n1) * (Card_Intersection ((Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))),(n1 + 1))) )
by A20, VALUED_1:6;
0 + 1
<= n
by A44, NAT_1:13;
then
F1 . n = ((- 1) * ((- 1) |^ n1)) * (Card_Intersection ((Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))),(n1 + 1)))
by A32, A42, A40, A45, AFINSQ_1:19;
then A46:
F1 . n = ((- 1) |^ (n1 + 1)) * (Card_Intersection ((Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))),(n1 + 1)))
by NEWTON:6;
A47:
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1)))
by A6, A34;
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, A30, A39, Th53;
then A48:
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 A47;
per cases
( n < k or n = k )
by A43, XXREAL_0:1;
suppose
n < k
;
XFS . n = addint . ((F1 . n),(F2 . n))then A49:
n in k
by NAT_1:44;
card (X \ {x}) = k
by A3, A4, A15, STIRL2_1:55;
then
(
XFyX . n = ((- 1) |^ n) * (Card_Intersection ((Fy | (X \ {x})),(n + 1))) &
F2 . n = XFyX . n )
by A17, A18, A49, AFINSQ_1:def 3;
hence
XFS . n = addint . (
(F1 . n),
(F2 . n))
by A48, A46, BINOP_2:def 20;
verum end; suppose A50:
n = k
;
XFS . n = addint . ((F1 . n),(F2 . n))then
n = card (X \ {x})
by A3, A4, A15, STIRL2_1:55;
then
n + 1
> card (X \ {x})
by NAT_1:13;
then A51:
Card_Intersection (
(Fy | (X \ {x})),
(n + 1))
= 0
by A30, Th43;
n = len XFyX
by A3, A4, A15, A17, A50, STIRL2_1:55;
then
F2 . n = 0
by AFINSQ_1:36;
hence
XFS . n = addint . (
(F1 . n),
(F2 . n))
by A48, A46, A51, BINOP_2:def 20;
verum end; end;
end;
card urngFyX = Sum XFyX
by A2, A30, A17, A18, A21;
then A52:
card urngFy = ((Sum XFyX) + (card (Fy . x))) - (Sum XI)
by A31, A28, A29, CARD_2:45;
A53:
len <%0%> = 1
by AFINSQ_1:33;
len XFyX = card (X \ {x})
by A17;
then A54:
len F2 = k + 1
by A53, A16, AFINSQ_1:17;
A55:
len XFS = k + 1
by A4, A5;
Sum XFS =
addint "**" XFS
by AFINSQ_2:50
.=
addint "**" (F1 ^ F2)
by A32, A54, A33, A55, AFINSQ_2:46
.=
Sum (F1 ^ F2)
by AFINSQ_2:50
;
hence
card (union (rng Fy)) = Sum XFS
by A27, A52;
verum end;
end;
A56:
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 st dom XFS = card X & ( for n being 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 st dom XFS = card X & ( for n being 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 A57:
dom Fy = X
and A58:
card X = 0
;
for XFS being XFinSequence of st dom XFS = card X & ( for n being 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 A57, A58;
then A59:
rng Fy = {}
by RELAT_1:42;
let XFS be
XFinSequence of ;
( dom XFS = card X & ( for n being 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 A60:
dom XFS = card X
and
for
n being
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 A58, A60;
then addint "**" XFS =
the_unity_wrt addint
by AFINSQ_2:def 8
.=
0
by BINOP_2:4
;
hence
card (union (rng Fy)) = Sum XFS
by A59, A58, AFINSQ_2:50, ZFMISC_1:2;
verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A56, A1);
hence
for Fy being finite-yielding Function
for X being finite set st dom Fy = X holds
for XFS being XFinSequence of st dom XFS = card X & ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) holds
card (union (rng Fy)) = Sum XFS
; verum