set g = seq_logn ;
let f be Real_Sequence; :: thesis: ( ( for n being 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 Nat holds f . n = log (2,(n !)) ; :: thesis: for n being Element of NAT holds f . n = Sum (seq_logn,n)
defpred S₁[ Nat] means f . $1 = Sum (seq_logn,$1);
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be 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:17;
f . (k + 1) = log (2,((k + 1) !)) by A1
.= log (2,((k + 1) * (k !))) by NEWTON:15
.= (log (2,(k + 1))) + (log (2,(k !))) by A4, POWER:53
.= (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 5
.= (Partial_Sums seq_logn) . (k + 1) by SERIES_1:def 1
.= Sum (seq_logn,(k + 1)) by SERIES_1:def 5 ;
hence S₁[k + 1] ; :: thesis: verum

end;

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