let X be finite set ; :: thesis: 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 ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { 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 ) ) } or x in { 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 ) ) } )
assume x in { 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 ) ) } ; :: thesis: x in { 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 ) ) }
then consider h being Function of X,X such that
A2: ( h = x & h is one-to-one ) and
A3: for y being set st y in X holds
h . y <> y ;
for y being set st y in X holds
(id X) . y <> h . y by A3, FUNCT_1:17;
hence x in { 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 ) ) } by A2; :: thesis: verum

end;

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 ) ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { 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 ) ) } or x in { 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 ) ) } )
assume x in { 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 ) ) } ; :: thesis: x in { 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 consider h being Function of X,X such that
A5: ( h = x & h is one-to-one ) and
A6: for y being set st y in X holds
h . y <> (id X) . y ;

now :: thesis: for y being set st y in X holds
h . y <> y

let y be set ; :: thesis: ( y in X implies h . y <> y )
assume A7: y in X ; :: thesis: h . y <> y
(id X) . y = y by A7, FUNCT_1:17;
hence h . y <> y by A6, A7; :: thesis: verum

end;

hence x in { 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 A5; :: thesis: verum

end;

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; :: thesis: verum