let Fy be finite-yielding Function; :: thesis: for X being finite set st dom Fy = X holds
for XF being XFinSequence of NAT st dom XF = card X & ( for n being Element of NAT st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) ) holds
ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
let X be finite set ; :: thesis: ( dom Fy = X implies for XF being XFinSequence of NAT st dom XF = card X & ( for n being Element of NAT st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) ) holds
ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) ) )
assume A1: dom Fy = X ; :: thesis: for XF being XFinSequence of NAT st dom XF = card X & ( for n being Element of NAT st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) ) holds
ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
let XF be XFinSequence of NAT ; :: thesis: ( dom XF = card X & ( for n being Element of NAT st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) ) implies ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) ) )
assume that
A2: dom XF = card X and
A3: for n being Element of NAT st n in dom XF holds
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) ; :: thesis: ex F being XFinSequence of INT st
( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1));
A4: for x being set st x in card X holds
ex y being set st
( y in INT & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in card X implies ex y being set st
( y in INT & S₁[x,y] ) )
assume A5: x in card X ; :: thesis: ex y being set st
( y in INT & S₁[x,y] )
card X is Subset of NAT by STIRL2_1:8;
then reconsider x' = x as Element of NAT by A5;
reconsider xx = ((- 1) |^ x') * (XF . x') as Integer ;
reconsider ch = (card X) choose (x' + 1) as Integer ;
take xx * ch ; :: thesis: ( xx * ch in INT & S₁[x,xx * ch] )
thus ( xx * ch in INT & S₁[x,xx * ch] ) by INT_1:def 2; :: thesis: verum

end;

consider F being Function of card X, INT such that
A6: for x being set st x in card X holds
S₁[x,F . x] from FUNCT_2:sch 1(A4);
A7: ( dom F = card X & rng F c= INT ) by FUNCT_2:def 1;
then reconsider F = F as XFinSequence by AFINSQ_1:7;
reconsider F = F as XFinSequence of INT by A7, ORDINAL1:def 8;
take F ; :: thesis: ( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
for n being Element of NAT st n in dom F holds
F . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1))

proof

let n be Element of NAT ; :: thesis: ( n in dom F implies F . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) )
assume A8: n in dom F ; :: thesis: F . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1))
ex x, y being set st
( x <> y & ( for f being Function st f in Choose X,(n + 1),x,y holds
card (Intersection Fy,f,x) = XF . n ) ) by A2, A3, A7, A8;
then ( Card_Intersection Fy,(n + 1) = (XF . n) * ((card X) choose (n + 1)) & F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) by A1, A6, A7, A8, Th68;
hence F . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ; :: thesis: verum

end;

hence ( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) ) by A1, A6, A7, Th67; :: thesis: verum