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 ) ) by A3, FINSET_1:8;
then reconsider urngFy = union (rng Fy) as finite set ;
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:

suppose A7: k = 0 ; :: thesis:

then 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 object 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 Th45, A13, A10;
hence card (union (rng Fy)) = Sum XFS by A9, AFINSQ_2:50; :: thesis:

end;

suppose A14: k > 0 ; :: thesis:

consider x being object such that
A15: x in dom Fy by A3, A4, CARD_1:27, XBOOLE_0:def 1;
reconsider x = x as set by TARSKI: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 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 Th54;
urngFyX /\ (Fy . x) = union (rng (Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x))))) by Th49;
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 Th54;
set XI1 = (- 1) (#) XI;
reconsider XI1 = (- 1) (#) XI as XFinSequence of INT ;
reconsider XcF = <%(card (Fy . x))%>, X0 = <%0%> as XFinSequence of INT ;
reconsider F1 = <%(card (Fy . x))%> ^ XI1, F2 = XFyX ^ <%0%> as XFinSequence of INT ;
A21: card (X \ {x}) = k by A3, A4, A15, STIRL2_1:55;
reconsider zz = 0 as Element of INT by INT_1:def 2;
A22: addint "**" X0 = zz 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) + zz 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, Th53;
A29: urngFyX /\ (Fy . x) = urngI by Th49;
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 Th48;
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; :: thesis:
assume A34: n in dom XFS ; :: thesis:
A35: n < len XFS by A34, AFINSQ_1:86;
reconsider N = n as Element of NAT by ORDINAL1:def 12;

per cases ;

suppose A36: n = 0 ; :: thesis:

A37: 0 in Segm k by A14, NAT_1:44;
k = dom XFyX by A3, A4, A15, A17, STIRL2_1:55;
then A38: ( F2 . 0 = XFyX . 0 & XFyX . 0 = ((- 1) |^ 0) * (Card_Intersection ((Fy | (X \ {x})),(0 + 1))) ) by A18, AFINSQ_1:def 3, A37;
( F1 . 0 = card (Fy . x) & (- 1) |^ 0 = 1 ) by AFINSQ_1:35, NEWTON:4;
then A39: addint . ((F1 . 0),(F2 . 0)) = (card (Fy . x)) + (Card_Intersection ((Fy | (X \ {x})),(0 + 1))) by A38, BINOP_2:def 20;
A40: (- 1) |^ 0 = 1 by NEWTON:4;
XFS . 0 = ((- 1) |^ 0) * (Card_Intersection (Fy,(0 + 1))) by A6, A34, A36;
hence XFS . n = addint . ((F1 . n),(F2 . n)) by A3, A15, A36, A39, A40, Th47; :: thesis:

end;

suppose A41: n > 0 ; :: thesis:

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
A42: len <%(card (Fy . x))%> = 1 by AFINSQ_1:33;
A43: card (X \ {x}) = k by A3, A4, A15, STIRL2_1:55;
A44: n < k + 1 by A4, A5, A35;
then A45: n <= k by NAT_1:13;
A46: n1 < n1 + 1 by NAT_1:13;
then n1 < k by A45, XXREAL_0:2;
then n1 < len XI by A19, A43;
then n1 in dom XI by AFINSQ_1:86;
then A47: ( 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 A46, 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, A44, A42, A47, AFINSQ_1:19;
then A48: F1 . n = ((- 1) |^ (n1 + 1)) * (Card_Intersection ((Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))),(n1 + 1))) by NEWTON:6;
A49: 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, A41, Th52;
then A50: 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 A49;

per cases by A45, XXREAL_0:1;

suppose n < k ; :: thesis:

then A51: n in Segm 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, A51, AFINSQ_1:def 3;
hence XFS . n = addint . ((F1 . n),(F2 . n)) by A50, A48, BINOP_2:def 20; :: thesis:

end;

suppose A52: n = k ; :: thesis:

then n = card (X \ {x}) by A3, A4, A15, STIRL2_1:55;
then n + 1 > card (X \ {x}) by NAT_1:13;
then A53: Card_Intersection ((Fy | (X \ {x})),(n + 1)) = 0 by A30, Th42;
n = len XFyX by A3, A4, A15, A17, A52, STIRL2_1:55;
then F2 . n = 0 by AFINSQ_1:36;
hence XFS . n = addint . ((F1 . n),(F2 . n)) by A50, A48, A53, BINOP_2:def 20; :: thesis:

end;

card urngFyX = Sum XFyX by A2, A30, A17, A18, A21;
then A54: card urngFy = ((Sum XFyX) + (card (Fy . x))) - (Sum XI) by A31, A28, A29, CARD_2:45;
A55: len <%0%> = 1 by AFINSQ_1:33;
len XFyX = card (X \ {x}) by A17;
then A56: len F2 = k + 1 by A55, A16, AFINSQ_1:17;
A57: len XFS = k + 1 by A4, A5;
Sum XFS = addint "**" XFS by AFINSQ_2:50
.= addint "**" (F1 ^ F2) by A32, A56, A33, A57, AFINSQ_2:46
.= Sum (F1 ^ F2) by AFINSQ_2:50 ;
hence card (union (rng Fy)) = Sum XFS by A27, A54; :: thesis:

end;

A58: S₁[ 0 ]

proof

let Fy be finite-yielding Function; :: thesis:
let X be finite set ; :: thesis:
assume that
A59: dom Fy = X and
A60: card X = 0 ; :: thesis:
dom Fy = {} by A59, A60;
then A61: rng Fy = {} by RELAT_1:42;
let XFS be XFinSequence of INT ; :: thesis:
assume that
A62: 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 A60, A62;
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 A61, AFINSQ_2:50, ZFMISC_1:2; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A58, 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: