let X, Y be finite set ; :: thesis: ( not X is empty & not Y is empty implies ex F being XFinSequence of st
( dom F = (card Y) + 1 & Sum F = card { f where f is Function of X,Y : f is onto } & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) ) )
assume A1: ( not X is empty & not Y is empty ) ; :: thesis: ex F being XFinSequence of st
( dom F = (card Y) + 1 & Sum F = card { f where f is Function of X,Y : f is onto } & ( for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
set Onto = { f where f is Function of X,Y : f is onto } ;
consider F being XFinSequence of such that
A2: dom F = card Y and
A3: ((card Y) |^ (card X)) - (Sum F) = card { f where f is Function of X,Y : f is onto } and
A4: for n being Element of NAT st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) by A1, Lm4;
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = (- 1) * (F . n);
A5: for k being Element of NAT st k in card Y holds
ex x being Element of INT st S₁[k,x]

proof

let k be Element of NAT ; :: thesis: ( k in card Y implies ex x being Element of INT st S₁[k,x] )
assume k in card Y ; :: thesis: ex x being Element of INT st S₁[k,x]
( S₁[k,(- 1) * (F . k)] & (- 1) * (F . k) is Element of INT ) by INT_1:def 2;
hence ex x being Element of INT st S₁[k,x] ; :: thesis: verum

end;

consider F1 being XFinSequence of such that
A6: dom F1 = card Y and
A7: for k being Element of NAT st k in card Y holds
S₁[k,F1 . k] from STIRL2_1:sch 6(A5);
reconsider c = (card Y) |^ (card X) as Element of INT by INT_1:def 2;
reconsider GF1 = <%c%> ^ F1 as XFinSequence of ;
take GF1 ; :: thesis: ( dom GF1 = (card Y) + 1 & Sum GF1 = card { f where f is Function of X,Y : f is onto } & ( for n being Element of NAT st n in dom GF1 holds
GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
( len F1 = card Y & len <%c%> = 1 ) by A6, AFINSQ_1:36;
hence A8: dom GF1 = (card Y) + 1 by AFINSQ_1:def 4; :: thesis: ( Sum GF1 = card { f where f is Function of X,Y : f is onto } & ( for n being Element of NAT st n in dom GF1 holds
GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
for n being Element of NAT st n in dom F holds
(- 1) * (F . n) = F1 . n by A2, A7;
then ( (- 1) * (Sum F) = Sum F1 & (- 1) * (Sum F) = - (Sum F) ) by A2, A6, Th64;
then c - (Sum F) = c + (Sum F1)
.= addint . c,(Sum F1) by GR_CY_1:14
.= addint . (addint "**" <%c%>),(addint "**" F1) by STIRL2_1:44
.= Sum GF1 by STIRL2_1:47 ;
hence Sum GF1 = card { f where f is Function of X,Y : f is onto } by A3; :: thesis: for n being Element of NAT st n in dom GF1 holds
GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))
let n be Element of NAT ; :: thesis: ( n in dom GF1 implies GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) )
assume A9: n in dom GF1 ; :: thesis: GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))

now

per cases ( n = 0 or n > 0 ) ;

suppose n = 0 ; :: thesis: GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))

then ( (- 1) |^ n = 1 & (card Y) choose n = 1 & ((card Y) - n) |^ (card X) = c & GF1 . n = c ) by AFINSQ_1:39, NEWTON:9, NEWTON:29;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ; :: thesis: verum

end;

suppose n > 0 ; :: thesis: GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
n < (card Y) + 1 by A8, A9, NAT_1:45;
then n1 + 1 <= card Y by NAT_1:13;
then n1 < card Y by NAT_1:13;
then ( n1 in dom F1 & len <%c%> = 1 ) by A6, AFINSQ_1:36, NAT_1:45;
then A10: ( GF1 . (n1 + 1) = F1 . n1 & n1 in card Y ) by A6, AFINSQ_1:def 4;
then A11: ( GF1 . (n1 + 1) = (- 1) * (F . n1) & n1 + 1 = n & ((card Y) - n1) - 1 = (card Y) - n & F . n1 = (((- 1) |^ n1) * ((card Y) choose (n1 + 1))) * ((((card Y) - n1) - 1) |^ (card X)) ) by A2, A4, A7;
(- 1) * ((- 1) |^ n1) = (- 1) |^ n by A10, NEWTON:11;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) by A11; :: thesis: verum

end;

end;

end;

hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ; :: thesis: verum