:: CARDFIN2 semantic presentation

begin


registration
let c be real number ;
cluster exp_R c ->  positive ;
coherence
 exp_R c is positive by SIN_COS:55;
end;

registration
cluster number_e  ->  positive ;
coherence
 number_e is positive by TAYLOR_1:11;
end;

theorem Th1: :: CARDFIN2:1
id {} is without_fixpoints
proof
assume  id {} is with_fixpoint ; ::_thesis: contradiction
then consider y being set  such that
A1: y is_a_fixpoint_of id {} by ABIAN:def_5;
 y in dom (id {}) by A1, ABIAN:def_3;
hence  contradiction ; ::_thesis: verum
end;

theorem Th2: :: CARDFIN2:2
for c being real number st c < 0 holds
exp_R c < 1
proof
let c be real number ; ::_thesis: ( c < 0 implies exp_R c < 1 )
assume  c < 0 ; ::_thesis: exp_R c < 1
then  ( exp_R c <= 1 & exp_R c <> 1 ) by SIN_COS:53, SIN_COS7:29;
hence  exp_R c < 1 by XXREAL_0:1; ::_thesis: verum
end;

begin

definition
let n be real number ;
func round n ->  Integer equals :: CARDFIN2:def 1
[\(n + (1 / 2))/];
coherence
 [\(n + (1 / 2))/] is Integer ;
end;

:: deftheorem  defines round CARDFIN2:def_1_:_
 for n being real number holds round n = [\(n + (1 / 2))/];

theorem :: CARDFIN2:3
for a being Integer holds round a = a
proof
let a be Integer; ::_thesis: round a = a
 a - (1 / 2) < a - 0 by XREAL_1:6;
then  ( a + 0 <= a + (1 / 2) & (a + (1 / 2)) - 1 < a - 0 ) by XREAL_1:6;
hence  round a = a by INT_1:def_6; ::_thesis: verum
end;

theorem Th4: :: CARDFIN2:4
for a being Integer
for b being real number st |.(a - b).| < 1 / 2 holds
a = round b
proof
let a be Integer; ::_thesis: for b being real number st |.(a - b).| < 1 / 2 holds
a = round b
let b be real number ; ::_thesis: ( |.(a - b).| < 1 / 2 implies a = round b )
assume A1: |.(a - b).| < 1 / 2 ; ::_thesis: a = round b
then  a - b < 1 / 2 by SEQ_2:1;
then A2: (a - b) + b < (1 / 2) + b by XREAL_1:8;
 - (1 / 2) < a - b by A1, SEQ_2:1;
then  - (a - b) < - (- (1 / 2)) by XREAL_1:24;
then  (b - a) + a < (1 / 2) + a by XREAL_1:8;
then  b - (1 / 2) < (a + (1 / 2)) - (1 / 2) by XREAL_1:14;
then  (b + (1 / 2)) - 1 < a ;
hence  a = round b by A2, INT_1:def_6; ::_thesis: verum
end;

begin

theorem Th5: :: CARDFIN2:5
for n being Nat
for a, b being real number st a < b holds
ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
proof
let n be Nat; ::_thesis: for a, b being real number st a < b holds
ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
let a, b be real number ; ::_thesis: ( a < b implies ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) )
assume A1: a < b ; ::_thesis: ex c being real number st
( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
set f = exp_R ;
set Z = [#] REAL;
A2: n in NAT by ORDINAL1:def_12;
then A3: exp_R is_differentiable_on n, [#] REAL by TAYLOR_2:10;
 (diff (exp_R,([#] REAL))) . n = exp_R | ([#] REAL) by A2, TAYLOR_2:6;
then A4: ((diff (exp_R,([#] REAL))) . n) | [.a,b.] is continuous ;
A5: exp_R is_differentiable_on n + 1,].a,b.[ by TAYLOR_2:10;
 ( a in REAL & b in REAL ) by XREAL_0:def_1;
then consider c being Real such that
A6: c in ].a,b.[ and
A7: exp_R . a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((((diff (exp_R,].a,b.[)) . (n + 1)) . c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) by A1, A3, A4, A5, A2, SIN_COS:47, TAYLOR_1:29;
take  c ; ::_thesis: ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) )
thus  ( c in ].a,b.[ & exp_R a = ((Partial_Sums (Taylor (exp_R,([#] REAL),b,a))) . n) + (((exp_R c) * ((a - b) |^ (n + 1))) / ((n + 1) !)) ) by A7, A6, TAYLOR_2:7; ::_thesis: verum
end;

theorem Th6: :: CARDFIN2:6
for n being positive Nat
for c being real number st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
proof
let n be positive Nat; ::_thesis: for c being real number st c < 0 holds
|.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
let c be real number ; ::_thesis: ( c < 0 implies |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 )
 n >= 0 + 1 by NAT_1:13;
then  n + 1 >= 1 + 1 by XREAL_1:6;
then A1: (exp_R c) / (n + 1) <= (exp_R c) / 2 by XREAL_1:118;
assume  c < 0 ; ::_thesis: |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2
then  (exp_R c) / 2 < 1 / 2 by Th2, XREAL_1:74;
then A2: (exp_R c) / (n + 1) < 1 / 2 by A1, XXREAL_0:2;
A3: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
proof
percases ( n is even or n is odd ) ;
supposeA4: n is even ; ::_thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
A5: (- 1) |^ n = (- 1) to_power n
.= 1 to_power n by A4, POWER:47
.= 1 by NEWTON:10 ;
 - (1 / 2) < (exp_R c) / (n + 1) ;
hence  |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A5, A2, SEQ_2:1; ::_thesis: verum
end;
supposeA6: n is odd ; ::_thesis: |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2
A7: (- 1) |^ n = (- 1) to_power n
.= - 1 by A6, FIB_NUM2:2 ;
 - (1 / 2) < - ((exp_R c) / (n + 1)) by A2, XREAL_1:24;
hence  |.(((exp_R c) * ((- 1) |^ n)) / (n + 1)).| < 1 / 2 by A7, SEQ_2:1; ::_thesis: verum
end;
end;
end;
((exp_R c) * ((- 1) |^ n)) / (n + 1) = ((exp_R c) * ((- 1) * (((- 1) |^ n) * (- 1)))) / (n + 1)
.= ((exp_R c) * ((- 1) * ((- 1) |^ (n + 1)))) / (n + 1) by NEWTON:6
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (1 / (n + 1)))
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * (((n !) / (n !)) / (n + 1))) by XCMPLX_1:60
.= - (((exp_R c) * ((- 1) |^ (n + 1))) * ((n !) / ((n !) * (n + 1)))) by XCMPLX_1:78
.= - ((((exp_R c) * ((- 1) |^ (n + 1))) * (n !)) / ((n + 1) * (n !)))
.= - ((((n !) * (exp_R c)) * ((- 1) |^ (n + 1))) / ((n + 1) !)) by NEWTON:15 ;
hence  |.(- ((n !) * (((exp_R c) * ((- 1) |^ (n + 1))) / ((n + 1) !)))).| < 1 / 2 by A3; ::_thesis: verum
end;

definition
let s be set ;
func derangements s ->  set  equals :: CARDFIN2:def 2
 {  f where f is Permutation of s : f is without_fixpoints  }  ;
coherence
  {  f where f is Permutation of s : f is without_fixpoints  }  is set ;
end;

:: deftheorem  defines derangements CARDFIN2:def_2_:_
 for s being set holds derangements s =  {  f where f is Permutation of s : f is without_fixpoints  }  ;

registration
let s be finite set ;
cluster derangements s ->  finite ;
coherence
 derangements s is finite
proof
A1: card  {  F where F is Function of s,s : F is Permutation of s  }  = (card s) ! by CARD_FIN:8;
 derangements s c=  {  F where F is Function of s,s : F is Permutation of s  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in derangements s or x in  {  F where F is Function of s,s : F is Permutation of s  }  )
assume  x in derangements s ; ::_thesis: x in  {  F where F is Function of s,s : F is Permutation of s  }
then  ex f being Permutation of s st
( x = f & f is without_fixpoints ) ;
hence  x in  {  F where F is Function of s,s : F is Permutation of s  }  ; ::_thesis: verum
end;
then  card (derangements s) c= (card s) ! by A1, CARD_1:11;
hence  derangements s is finite ; ::_thesis: verum
end;
end;

theorem Th7: :: CARDFIN2:7
for s being finite set holds derangements s =  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }
proof
let s be finite set ; ::_thesis: derangements s =  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }
set xx =  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  ;
hereby  :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis:  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  c= derangements s
let x be set ; ::_thesis: ( x in derangements s implies x in  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  )
assume  x in derangements s ; ::_thesis: x in  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }
then consider f being Permutation of s such that
A1: ( x = f & f is without_fixpoints ) ;
now__::_thesis:_for_y_being_set_st_y_in_s_holds_
f_._y_<>_y
let y be set ; ::_thesis: ( y in s implies f . y <> y )
 not y is_a_fixpoint_of f by A1, ABIAN:def_5;
hence  ( y in s implies f . y <> y ) by ABIAN:def_4; ::_thesis: verum
end;
hence  x in  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  or x in derangements s )
assume  x in  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  ; ::_thesis: x in derangements s
then consider h being Function of s,s such that
A2: ( x = h & h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) ;
 card s = card s ;
then A3: h is onto by A2, STIRL2_1:60;
now__::_thesis:_for_y_being_set_holds_not_y_is_a_fixpoint_of_h
let y be set ; ::_thesis: not y is_a_fixpoint_of h
assume  y is_a_fixpoint_of h ; ::_thesis: contradiction
then  ( y in dom h & h . y = y ) by ABIAN:def_3;
hence  contradiction by A2; ::_thesis: verum
end;
then  h is without_fixpoints by ABIAN:def_5;
hence  x in derangements s by A3, A2; ::_thesis: verum
end;

theorem Th8: :: CARDFIN2:8
for s being non empty finite set ex c being real number st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
proof
let s be non empty finite set ; ::_thesis: ex c being real number st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
set n = card s;
consider XF being XFinSequence of  such that
A1: Sum XF = card  {  h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) )  }  and
A2: dom XF = (card s) + 1 and
A3: for m being Nat st m in dom XF holds
XF . m = (((- 1) |^ m) * ((card s) !)) / (m !) by CARD_FIN:63;
A4: Sum XF = card (derangements s) by A1, Th7;
set T = Taylor (exp_R,([#] REAL),0,(- 1));
consider c being real number  such that
A5: ( c in ].(- 1),0.[ & exp_R (- 1) = ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) + (((exp_R c) * (((- 1) - 0) |^ ((card s) + 1))) / (((card s) + 1) !)) ) by Th5;
 Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) = ((card s) !) (#) (Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) by SERIES_1:9;
then A6: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = ((card s) !) * ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) by SEQ_1:9;
 (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF
proof
consider f being Function of NAT,INT such that
A7: f . 0 = XF . 0 and
A8: for n being Nat st n + 1 < len XF holds
f . (n + 1) = addint . ((f . n),(XF . (n + 1))) and
A9: addint "**" XF = f . ((len XF) - 1) by A2, AFINSQ_2:def_8;
A10: Sum XF = f . ((len XF) - 1) by A9, AFINSQ_2:50;
defpred S1[ Element of NAT ] means ( $1 in (card s) + 1 implies (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . $1 = f . $1 );
A11: S1[ 0 ]
proof
A12: 0 in dom XF by A2, NAT_1:44;
(Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . 0 = (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . 0 by SERIES_1:def_1
.= ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . 0) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) / (0 !)) by TAYLOR_1:def_7
.= ((card s) !) * ((1 * ((- 1) |^ 0)) / (0 !)) by SIN_COS2:13, TAYLOR_2:7
.= (((card s) !) * ((- 1) |^ 0)) / (0 !)
.= f . 0 by A3, A12, A7 ;
hence  S1[ 0 ] ; ::_thesis: verum
end;
A13: for j being Element of NAT st S1[j] holds
S1[j + 1]
proof
let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] )
assume A14: S1[j] ; ::_thesis: S1[j + 1]
set j1 = j + 1;
assume A15: j + 1 in (card s) + 1 ; ::_thesis: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = f . (j + 1)
then A16: j + 1 < (card s) + 1 by NAT_1:44;
then A17: j < (card s) + 1 by NAT_1:13;
(((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . (j + 1) = ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . (j + 1)) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . (j + 1)) . 0) * (((- 1) - 0) |^ (j + 1))) / ((j + 1) !)) by TAYLOR_1:def_7
.= ((card s) !) * ((1 * ((- 1) |^ (j + 1))) / ((j + 1) !)) by SIN_COS2:13, TAYLOR_2:7
.= (((card s) !) * ((- 1) |^ (j + 1))) / ((j + 1) !)
.= XF . (j + 1) by A3, A15, A2 ;
hence (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = (f . j) + (XF . (j + 1)) by A14, A17, NAT_1:44, SERIES_1:def_1
.= addint . ((f . j),(XF . (j + 1))) by BINOP_2:def_20
.= f . (j + 1) by A8, A16, A2 ;
::_thesis: verum
end;
 for j being Element of NAT holds S1[j] from NAT_1:sch_1(A11, A13);
hence  (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF by A10, A2, NAT_1:45; ::_thesis: verum
end;
then A18: (card (derangements s)) + (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) = ((card s) !) * (exp_R (- 1)) by A4, A5, A6
.= ((card s) !) * (1 / (exp_R 1)) by TAYLOR_1:4
.= ((card s) !) / number_e by IRRAT_1:def_7 ;
take  c ; ::_thesis: ( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
thus  c in ].(- 1),0.[ by A5; ::_thesis: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !)))
thus  (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by A18; ::_thesis: verum
end;

theorem Th9: :: CARDFIN2:9
for s being non empty finite set holds |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2
proof
let s be non empty finite set ; ::_thesis: |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2
set n = card s;
consider c being real number  such that
A1: c in ].(- 1),0.[ and
A2: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by Th8;
 c < 0 by A1, XXREAL_1:4;
hence  |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by A2, Th6; ::_thesis: verum
end;

theorem Th10: :: CARDFIN2:10
for s being non empty finite set holds card (derangements s) = round (((card s) !) / number_e)
proof
let s be non empty finite set ; ::_thesis: card (derangements s) = round (((card s) !) / number_e)
 |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by Th9;
hence  card (derangements s) = round (((card s) !) / number_e) by Th4; ::_thesis: verum
end;

theorem Th11: :: CARDFIN2:11
derangements {} = {{}}
proof
hereby  :: according to XBOOLE_0:def_10,TARSKI:def_3 ::_thesis: {{}} c= derangements {}
let x be set ; ::_thesis: ( x in derangements {} implies x in {{}} )
assume  x in derangements {} ; ::_thesis: x in {{}}
then  ex f being Permutation of {} st
( x = f & f is without_fixpoints ) ;
hence  x in {{}} by ALTCAT_1:2, FUNCT_2:9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in derangements {} )
assume  x in {{}} ; ::_thesis: x in derangements {}
then A1: x = {} by TARSKI:def_1;
 rng (id {}) = {} ;
then  id {} is Permutation of {} by FUNCT_2:57;
hence  x in derangements {} by A1, Th1; ::_thesis: verum
end;

theorem Th12: :: CARDFIN2:12
for x being set holds derangements {x} = {}
proof
let x be set ; ::_thesis: derangements {x} = {}
A1: card {x} = 1 by CARD_1:30;
 1 / number_e < 1 / 2 by TAYLOR_1:11, XREAL_1:76;
then  - (1 / 2) < - (1 / number_e) by XREAL_1:24;
then  |.(0 - (1 / number_e)).| < 1 / 2 by SEQ_2:1;
then  round (1 / number_e) = 0 by Th4;
then  card (derangements {x}) = 0 by Th10, A1, NEWTON:13;
hence  derangements {x} = {} ; ::_thesis: verum
end;

reconsider j = 1, z = 0 as Element of INT by INT_1:def_2;

deffunc H1( Element of NAT , Integer, Integer) ->  Element of INT = ($1 + 1) * ($2 + $3);

definition
func der_seq  ->  sequence of INT means :Def3: :: CARDFIN2:def 3
( it . 0 = 1 & it . 1 = 0 & ( for n being Nat holds it . (n + 2) = (n + 1) * ((it . n) + (it . (n + 1))) ) );
existence
 ex b1 being sequence of INT st
( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) )
proof
consider f being Function of NAT,INT such that
A1: ( f . 0 = j & f . 1 = z & ( for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) ) ) from RECDEF_2:sch_5();
take  f ; ::_thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) )
thus  ( f . 0 = 1 & f . 1 = 0 ) by A1; ::_thesis: for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
let n be Nat; ::_thesis: f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1)))
 n is Element of NAT by ORDINAL1:def_12;
hence  f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being sequence of INT st b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) & b2 . 0 = 1 & b2 . 1 = 0 & ( for n being Nat holds b2 . (n + 2) = (n + 1) * ((b2 . n) + (b2 . (n + 1))) ) holds
b1 = b2
proof
let f, g be sequence of INT; ::_thesis: ( f . 0 = 1 & f . 1 = 0 & ( for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ) & g . 0 = 1 & g . 1 = 0 & ( for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ) implies f = g )
assume  ( f . 0 = 1 & f . 1 = 0 ) ; ::_thesis: ( ex n being Nat st not f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) or not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A2: ( f . 0 = j & f . 1 = z ) ;
assume  for n being Nat holds f . (n + 2) = (n + 1) * ((f . n) + (f . (n + 1))) ; ::_thesis: ( not g . 0 = 1 or not g . 1 = 0 or ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A3: for n being Element of NAT holds f . (n + 2) = H1(n,f . n,f . (n + 1)) ;
assume  ( g . 0 = 1 & g . 1 = 0 ) ; ::_thesis: ( ex n being Nat st not g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) or f = g )
then A4: ( g . 0 = j & g . 1 = z ) ;
assume  for n being Nat holds g . (n + 2) = (n + 1) * ((g . n) + (g . (n + 1))) ; ::_thesis: f = g
then A5: for n being Element of NAT holds g . (n + 2) = H1(n,g . n,g . (n + 1)) ;
thus  f = g from RECDEF_2:sch_7(A2, A3, A4, A5); ::_thesis: verum
end;
end;

:: deftheorem Def3 defines der_seq CARDFIN2:def_3_:_
 for b1 being sequence of INT holds
( b1 = der_seq iff ( b1 . 0 = 1 & b1 . 1 = 0 & ( for n being Nat holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) ) );

registration
let c be Integer;
let F be XFinSequence of ;
clusterc (#) F ->  T-Sequence-like INT -valued finite ;
coherence
 ( c (#) F is finite & c (#) F is INT -valued & c (#) F is T-Sequence-like ) ;
end;

registration
let c be complex number ;
let F be empty Function;
clusterc (#) F ->  empty ;
coherence
 c (#) F is empty ;
end;

theorem :: CARDFIN2:13
for F being XFinSequence of
for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
proof
let F be XFinSequence of ; ::_thesis: for c being Integer holds c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
let c be Integer; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
percases ( len F = 0 or len F > 0 ) ;
suppose len F = 0 ; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
then A1: ( F is empty & F . ((len F) -' 1) = 0 ) by FUNCT_1:def_2;
then  Sum F = 0 ;
hence  c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A1; ::_thesis: verum
end;
suppose len F > 0 ; ::_thesis: c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1)))
then A2: ((len F) -' 1) + 1 = len F by NAT_1:14, XREAL_1:235;
A3: dom F = dom (c (#) F) by VALUED_1:def_5;
A4: c * (Sum F) = Sum (c (#) F) by AFINSQ_2:64;
A5: Sum (c (#) F) = Sum ((c (#) F) | (len F)) by A3, RELAT_1:69;
 Sum ((c (#) F) | (((len F) -' 1) + 1)) = (Sum ((c (#) F) | ((len F) -' 1))) + ((c (#) F) . ((len F) -' 1)) by A3, A2, AFINSQ_2:65, NAT_1:45;
hence  c * (Sum F) = (Sum ((c (#) F) | ((len F) -' 1))) + (c * (F . ((len F) -' 1))) by A4, A5, A2, VALUED_1:6; ::_thesis: verum
end;
end;
end;

theorem Th14: :: CARDFIN2:14
for X, N being XFinSequence of st len N = (len X) + 1 holds
for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))
proof
let X, N be XFinSequence of ; ::_thesis: ( len N = (len X) + 1 implies for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X)) )
assume A1: len N = (len X) + 1 ; ::_thesis: for c being Integer st N | (len X) = c (#) X holds
Sum N = (c * (Sum X)) + (N . (len X))
let c be Integer; ::_thesis: ( N | (len X) = c (#) X implies Sum N = (c * (Sum X)) + (N . (len X)) )
assume A2: N | (len X) = c (#) X ; ::_thesis: Sum N = (c * (Sum X)) + (N . (len X))
thus  Sum N = Sum (N | (len N)) by RELAT_1:69
.= (Sum (N | (len X))) + (N . (len X)) by A1, AFINSQ_2:65, NAT_1:45
.= (c * (Sum X)) + (N . (len X)) by A2, AFINSQ_2:64 ; ::_thesis: verum
end;

theorem :: CARDFIN2:15
for s being finite set holds der_seq . (card s) = card (derangements s)
proof
let s be finite set ; ::_thesis: der_seq . (card s) = card (derangements s)
defpred S1[ finite set ] means  for s being finite set st card s = $1 holds
der_seq . $1 = card (derangements s);
A1: S1[ 0 ]
proof
let s be finite set ; ::_thesis: ( card s = 0 implies der_seq . 0 = card (derangements s) )
assume  card s = 0 ; ::_thesis: der_seq . 0 = card (derangements s)
then A2: s = {} ;
thus der_seq . 0 = 1 by Def3
.= card (derangements s) by Th11, A2, CARD_1:30 ; ::_thesis: verum
end;
A3: S1[1]
proof
let s be finite set ; ::_thesis: ( card s = 1 implies der_seq . 1 = card (derangements s) )
assume  card s = 1 ; ::_thesis: der_seq . 1 = card (derangements s)
then consider x being set  such that
A4: s = {x} by CARD_2:42;
thus der_seq . 1 = card {} by Def3
.= card (derangements s) by Th12, A4 ; ::_thesis: verum
end;
A5: for n being Nat st S1[n] & S1[n + 1] holds
S1[n + 2]
proof
let n be Nat; ::_thesis: ( S1[n] & S1[n + 1] implies S1[n + 2] )
assume A6: S1[n] ; ::_thesis: ( not S1[n + 1] or S1[n + 2] )
assume A7: S1[n + 1] ; ::_thesis: S1[n + 2]
set n1 = n + 1;
A8: ( card n = n & card (n + 1) = n + 1 ) by CARD_1:def_2;
then consider XFn being XFinSequence of  such that
A9: Sum XFn = card  {  h where h is Function of n,n : ( h is one-to-one & ( for x being set st x in n holds
h . x <> x ) )  }  and
A10: dom XFn = n + 1 and
A11: for m being Nat st m in dom XFn holds
XFn . m = (((- 1) |^ m) * (n !)) / (m !) by CARD_FIN:63;
consider XFn1 being XFinSequence of  such that
A12: Sum XFn1 = card  {  h where h is Function of (n + 1),(n + 1) : ( h is one-to-one & ( for x being set st x in n + 1 holds
h . x <> x ) )  }  and
A13: dom XFn1 = (n + 1) + 1 and
A14: for m being Nat st m in dom XFn1 holds
XFn1 . m = (((- 1) |^ m) * ((n + 1) !)) / (m !) by A8, CARD_FIN:63;
 Sum XFn = card (derangements n) by A9, Th7;
then A15: der_seq . n = Sum XFn by A6, A8;
 Sum XFn1 = card (derangements (n + 1)) by A12, Th7;
then A16: der_seq . (n + 1) = Sum XFn1 by A7, A8;
let sn2 be finite set ; ::_thesis: ( card sn2 = n + 2 implies der_seq . (n + 2) = card (derangements sn2) )
assume  card sn2 = n + 2 ; ::_thesis: der_seq . (n + 2) = card (derangements sn2)
then consider XFn2 being XFinSequence of  such that
A17: Sum XFn2 = card  {  h where h is Function of sn2,sn2 : ( h is one-to-one & ( for x being set st x in sn2 holds
h . x <> x ) )  }  and
A18: dom XFn2 = (n + 2) + 1 and
A19: for m being Nat st m in dom XFn2 holds
XFn2 . m = (((- 1) |^ m) * ((n + 2) !)) / (m !) by CARD_FIN:63;
A20: Sum XFn2 = card (derangements sn2) by A17, Th7;
A21: len XFn1 = (len XFn) + 1 by A10, A13;
A22: len XFn2 = (len XFn1) + 1 by A13, A18;
 n + 1 < n + 2 by XREAL_1:8;
then A23: len XFn c= dom XFn1 by A10, A13, NAT_1:39;
A24: dom ((n + 1) (#) XFn) = len XFn by VALUED_1:def_5;
A25: now__::_thesis:_for_x_being_set_st_x_in_dom_(XFn1_|_(len_XFn))_holds_
(XFn1_|_(len_XFn))_._x_=_((n_+_1)_(#)_XFn)_._x
let x be set ; ::_thesis: ( x in dom (XFn1 | (len XFn)) implies (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x )
assume A26: x in dom (XFn1 | (len XFn)) ; ::_thesis: (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x
then A27: x in dom XFn1 by RELAT_1:57;
reconsider m = x as Element of NAT by A26;
A28: m in dom XFn by A26, RELAT_1:57;
thus (XFn1 | (len XFn)) . x = XFn1 . x by A26, FUNCT_1:47
.= (((- 1) |^ m) * ((n + 1) !)) / (m !) by A27, A14
.= (((- 1) |^ m) * ((n !) * (n + 1))) / (m !) by NEWTON:15
.= (n + 1) * ((((- 1) |^ m) * (n !)) / (m !))
.= (n + 1) * (XFn . m) by A11, A28
.= ((n + 1) (#) XFn) . x by VALUED_1:6 ; ::_thesis: verum
end;
set a = (- 1) |^ (n + 1);
A29: (- 1) * ((- 1) |^ (n + 1)) = (- 1) |^ ((n + 1) + 1) by NEWTON:6;
 (n + 1) + 0 < (n + 1) + 1 by XREAL_1:8;
then A30: n + 1 in dom XFn1 by A13, NAT_1:44;
 (n + 2) + 0 < (n + 2) + 1 by XREAL_1:8;
then A31: n + 2 in dom XFn2 by A18, NAT_1:44;
 XFn1 | (len XFn) = (n + 1) (#) XFn by A23, A24, A25, FUNCT_1:2, RELAT_1:62;
then A32: Sum XFn1 = ((n + 1) * (Sum XFn)) + (XFn1 . (len XFn)) by Th14, A21
.= ((n + 1) * (Sum XFn)) + ((((- 1) |^ (n + 1)) * ((n + 1) !)) / ((n + 1) !)) by A10, A14, A30
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * (((n + 1) !) / ((n + 1) !)))
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * 1) by XCMPLX_1:60 ;
A33: now__::_thesis:_for_x_being_set_st_x_in_dom_(XFn2_|_(len_XFn1))_holds_
(XFn2_|_(len_XFn1))_._x_=_((n_+_2)_(#)_XFn1)_._x
let x be set ; ::_thesis: ( x in dom (XFn2 | (len XFn1)) implies (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x )
assume A34: x in dom (XFn2 | (len XFn1)) ; ::_thesis: (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x
then A35: x in dom XFn2 by RELAT_1:57;
reconsider m = x as Element of NAT by A34;
A36: m in dom XFn1 by A34, RELAT_1:57;
thus (XFn2 | (len XFn1)) . x = XFn2 . x by A34, FUNCT_1:47
.= (((- 1) |^ m) * (((n + 1) + 1) !)) / (m !) by A35, A19
.= (((- 1) |^ m) * (((n + 1) !) * ((n + 1) + 1))) / (m !) by NEWTON:15
.= ((n + 1) + 1) * ((((- 1) |^ m) * ((n + 1) !)) / (m !))
.= (n + 2) * (XFn1 . m) by A14, A36
.= ((n + 2) (#) XFn1) . x by VALUED_1:6 ; ::_thesis: verum
end;
 n + 2 < n + 3 by XREAL_1:8;
then  len XFn1 c= dom XFn2 by A13, A18, NAT_1:39;
then A37: dom (XFn2 | (len XFn1)) = len XFn1 by RELAT_1:62;
 dom ((n + 2) (#) XFn1) = len XFn1 by VALUED_1:def_5;
then  Sum XFn2 = ((n + 2) * (Sum XFn1)) + (XFn2 . (len XFn1)) by Th14, A22, A37, A33, FUNCT_1:2
.= ((n + 2) * (Sum XFn1)) + ((((- 1) |^ (n + 2)) * ((n + 2) !)) / ((n + 2) !)) by A19, A31, A13
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * (((n + 2) !) / ((n + 2) !))) by A29
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * 1) by XCMPLX_1:60
.= (n + 1) * ((Sum XFn) + (Sum XFn1)) by A32 ;
hence  der_seq . (n + 2) = card (derangements sn2) by A20, Def3, A15, A16; ::_thesis: verum
end;
 for n being Nat holds S1[n] from FIB_NUM:sch_1(A1, A3, A5);
hence  der_seq . (card s) = card (derangements s) ; ::_thesis: verum
end;

begin

definition
let s, t be set ;
func not-one-to-one (s,t) ->  Subset of (Funcs (s,t)) equals :: CARDFIN2:def 4
 {  f where f is Function of s,t : not f is one-to-one  }  ;
coherence
  {  f where f is Function of s,t : not f is one-to-one  }  is Subset of (Funcs (s,t))
proof
percases ( not t is empty or t is empty ) ;
supposeA1: not t is empty ; ::_thesis:  {  f where f is Function of s,t : not f is one-to-one  }  is Subset of (Funcs (s,t))
  {  f where f is Function of s,t : not f is one-to-one  }  c= Funcs (s,t)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is Function of s,t : not f is one-to-one  }  or x in Funcs (s,t) )
assume  x in  {  f where f is Function of s,t : not f is one-to-one  }  ; ::_thesis: x in Funcs (s,t)
then  ex f being Function of s,t st
( x = f & not f is one-to-one ) ;
hence  x in Funcs (s,t) by A1, FUNCT_2:8; ::_thesis: verum
end;
hence   {  f where f is Function of s,t : not f is one-to-one  }  is Subset of (Funcs (s,t)) ; ::_thesis: verum
end;
supposeA2: t is empty ; ::_thesis:  {  f where f is Function of s,t : not f is one-to-one  }  is Subset of (Funcs (s,t))
  {  f where f is Function of s,t : not f is one-to-one  }  = {}
proof
assume   {  f where f is Function of s,t : not f is one-to-one  }  <> {} ; ::_thesis: contradiction
then consider x being set  such that
A3: x in  {  f where f is Function of s,t : not f is one-to-one  }  by XBOOLE_0:def_1;
 ex f being Function of s,t st
( x = f & not f is one-to-one ) by A3;
hence  contradiction by A2; ::_thesis: verum
end;
hence   {  f where f is Function of s,t : not f is one-to-one  }  is Subset of (Funcs (s,t)) by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem  defines not-one-to-one CARDFIN2:def_4_:_
 for s, t being set holds not-one-to-one (s,t) =  {  f where f is Function of s,t : not f is one-to-one  }  ;

registration
let s, t be finite set ;
cluster not-one-to-one (s,t) ->  finite ;
coherence
 not-one-to-one (s,t) is finite ;
end;

scheme :: CARDFIN2:sch 1
FraenkelDiff{ F1() ->  set , F2() ->  set , P1[ set ] } :
  {  f where f is Function of F1(),F2() : P1[f]  }  = (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }
provided
A1: ( F2() = {} implies F1() = {} )
proof
set z1 =  {  f where f is Function of F1(),F2() : P1[f]  }  ;
set z2 =  {  f where f is Function of F1(),F2() : P1[f]  }  ;
set zc = Funcs (F1(),F2());
thus   {  f where f is Function of F1(),F2() : P1[f]  }  c= (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  :: according to XBOOLE_0:def_10 ::_thesis: (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  c=  {  f where f is Function of F1(),F2() : P1[f]  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is Function of F1(),F2() : P1[f]  }  or x in (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  )
assume  x in  {  f where f is Function of F1(),F2() : P1[f]  }  ; ::_thesis: x in (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }
then consider f being Function of F1(),F2() such that
A2: ( x = f & P1[f] ) ;
A3: f in Funcs (F1(),F2()) by A1, FUNCT_2:8;
 not f in  {  f where f is Function of F1(),F2() : P1[f]  }
proof
assume  f in  {  f where f is Function of F1(),F2() : P1[f]  }  ; ::_thesis: contradiction
then  ex g being Function of F1(),F2() st
( f = g & P1[g] ) ;
hence  contradiction by A2; ::_thesis: verum
end;
hence  x in (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  by A3, A2, XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  or x in  {  f where f is Function of F1(),F2() : P1[f]  }  )
assume A4: x in (Funcs (F1(),F2())) \  {  f where f is Function of F1(),F2() : P1[f]  }  ; ::_thesis: x in  {  f where f is Function of F1(),F2() : P1[f]  }
then A5: x is Function of F1(),F2() by FUNCT_2:66;
 not x in  {  f where f is Function of F1(),F2() : P1[f]  }  by A4, XBOOLE_0:def_5;
then  P1[x] by A5;
hence  x in  {  f where f is Function of F1(),F2() : P1[f]  }  by A5; ::_thesis: verum
end;

theorem Th16: :: CARDFIN2:16
for s, t being finite set st card s <= card t holds
card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))
proof
let s, t be finite set ; ::_thesis: ( card s <= card t implies card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) )
assume A1: card s <= card t ; ::_thesis: card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !))
defpred S1[ Function] means $1 is one-to-one ;
set onetoone =  {  f where f is Function of s,t : f is one-to-one  }  ;
A2: ( t = {} implies s = {} )
proof
assume  t = {} ; ::_thesis: s = {}
then  card t = 0 ;
hence  s = {} by A1; ::_thesis: verum
end;
  {  f where f is Function of s,t : f is one-to-one  }  c= Funcs (s,t)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  f where f is Function of s,t : f is one-to-one  }  or x in Funcs (s,t) )
assume  x in  {  f where f is Function of s,t : f is one-to-one  }  ; ::_thesis: x in Funcs (s,t)
then  ex f being Function of s,t st
( x = f & f is one-to-one ) ;
hence  x in Funcs (s,t) by A2, FUNCT_2:8; ::_thesis: verum
end;
then reconsider onetoone =  {  f where f is Function of s,t : f is one-to-one  }  as Subset of (Funcs (s,t)) ;
  {  f where f is Function of s,t : not S1[f]  }  = (Funcs (s,t)) \  {  f where f is Function of s,t : S1[f]  }  from CARDFIN2:sch_1(A2);
then  card (not-one-to-one (s,t)) = (card (Funcs (s,t))) - (card onetoone) by CARD_2:44
.= (card (Funcs (s,t))) - (((card t) !) / (((card t) -' (card s)) !)) by A1, CARD_FIN:7
.= ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) by A2, CARD_FIN:4 ;
hence  card (not-one-to-one (s,t)) = ((card t) |^ (card s)) - (((card t) !) / (((card t) -' (card s)) !)) ; ::_thesis: verum
end;

Lm1:  2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
proof
A1: (364 + 1) ! = (364 !) * (364 + 1) by NEWTON:15;
A2: (363 + 1) ! = (363 !) * (363 + 1) by NEWTON:15;
A3: (362 + 1) ! = (362 !) * (362 + 1) by NEWTON:15;
A4: (361 + 1) ! = (361 !) * (361 + 1) by NEWTON:15;
A5: (360 + 1) ! = (360 !) * (360 + 1) by NEWTON:15;
A6: (359 + 1) ! = (359 !) * (359 + 1) by NEWTON:15;
A7: (358 + 1) ! = (358 !) * (358 + 1) by NEWTON:15;
A8: (357 + 1) ! = (357 !) * (357 + 1) by NEWTON:15;
A9: (356 + 1) ! = (356 !) * (356 + 1) by NEWTON:15;
A10: (355 + 1) ! = (355 !) * (355 + 1) by NEWTON:15;
A11: (354 + 1) ! = (354 !) * (354 + 1) by NEWTON:15;
A12: (353 + 1) ! = (353 !) * (353 + 1) by NEWTON:15;
A13: (352 + 1) ! = (352 !) * (352 + 1) by NEWTON:15;
A14: (351 + 1) ! = (351 !) * (351 + 1) by NEWTON:15;
A15: (350 + 1) ! = (350 !) * (350 + 1) by NEWTON:15;
A16: (349 + 1) ! = (349 !) * (349 + 1) by NEWTON:15;
A17: (348 + 1) ! = (348 !) * (348 + 1) by NEWTON:15;
A18: (347 + 1) ! = (347 !) * (347 + 1) by NEWTON:15;
A19: (346 + 1) ! = (346 !) * (346 + 1) by NEWTON:15;
A20: (345 + 1) ! = (345 !) * (345 + 1) by NEWTON:15;
A21: (344 + 1) ! = (344 !) * (344 + 1) by NEWTON:15;
A22: (343 + 1) ! = (343 !) * (343 + 1) by NEWTON:15;
 (342 + 1) ! = (342 !) * (342 + 1) by NEWTON:15;
then  365 ! = (((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343)) * (342 !) by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22;
then A23: (365 !) / (342 !) = ((((((365 * 364) * 363) * 362) * 361) * 360) * ((((((359 * 358) * 357) * 356) * 355) * 354) * 353)) * (((((((((352 * 351) * 350) * 349) * 348) * 347) * 346) * 345) * 344) * 343) by XCMPLX_1:89;
 365 |^ 1 = 365 by NEWTON:5;
then A24: 365 |^ (1 + 1) = 365 * 365 by NEWTON:6;
then A25: 365 |^ (2 + 1) = (365 * 365) * 365 by NEWTON:6;
A26: 365 |^ (3 + 2) = (365 |^ 3) * (365 |^ 2) by NEWTON:8;
A27: 365 |^ (3 + 3) = (365 |^ 3) * (365 |^ 3) by NEWTON:8;
A28: 365 |^ (6 + 5) = (365 |^ 6) * (365 |^ 5) by NEWTON:8;
A29: 365 |^ (6 + 6) = (365 |^ 6) * (365 |^ 6) by NEWTON:8;
 365 |^ (12 + 11) = (365 |^ 12) * (365 |^ 11) by NEWTON:8;
then A30: 2 * ((365 |^ 23) - ((365 !) / (342 !))) > 365 |^ 23 by A28, A23, A29, A26, A24, A25, A27;
 365 - 23 >= 0 ;
hence  2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23 by A30, XREAL_0:def_2; ::_thesis: verum
end;

theorem Th17: :: CARDFIN2:17
for s being finite set
for t being non empty finite set st card s = 23 & card t = 365 holds
2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
proof
let s be finite set ; ::_thesis: for t being non empty finite set st card s = 23 & card t = 365 holds
2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
let t be non empty finite set ; ::_thesis: ( card s = 23 & card t = 365 implies 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume A1: card s = 23 ; ::_thesis: ( not card t = 365 or 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) )
assume A2: card t = 365 ; ::_thesis: 2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t))
then  card (not-one-to-one (s,t)) = (365 |^ 23) - ((365 !) / ((365 -' 23) !)) by Th16, A1;
hence  2 * (card (not-one-to-one (s,t))) > card (Funcs (s,t)) by Lm1, A1, A2, CARD_FIN:4; ::_thesis: verum
end;

theorem :: CARDFIN2:18
for s, t being non empty finite set st card s = 23 & card t = 365 holds
prob (not-one-to-one (s,t)) > 1 / 2
proof
let s, t be non empty finite set ; ::_thesis: ( card s = 23 & card t = 365 implies prob (not-one-to-one (s,t)) > 1 / 2 )
assume A1: card s = 23 ; ::_thesis: ( not card t = 365 or prob (not-one-to-one (s,t)) > 1 / 2 )
assume A2: card t = 365 ; ::_thesis: prob (not-one-to-one (s,t)) > 1 / 2
set E = not-one-to-one (s,t);
set comega = card (Funcs (s,t));
 (2 * (card (not-one-to-one (s,t)))) / 2 > (card (Funcs (s,t))) / 2 by Th17, A1, A2, XREAL_1:74;
then  (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / 2) / (card (Funcs (s,t))) by XREAL_1:74;
then  (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > ((card (Funcs (s,t))) / (card (Funcs (s,t)))) / 2 ;
then  (card (not-one-to-one (s,t))) / (card (Funcs (s,t))) > 1 / 2 by XCMPLX_0:def_7;
hence  prob (not-one-to-one (s,t)) > 1 / 2 by RPR_1:def_1; ::_thesis: verum
end;