let X be finite set ; ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
set S1 = { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> (id X) . x ) ) } ;
set S2 = { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) } ;
A1:
{ h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) } c= { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> (id X) . x ) ) }
A4:
( dom (id X) = X & rng (id X) = X )
;
{ h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> (id X) . x ) ) } c= { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) }
then
{ h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> (id X) . x ) ) } = { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) }
by A1;
hence
ex XF being XFinSequence of INT st
( Sum XF = card { h where h is Function of X,X : ( h is one-to-one & ( for x being set st x in X holds
h . x <> x ) ) } & dom XF = (card X) + 1 & ( for n being Nat st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) !)) / (n !) ) )
by A4, Th61; verum