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
set g = seq_logn ;
defpred S₁[ Element of NAT ] means f . $1 = Sum seq_logn ,$1;
A2: S₁[ 0 ]

proof

A3: f . 0 = log 2,1 by A1, NEWTON:18
.= 0 by POWER:59 ;
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 ;
hence S₁[ 0 ] by A3; :: thesis: verum

end;

A4: 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 A5: f . k = Sum seq_logn ,k ; :: thesis: S₁[k + 1]
A6: 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 A6, POWER:61
.= (log 2,(k + 1)) + (Sum seq_logn ,k) by A1, A5
.= (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;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A4);
hence for n being Element of NAT holds f . n = Sum seq_logn ,n ; :: thesis: verum