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 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 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 A1: ( dom F' = X & F' is one-to-one ) ; :: thesis: ex XF being XFinSequence of 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, 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 such that
A2: dom Xf = card X and
A3: ((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
A4: for n being Element of NAT st n in dom Xf holds
Xf . n = (((- 1) |^ n) * ((card X) ! )) / ((n + 1) ! ) by A1, Lm5;
defpred S₁[ set , set ] means for n being Element of NAT st n = $1 holds
$2 = (- 1) * (Xf . n);
A5: 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 such that
A6: dom F1 = card X and
A7: for k being Element of NAT st k in card X holds
S₁[k,F1 . k] from STIRL2_1:sch 6(A5);
reconsider c = (card X) ! as Element of INT by INT_1:def 2;
reconsider XF = <%c%> ^ F1 as XFinSequence of ;
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 A2, A7;
then ( (- 1) * (Sum Xf) = Sum F1 & (- 1) * (Sum Xf) = - (Sum Xf) ) by A2, A6, Th64;
then c - (Sum Xf) = c + (Sum F1)
.= addint . c,(Sum F1) by GR_CY_1:14
.= 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 A3; :: 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 & len <%c%> = 1 ) by A6, AFINSQ_1:36;
hence A8: dom XF = (card X) + 1 by 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 A9: n in dom XF ; :: thesis: XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! )

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

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

then ( (- 1) |^ n = 1 & n ! = 1 & XF . n = c ) by AFINSQ_1:39, NEWTON:9, NEWTON:18;
hence XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ; :: 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;
n < (card X) + 1 by A8, A9, NAT_1:45;
then n1 + 1 <= card X by NAT_1:13;
then n1 < card X by NAT_1:13;
then n1 < len F1 by A6;
then X: n1 in dom F1 by NAT_1:45;
len <%c%> = 1 by AFINSQ_1:36;
then ( XF . (n1 + 1) = F1 . n1 & n1 in card X ) by A6, X, AFINSQ_1:def 4;
then ( XF . (n1 + 1) = (- 1) * (Xf . n1) & n1 + 1 = n & Xf . n1 = (((- 1) |^ n1) * ((card X) ! )) / ((n1 + 1) ! ) ) by A2, A4, A7;
then ( XF . n = ((- 1) * (((- 1) |^ n1) * ((card X) ! ))) / (n ! ) & n1 + 1 = n ) by XCMPLX_1:75;
then ( (- 1) * ((- 1) |^ n1) = (- 1) |^ n & XF . n = (((- 1) * ((- 1) |^ n1)) * ((card X) ! )) / (n ! ) ) by NEWTON:11;
hence XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ; :: thesis: verum

end;

end;