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 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 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 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 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;
set F1 = (- 1) (#) F;
rng ((- 1) (#) F) c= INT by VALUED_0:def 5;
then reconsider F1 = (- 1) (#) F as XFinSequence of by RELAT_1:def 19;
A7: ( dom F1 = dom F & dom F = card Y ) by A3, VALUED_1:def 5;
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 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 A3, VALUED_1:def 5;
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 Nat st n in dom GF1 holds
GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) ) )
(- 1) * (Sum F) = Sum F1 by AFINSQ_2:76;
then c - (Sum F) = c + (Sum F1)
.= addint . (c,(Sum F1)) by BINOP_2:def 20
.= addint . ((addint "**" <%c%>),(Sum F1)) by AFINSQ_2:49
.= addint . ((addint "**" <%c%>),(addint "**" F1)) by AFINSQ_2:62
.= addint "**" GF1 by AFINSQ_2:54
.= Sum GF1 by AFINSQ_2:62 ;
hence Sum GF1 = card { f where f is Function of X,Y : f is onto } by A4; :: thesis: for n being Nat st n in dom GF1 holds
GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))
let n be 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 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 VALUED_1:6, 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