let X be finite set ; :: thesis: for F being Function st dom F = X & F is one-to-one holds
ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,(rng F) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F . x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
let F9 be Function; :: thesis: ( dom F9 = X & F9 is one-to-one implies ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) ) )
assume that
A1: dom F9 = X and
A2: F9 is one-to-one ; :: thesis: ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
X, rng F9 are_equipotent by A1, A2, WELLORD2:def 4;
then card X = card (rng F9) by CARD_1:5;
then reconsider rngF = rng F9 as finite set ;
reconsider F = F9 as Function of X,rngF by A1, FUNCT_2:1;
set S = { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } ;
rng F9 = rng F ;
then consider Xf being XFinSequence of INT such that
A3: dom Xf = card X and
A4: ((card X) !) - (Sum Xf) = card { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } and
A5: for n being Nat st n in dom Xf holds
Xf . n = (((- 1) |^ n) * ((card X) !)) / ((n + 1) !) by A1, A2, Lm4;
reconsider c = (card X) ! as Element of INT by INT_1:def 2;
A6: len <%c%> = 1 by AFINSQ_1:33;
set F1 = (- 1) (#) Xf;
A7: dom ((- 1) (#) Xf) = card X by A3, VALUED_1:def 5;
reconsider F1 = (- 1) (#) Xf as XFinSequence of INT ;
set XF = <%c%> ^ F1;
take <%c%> ^ F1 ; :: thesis: ( Sum (<%c%> ^ F1) = card { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } & dom (<%c%> ^ F1) = (card X) + 1 & ( for n being Nat st n in dom (<%c%> ^ F1) holds
(<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
(- 1) * (Sum Xf) = Sum F1 by AFINSQ_2:64;
then c - (Sum Xf) = 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 "**" (<%c%> ^ F1) by AFINSQ_2:42
.= Sum (<%c%> ^ F1) by AFINSQ_2:50 ;
hence Sum (<%c%> ^ F1) = card { h where h is Function of X,(rng F9) : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F9 . x ) ) } by A4; :: thesis: ( dom (<%c%> ^ F1) = (card X) + 1 & ( for n being Nat st n in dom (<%c%> ^ F1) holds
(<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
len F1 = card X by A3, VALUED_1:def 5;
hence A8: dom (<%c%> ^ F1) = (card X) + 1 by A6, AFINSQ_1:def 3; :: thesis: for n being Nat st n in dom (<%c%> ^ F1) holds
(<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !)
let n be Nat; :: thesis: ( n in dom (<%c%> ^ F1) implies (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !) )
assume A9: n in dom (<%c%> ^ F1) ; :: thesis: (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !)

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

suppose A10: n = 0 ; :: thesis: (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !)

then (- 1) |^ n = 1 by NEWTON:4;
hence (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !) by A10, AFINSQ_1:35, NEWTON:12; :: thesis: verum

end;

suppose n > 0 ; :: thesis: (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !)

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
n1 + 1 = n ;
then A11: (- 1) * ((- 1) |^ n1) = (- 1) |^ n by NEWTON:6;
n < len (<%c%> ^ F1) by A9, AFINSQ_1:86;
then n < (card X) + 1 by A8;
then n1 + 1 <= card X by NAT_1:13;
then n1 < len F1 by A7, NAT_1:13;
then A12: n1 in dom F1 by AFINSQ_1:86;
len <%c%> = 1 by AFINSQ_1:33;
then (<%c%> ^ F1) . (n1 + 1) = F1 . n1 by A12, AFINSQ_1:def 3;
then A13: (<%c%> ^ F1) . (n1 + 1) = (- 1) * (Xf . n1) by VALUED_1:6;
Xf . n1 = (((- 1) |^ n1) * ((card X) !)) / ((n1 + 1) !) by A3, A5, A7, A12;
then (<%c%> ^ F1) . n = ((- 1) * (((- 1) |^ n1) * ((card X) !))) / (n !) by A13, XCMPLX_1:74;
hence (<%c%> ^ F1) . n = (((- 1) |^ n) * ((card X) !)) / (n !) by A11; :: thesis: verum

end;

end;