let X, Y be finite set ; :: thesis: ( not X is empty & not Y is empty implies ex F being XFinSequence of INT 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 INT 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)) ) )
reconsider c = (card Y) |^ (card X) as Element of INT by INT_1:def 2;
A2: len <%c%> = 1 by AFINSQ_1:36;
set Onto = { f where f is Function of X,Y : f is onto } ;
consider F being XFinSequence of INT such that
A3: dom F = card Y and
A4: ((card Y) |^ (card X)) - (Sum F) = card { f where f is Function of X,Y : f is onto } and
A5: 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);
A6: 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 INT such that
A7: dom F1 = card Y and
A8: for k being Element of NAT st k in card Y holds
S₁[k,F1 . k] from STIRL2_1:sch 6(A6);
reconsider GF1 = <%c%> ^ F1 as XFinSequence of INT ;
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 by A7;
hence A9: dom GF1 = (card Y) + 1 by A2, 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 A3, A8;
then (- 1) * (Sum F) = Sum F1 by A3, A7, Th64;
then c - (Sum F) = c + (Sum F1)
.= addint . c,(Sum F1) by BINOP_2:def 20
.= 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 A4; :: 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 A10: 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 A11: 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 ) by NEWTON:9, NEWTON:29;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) by A11, AFINSQ_1:39; :: 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 A9, A10, NAT_1:45;
then n1 + 1 <= card Y by NAT_1:13;
then n1 < card Y by NAT_1:13;
then A12: n1 in dom F1 by A7, NAT_1:45;
then A13: F . n1 = (((- 1) |^ n1) * ((card Y) choose (n1 + 1))) * ((((card Y) - n1) - 1) |^ (card X)) by A3, A5, A7;
len <%c%> = 1 by AFINSQ_1:36;
then A14: GF1 . (n1 + 1) = F1 . n1 by A12, AFINSQ_1:def 4;
then A15: (- 1) * ((- 1) |^ n1) = (- 1) |^ n by NEWTON:11;
GF1 . (n1 + 1) = (- 1) * (F . n1) by A7, A8, A12, A14;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) by A13, A15; :: thesis: verum

end;

end;

end;

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