theorem :: ASYMPT_1:88

for f being Real_Sequence st ( for n being Nat holds f . n = log (2,(n !)) ) holds
for n being Element of NAT holds f . n = Sum (seq_logn,n) by Lm44;