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 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 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 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 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 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 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 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 Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) ) )
assume A2: ( dom XF = card X & ( for n being 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 Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
defpred S1[ object , object ] means for n being Nat st n = $1 holds
$2 = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1));
A3: for x being object st x in card X holds
ex y being object st
( y in INT & S1[x,y] )
proof
A4: card X is Subset of NAT by STIRL2_1:8;
let x be object ; :: thesis: ( x in card X implies ex y being object st
( y in INT & S1[x,y] ) )
assume x in card X ; :: thesis: ex y being object st
( y in INT & S1[x,y] )
then reconsider x9 = x as Element of NAT by A4;
reconsider xx = ((- 1) |^ x9) * (XF . x9) as Integer ;
reconsider ch = (card X) choose (x9 + 1) as Integer ;
take xx * ch ; :: thesis: ( xx * ch in INT & S1[x,xx * ch] )
thus ( xx * ch in INT & S1[x,xx * ch] ) by INT_1:def 2; :: thesis: verum
end;
consider F being Function of (card X),INT such that
A5: for x being object st x in card X holds
S1[x,F . x] from FUNCT_2:sch 1(A3);
 A6: dom F = card X by FUNCT_2:def 1;
then reconsider F = F as XFinSequence by AFINSQ_1:5;
reconsider F = F as XFinSequence of INT ;
take F ; :: thesis: ( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) )
for n being Nat st n in dom F holds
F . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1)))
proof
let n be Nat; :: thesis: ( n in dom F implies F . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) )
assume A7: 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, A6, A7;
then A8: Card_Intersection (Fy,(n + 1)) = (XF . n) * ((card X) choose (n + 1)) by A1, Th56;
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) by A5, A6, A7;
hence F . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) by A8; :: thesis: verum
end;
hence ( dom F = card X & card (union (rng Fy)) = Sum F & ( for n being Nat st n in dom F holds
F . n = (((- 1) |^ n) * (XF . n)) * ((card X) choose (n + 1)) ) ) by A1, A5, A6, Th55; :: thesis: verum