defpred S₁[ 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 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 S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A2: S₁[k] ; :: thesis:
let Fy be finite-yielding Function; :: thesis:
let X be finite set ; :: thesis:
assume that
A3: dom Fy = X and
A4: card X = k + 1 ; :: thesis:
( rng Fy is finite & ( for x being set st x in rng Fy holds
x is finite ) )

thus rng Fy is finite by A3, FINSET_1:26; :: thesis:
let x be set ; :: thesis:
assume x in rng Fy ; :: thesis:
then ex x1 being set st
( x1 in dom Fy & Fy . x1 = x ) by FUNCT_1:def 5;
hence x is finite ; :: thesis:

end;

then reconsider urngFy = union (rng Fy) as finite set by FINSET_1:25;
let XFS be XFinSequence of INT ; :: thesis:
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)) ; :: thesis:

per cases ;

suppose A7: k = 0 ; :: thesis:

then 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, AFINSQ_2:49;
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;
then XFS . 0 = card (union (rng Fy)) by Th54, A13, A10;
hence card (union (rng Fy)) = Sum XFS by A9, AFINSQ_2:62; :: thesis:

end;

suppose A14: k > 0 ; :: thesis:

consider 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 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 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 H₁( set ) -> Element of INT = (- 1) * (XI . $1);
set XI1 = (- 1) (#) XI;
B: rng ((- 1) (#) XI) c= INT by VALUED_0:def 5;
then reconsider XI1 = (- 1) (#) XI as XFinSequence of INT by RELAT_1:def 19;
BBB: 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 INT ) by AFINSQ_1:36, SUBSET_1:55;
(rng <%(card (Fy . x))%>) \/ (rng XI1) c= INT by B, A24, XBOOLE_1:8;
then A25: rng (<%(card (Fy . x))%> ^ XI1) c= INT by AFINSQ_1:29;
E: 0 is Element of INT by INT_1:def 2;
then A26: ( rng <%0 %> = {0 } & {0 } is Subset of INT ) by AFINSQ_1:36, SUBSET_1:55;
reconsider XcF = <%(card (Fy . x))%>, X0 = <%0 %> as XFinSequence of INT by BBB, E;
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 Y1: addint "**" X0 = 0 by AFINSQ_2:49;
card (Fy . x) is Element of INT by INT_1:def 2;
then HG: addint "**" XcF = card (Fy . x) by AFINSQ_2:49;
A30: (- 1) * (Sum XI) = Sum XI1 by AFINSQ_2:76;
B2: addint "**" F1 = addint . (card (Fy . x)),(addint "**" XI1) by HG, AFINSQ_2:54
.= (card (Fy . x)) + (addint "**" XI1) by BINOP_2:def 20
.= (card (Fy . x)) + (Sum XI1) by AFINSQ_2:62 ;
B3: addint "**" F2 = addint . (addint "**" XFyX),0 by Y1, AFINSQ_2:54
.= (addint "**" XFyX) + 0 by BINOP_2:def 20
.= Sum XFyX by AFINSQ_2:62 ;
A32: Sum (F1 ^ F2) = (Sum F1) + (Sum F2) by AFINSQ_2:67
.= (addint "**" F1) + (Sum F2) by AFINSQ_2:62
.= ((card (Fy . x)) + ((- 1) * (Sum XI))) + (Sum XFyX) by AFINSQ_2:62, A30, B2, B3 ;
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, VALUED_1:def 5, A19;
then A37: len F1 = k + 1 by A16, AFINSQ_1:20;
A38: for n being Nat st n in dom XFS holds
XFS . n = addint . (F1 . n),(F2 . n)

proof

let n be Nat; :: thesis:
assume A39: n in dom XFS ; :: thesis:
reconsider N = n as Element of NAT by ORDINAL1:def 13;

per cases ;

suppose A40: n = 0 ; :: thesis:

( 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; :: thesis:

end;

suppose A44: n > 0 ; :: thesis:

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 dom XI by A19, 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 A20, VALUED_1:6;
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 by A48, XXREAL_0:1;

suppose n < k ; :: thesis:

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; :: thesis:

end;

suppose A55: n = k ; :: thesis:

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; :: thesis:

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;
A60: len XFS = k + 1 by A4, A5;
Sum XFS = addint "**" XFS by AFINSQ_2:62
.= addint "**" (F1 ^ F2) by A37, A59, A38, AFINSQ_2:58, A60
.= Sum (F1 ^ F2) by AFINSQ_2:62 ;
hence card (union (rng Fy)) = Sum XFS by A32, A57; :: thesis:

end;

A60: S₁[ 0 ]

proof

let Fy be finite-yielding Function; :: thesis:
let X be finite set ; :: thesis:
assume that
A61: dom Fy = X and
A62: card X = 0 ; :: thesis:
dom Fy = {} by A61, A62;
then A63: rng Fy = {} by RELAT_1:65;
let XFS be XFinSequence of INT ; :: thesis:
assume that
A64: dom XFS = card X and
for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ; :: thesis:
len XFS = 0 by A62, A64;
then addint "**" XFS = the_unity_wrt addint by AFINSQ_2:def 9
.= 0 by BINOP_2:4 ;
hence card (union (rng Fy)) = Sum XFS by A63, ZFMISC_1:2, AFINSQ_2:62, A62; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(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 Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) holds
card (union (rng Fy)) = Sum XFS ; :: thesis: