let X be finite set ; :: thesis: ex XF being XFinSequence of 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 Element of 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 <> (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 set ; :: 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 A2: 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 ) ) }
consider h being Function of X,X such that
A3: ( h = x & h is one-to-one & ( for y being set st y in X holds
h . y <> (id X) . y ) ) by A2;

now

let y be set ; :: thesis: ( y in X implies h . y <> y )
assume A4: y in X ; :: thesis: h . y <> y
(id X) . y = y by A4, FUNCT_1:34;
hence h . y <> y by A3, A4; :: 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 A3; :: thesis: verum

end;

A5: { 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 set ; :: 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 A6: 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 ) ) }
consider h being Function of X,X such that
A7: ( h = x & h is one-to-one & ( for y being set st y in X holds
h . y <> y ) ) by A6;

now

let y be set ; :: thesis: ( y in X implies (id X) . y <> h . y )
assume A8: y in X ; :: thesis: (id X) . y <> h . y
(id X) . y = y by A8, FUNCT_1:34;
hence (id X) . y <> h . y by A7, A8; :: 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 <> (id X) . x ) ) } by A7; :: thesis: verum

end;

( dom (id X) = X & rng (id X) = X & id X is one-to-one ) by RELAT_1:71;
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 ) ) } & ex XF being XFinSequence of 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 <> (id X) . 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 ! ) ) ) ) by A1, A5, Th73, XBOOLE_0:def 10;
hence ex XF being XFinSequence of 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 Element of NAT st n in dom XF holds
XF . n = (((- 1) |^ n) * ((card X) ! )) / (n ! ) ) ) ; :: thesis: verum