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 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:8; :: 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 3;
hence x is finite ; :: thesis:

end;

then reconsider urngFy = union (rng Fy) as finite set by FINSET_1:7;
let XFS be XFinSequence of ; :: 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: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 Th54, A13, A10;
hence card (union (rng Fy)) = Sum XFS by A9, AFINSQ_2:50; :: thesis:

end;

suppose A14: k > 0 ; :: thesis:

consider 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});
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:1, XBOOLE_1:7;
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 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 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;
set XI1 = (- 1) (#) XI;
A21: rng ((- 1) (#) XI) c= INT by VALUED_0:def 5;
then reconsider XI1 = (- 1) (#) XI as XFinSequence of by RELAT_1:def 19;
A22: card (Fy . x) is Element of INT by INT_1:def 2;
then ( rng <%(card (Fy . x))%> = {(card (Fy . x))} & {(card (Fy . x))} is Subset of INT ) by AFINSQ_1:33, SUBSET_1:33;
then (rng <%(card (Fy . x))%>) \/ (rng XI1) c= INT by A21, XBOOLE_1:8;
then A23: rng (<%(card (Fy . x))%> ^ XI1) c= INT by AFINSQ_1:26;
A24: 0 is Element of INT by INT_1:def 2;
then A25: ( rng <%0%> = {0} & {0} is Subset of INT ) by AFINSQ_1:33, SUBSET_1:33;
reconsider XcF = <%(card (Fy . x))%>, X0 = <%0%> as XFinSequence of by A22, A24;
rng XFyX c= INT by RELAT_1:def 19;
then (rng XFyX) \/ (rng <%0%>) c= INT by A25, XBOOLE_1:8;
then rng (XFyX ^ <%0%>) c= INT by AFINSQ_1:26;
then reconsider F1 = <%(card (Fy . x))%> ^ XI1, F2 = XFyX ^ <%0%> as XFinSequence of by A23, RELAT_1:def 19;
A26: card (X \ {x}) = k by A3, A4, A15, STIRL2_1:55;
0 is Element of INT by INT_1:def 2;
then A27: addint "**" X0 = 0 by AFINSQ_2:37;
card (Fy . x) is Element of INT by INT_1:def 2;
then A28: addint "**" XcF = card (Fy . x) by AFINSQ_2:37;
A29: (- 1) * (Sum XI) = Sum XI1 by AFINSQ_2:64;
A30: addint "**" F1 = addint . ((card (Fy . x)),(addint "**" XI1)) by A28, AFINSQ_2:42
.= (card (Fy . x)) + (addint "**" XI1) by BINOP_2:def 20
.= (card (Fy . x)) + (Sum XI1) by AFINSQ_2:50 ;
A31: addint "**" F2 = addint . ((addint "**" XFyX),0) by A27, AFINSQ_2:42
.= (addint "**" XFyX) + 0 by BINOP_2:def 20
.= Sum XFyX by AFINSQ_2:50 ;
A32: 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 A29, A30, A31, AFINSQ_2:50 ;
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:62;
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, A26;
( len <%(card (Fy . x))%> = 1 & len XI1 = card (X \ {x}) ) by A19, AFINSQ_1:33, VALUED_1:def 5;
then A37: len F1 = k + 1 by A16, AFINSQ_1:17;
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 12;

per cases ;

suppose A40: n = 0 ; :: thesis:

( 0 in k & k = dom XFyX ) by A3, A4, A14, A15, A17, NAT_1:44, STIRL2_1:55;
then A41: ( 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 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:4;
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:33;
A46: card (X \ {x}) = k by A3, A4, A15, STIRL2_1:55;
A47: n < k + 1 by A4, A5, A39, NAT_1:44;
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:44;
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:19;
then A51: F1 . n = ((- 1) |^ (n1 + 1)) * (Card_Intersection ((Intersect ((Fy | (X \ {x})),((dom (Fy | (X \ {x}))) --> (Fy . x)))),(n1 + 1))) by NEWTON:6;
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: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, A54, AFINSQ_1:def 3;
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:55;
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:55;
then F2 . n = 0 by AFINSQ_1:36;
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, A26;
then A57: card urngFy = ((Sum XFyX) + (card (Fy . x))) - (Sum XI) by A36, A33, A34, CARD_2:45;
A58: len <%0%> = 1 by AFINSQ_1:33;
len XFyX = card (X \ {x}) by A17;
then A59: len F2 = k + 1 by A58, A16, AFINSQ_1:17;
A60: len XFS = k + 1 by A4, A5;
Sum XFS = addint "**" XFS by AFINSQ_2:50
.= addint "**" (F1 ^ F2) by A37, A59, A38, A60, AFINSQ_2:46
.= Sum (F1 ^ F2) by AFINSQ_2:50 ;
hence card (union (rng Fy)) = Sum XFS by A32, A57; :: thesis:

end;

A61: S₁[ 0 ]

proof

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

end;

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