let Fy be finite-yielding Function; :: thesis: for X being finite set ex 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))) ) )
let X be finite set ; :: thesis: ex 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))) ) )
defpred S₁[ set , set ] means for n being Nat st n = $1 holds
$2 = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1)));
A1: for k being Nat st k in Segm (card X) holds
ex x being Element of INT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Segm (card X) implies ex x being Element of INT st S₁[k,x] )
assume k in Segm (card X) ; :: thesis: ex x being Element of INT st S₁[k,x]
reconsider C = ((- 1) |^ k) * (Card_Intersection (Fy,(k + 1))) as Element of INT by INT_1:def 2;
take C ; :: thesis: S₁[k,C]
thus S₁[k,C] ; :: thesis: verum

end;

consider XFS being XFinSequence of INT such that
A2: ( dom XFS = Segm (card X) & ( for k being Nat st k in Segm (card X) holds
S₁[k,XFS . k] ) ) from STIRL2_1:sch 5(A1);
take XFS ; :: thesis: ( dom XFS = card X & ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) )
thus ( dom XFS = card X & ( for n being Nat st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection (Fy,(n + 1))) ) ) by A2; :: thesis: verum