begin
theorem Th1:
theorem Th2:
begin
:: deftheorem defines round CARDFIN2:def 1 :
for n being real number holds round n = [\(n + (1 / 2))/];
theorem
theorem Th4:
begin
theorem Th5:
theorem Th6:
:: deftheorem defines derangements CARDFIN2:def 2 :
for s being set holds derangements s = { f where f is Permutation of s : f has_no_fixpoint } ;
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
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);
:: 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 natural number holds b1 . (n + 2) = (n + 1) * ((b1 . n) + (b1 . (n + 1))) ) ) );
theorem
theorem Th14:
theorem
begin
:: 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 } ;
scheme
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()
= {} )
theorem Th16:
Lm1:
2 * ((365 |^ 23) - ((365 !) / ((365 -' 23) !))) > 365 |^ 23
theorem Th17:
theorem