begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem
Lm1:
for n, m being Element of NAT st n > 1 holds
((m ! ) / (n ! )) * n = (m ! ) / ((n -' 1) ! )
theorem Th32:
theorem
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem Th41:
theorem
theorem Th43:
theorem
Lm2:
#Z 1 = id REAL
theorem Th45:
theorem
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem
theorem
theorem
theorem
theorem
theorem Th56:
theorem Th57:
theorem
theorem Th59:
theorem Th60:
theorem
theorem
theorem
Lm3:
for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st f is_differentiable_on Z holds
(f `| Z) `| Z = (diff f,Z) . 2
theorem Th64:
theorem
theorem
Lm4:
for f being PartFunc of REAL ,REAL holds f / f = ((dom f) \ (f " {0 })) --> 1
Lm5:
for f being PartFunc of REAL ,REAL holds (f (#) (f (#) f)) " {0 } = f " {0 }
theorem
theorem