set g = seq_logn ;
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds f . n = log 2,(n ! ) ) implies for n being Element of NAT holds f . n = Sum seq_logn ,n )
assume A1: for n being Element of NAT holds f . n = log 2,(n ! ) ; :: thesis: for n being Element of NAT holds f . n = Sum seq_logn ,n
defpred S₁[ Element of NAT ] means f . $1 = Sum seq_logn ,$1;
A2: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: f . k = Sum seq_logn ,k ; :: thesis: S₁[k + 1]
A4: k ! > 0 by NEWTON:23;
f . (k + 1) = log 2,((k + 1) ! ) by A1
.= log 2,((k + 1) * (k ! )) by NEWTON:21
.= (log 2,(k + 1)) + (log 2,(k ! )) by A4, POWER:61
.= (log 2,(k + 1)) + (Sum seq_logn ,k) by A1, A3
.= (seq_logn . (k + 1)) + (Sum seq_logn ,k) by Def2
.= (seq_logn . (k + 1)) + ((Partial_Sums seq_logn ) . k) by SERIES_1:def 6
.= (Partial_Sums seq_logn ) . (k + 1) by SERIES_1:def 1
.= Sum seq_logn ,(k + 1) by SERIES_1:def 6 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A5: Sum seq_logn ,0 = (Partial_Sums seq_logn ) . 0 by SERIES_1:def 6
.= seq_logn . 0 by SERIES_1:def 1
.= 0 by Def2 ;
f . 0 = log 2,1 by A1, NEWTON:18
.= 0 by POWER:59 ;
then A6: S₁[ 0 ] by A5;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A6, A2);
hence for n being Element of NAT holds f . n = Sum seq_logn ,n ; :: thesis: verum