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 Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
let F' be Function; :: thesis: ( dom F' = X & F' is one-to-one implies 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 Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) ) )
assume that
A1: dom F' = X and
A2: F' is one-to-one ; :: thesis: 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 Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
X, rng F' are_equipotent by A1, A2, WELLORD2:def 4;
then card X = card (rng F') by CARD_1:21;
then reconsider rngF = rng F' as finite set ;
reconsider F = F' as Function of X,rngF by A1, FUNCT_2:3;
set S = { 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 ) ) } ;
rng F' = 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 F' : ( h is one-to-one & ( for x being set st x in X holds
h . x <> F' . x ) ) } and
A5: for n being Element of NAT st n in dom Xf holds
Xf . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) by A1, A2, Lm5;
reconsider c = (card X) ! as Element of INT by INT_1:def 2;
A6: len <%c%> = 1 by AFINSQ_1:36;
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = (- 1) * (Xf . n);
A7: for k being Element of NAT st k in card X holds
ex x being Element of INT st S₁[k,x]

proof

let k be Element of NAT ; :: thesis: ( k in card X implies ex x being Element of INT st S₁[k,x] )
assume k in card X ; :: thesis: ex x being Element of INT st S₁[k,x]
( S₁[k,(- 1) * (Xf . k)] & (- 1) * (Xf . 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
A8: dom F1 = card X and
A9: for k being Element of NAT st k in card X holds
S₁[k,F1 . k] from STIRL2_1:sch 6(A7);
reconsider XF = <%c%> ^ F1 as XFinSequence of INT ;
take XF ; :: thesis: ( 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 Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
for n being Element of NAT st n in dom Xf holds
(- 1) * (Xf . n) = F1 . n by A3, A9;
then (- 1) * (Sum Xf) = Sum F1 by A3, A8, Th64;
then c - (Sum Xf) = c + (Sum F1)
.= addint . c,(Sum F1) by BINOP_2:def 20
.= addint . (addint "**" <%c%>),(addint "**" F1) by STIRL2_1:44
.= Sum XF by STIRL2_1:47 ;
hence 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 ) ) } by A4; :: thesis: ( dom XF = (card X) + 1 & ( for n being Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) )
len F1 = card X by A8;
hence A10: dom XF = (card X) + 1 by A6, AFINSQ_1:def 4; :: thesis: for n being Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! )
let n be Element of NAT ; :: thesis: ( n in dom XF implies XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) )
assume A11: n in dom XF ; :: thesis: XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! )

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

suppose A12: n = 0 ; :: thesis: XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! )

then (- 1) |^ n = 1 by NEWTON:9;
hence XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) by A12, AFINSQ_1:39, NEWTON:18; :: thesis: verum

end;

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

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
n1 + 1 = n ;
then A13: (- 1) * ((- 1) |^ n1) = (- 1) |^ n by NEWTON:11;
n < (card X) + 1 by A10, A11, NAT_1:45;
then n1 + 1 <= card X by NAT_1:13;
then n1 < len F1 by A8, NAT_1:13;
then A14: n1 in dom F1 by NAT_1:45;
len <%c%> = 1 by AFINSQ_1:36;
then XF . (n1 + 1) = F1 . n1 by A14, AFINSQ_1:def 4;
then A15: XF . (n1 + 1) = (- 1) * (Xf . n1) by A8, A9, A14;
Xf . n1 = (((- 1) |^ n1) * ((card X) ! )) / ((n1 + 1) ! ) by A3, A5, A8, A14;
then XF . n = ((- 1) * (((- 1) |^ n1) * ((card X) ! ))) / (n ! ) by A15, XCMPLX_1:75;
hence XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) by A13; :: thesis: verum

end;

end;