let Fy be finite-yielding Function; :: thesis: for X being finite set ex 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)) ) )
let X be finite set ; :: thesis: ex 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)) ) )
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 card X holds
ex x being Element of INT st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in card X implies ex x being Element of INT st S₁[k,x] )
assume k in 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 ;
take C ; :: thesis: S₁[k,C]
thus S₁[k,C] ; :: thesis: verum

end;

consider XFS being XFinSequence of such that
A2: ( dom XFS = card X & ( for k being Nat st k in 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