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 Element of 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 Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) )
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1));
A1: for k being Element of NAT st k in card X holds
ex x being Element of INT st S₁[k,x]

proof

let k be Element of 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 by INT_1:def 2;
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 and
A3: for k being Element of NAT st k in card X holds
S₁[k,XFS . k] from STIRL2_1:sch 6(A1);
take XFS ; :: thesis: ( dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) )
thus ( dom XFS = card X & ( for n being Element of NAT st n in dom XFS holds
XFS . n = ((- 1) |^ n) * (Card_Intersection Fy,(n + 1)) ) ) by A2, A3; :: thesis: verum