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 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 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:33;
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 Nat st n in dom F holds
F . n = (((- 1) |^ n) * ((card Y) choose (n + 1))) * ((((card Y) - n) - 1) |^ (card X)) by A1, Lm3;
set F1 = (- 1) (#) F;
reconsider F1 = (- 1) (#) F as XFinSequence of INT ;
A6: ( dom F1 = dom F & dom F = card Y ) by A3, VALUED_1:def 5;
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 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 A7: dom GF1 = (card Y) + 1 by A2, AFINSQ_1:def 3; :: 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:64;
then c - (Sum F) = c + (Sum F1)
.= addint . (c,(Sum F1)) by BINOP_2:def 20
.= addint . ((addint "**" <%c%>),(Sum F1)) by AFINSQ_2:37
.= addint . ((addint "**" <%c%>),(addint "**" F1)) by AFINSQ_2:50
.= addint "**" GF1 by AFINSQ_2:42
.= Sum GF1 by AFINSQ_2:50 ;
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 A8: n in dom GF1 ; :: thesis: GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X))

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

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

suppose A9: 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:4, NEWTON:19;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) by A9, AFINSQ_1:35; :: 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 < len GF1 by A8, AFINSQ_1:86;
then n < (card Y) + 1 by A7;
then n1 + 1 <= card Y by NAT_1:13;
then n1 < card Y by NAT_1:13;
then n1 < len F1 by A6;
then A10: n1 in dom F1 by AFINSQ_1:86;
then A11: F . n1 = (((- 1) |^ n1) * ((card Y) choose (n1 + 1))) * ((((card Y) - n1) - 1) |^ (card X)) by A5, A6;
len <%c%> = 1 by AFINSQ_1:33;
then A12: GF1 . (n1 + 1) = F1 . n1 by A10, AFINSQ_1:def 3;
then A13: (- 1) * ((- 1) |^ n1) = (- 1) |^ n by NEWTON:6;
GF1 . (n1 + 1) = (- 1) * (F . n1) by A12, VALUED_1:6;
hence GF1 . n = (((- 1) |^ n) * ((card Y) choose n)) * (((card Y) - n) |^ (card X)) by A11, A13; :: thesis: verum

end;

end;

end;

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