let e be positive Real; :: thesis: for f being Real_Sequence st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log 2,(n to_power e) ) holds
( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
let f be Real_Sequence; :: thesis: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log 2,(n to_power e) ) implies ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 ) )
assume A1: ( f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log 2,(n to_power e) ) ) ; :: thesis: ( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 )
set g = seq_n^ e;
set h = f /" (seq_n^ e);

A2: now

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p )
assume A3: p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p
reconsider p1 = p as Real by XREAL_0:def 1;
set i0 = [/((7 / p1) to_power (1 / e))\];
set i1 = [/((p1 to_power (- (2 / e))) + 1)\];
set N = max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2;
A4: ( max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 >= max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\] & max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 >= 2 ) by XXREAL_0:25;
( max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\] >= [/((7 / p1) to_power (1 / e))\] & max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\] >= [/((p1 to_power (- (2 / e))) + 1)\] ) by XXREAL_0:25;
then A5: ( max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 >= [/((7 / p1) to_power (1 / e))\] & max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 >= [/((p1 to_power (- (2 / e))) + 1)\] ) by A4, XXREAL_0:2;
max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 is Integer

proof

per cases ( max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 = max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\] or max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 = 2 ) by XXREAL_0:16;

suppose max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 = max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\] ; :: thesis: max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 is Integer

hence max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 is Integer by XXREAL_0:16; :: thesis: verum

end;

suppose max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 = 2 ; :: thesis: max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 is Integer

hence max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 is Integer ; :: thesis: verum

end;

end;

end;

then reconsider N = max (max [/((7 / p1) to_power (1 / e))\],[/((p1 to_power (- (2 / e))) + 1)\]),2 as Element of NAT by A4, INT_1:16;
p " > 0 by A3;
then 7 * (p " ) > 7 * 0 by XREAL_1:70;
then A6: 7 / p > 0 ;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs (((f /" (seq_n^ e)) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs (((f /" (seq_n^ e)) . n) - 0 ) < p )
assume A7: n >= N ; :: thesis: abs (((f /" (seq_n^ e)) . n) - 0 ) < p
then A8: ( n >= 2 & n >= [/((7 / p1) to_power (1 / e))\] & n >= [/((p1 to_power (- (2 / e))) + 1)\] ) by A4, A5, XXREAL_0:2;
[/((7 / p1) to_power (1 / e))\] >= (7 / p) to_power (1 / e) by INT_1:def 5;
then A9: n >= (7 / p) to_power (1 / e) by A8, XXREAL_0:2;
(7 / p1) to_power (1 / e) > 0 by A6, POWER:39;
then n to_power e >= ((7 / p) to_power (1 / e)) to_power e by A9, Lm6;
then n to_power e >= (7 / p1) to_power (e * (1 / e)) by A6, POWER:38;
then n to_power e >= (7 / p) to_power 1 by XCMPLX_1:107;
then n to_power e >= 7 / p1 by POWER:30;
then p * (n to_power e) >= (7 / p) * p by A3, XREAL_1:66;
then p * (n to_power e) >= 7 by A3, XCMPLX_1:88;
then p * (n to_power e) > 6 by XXREAL_0:2;
then A10: (p1 * (n to_power e)) ^2 < 2 to_power (p1 * (n to_power e)) by Lm14;
set c = p1 * (n to_power e);
A11: n to_power e > 0 by A4, A7, POWER:39;
then A12: (n to_power e) " > 0 ;
p * (n to_power e) > p * 0 by A3, A11, XREAL_1:70;
then p1 * (n to_power e) < (2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e)) by A10, XREAL_1:83;
then n to_power e < ((2 to_power (p1 * (n to_power e))) / (p1 * (n to_power e))) / p by A3, XREAL_1:83;
then A13: n to_power e < (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) by XCMPLX_1:79;
A14: p1 to_power 2 > 0 by A3, POWER:39;
A15: [/((p1 to_power (- (2 / e))) + 1)\] >= (p to_power (- (2 / e))) + 1 by INT_1:def 5;
(p to_power (- (2 / e))) + 1 > (p to_power (- (2 / e))) + 0 by XREAL_1:10;
then [/((p1 to_power (- (2 / e))) + 1)\] > p to_power (- (2 / e)) by A15, XXREAL_0:2;
then A16: n > p to_power (- (2 / e)) by A8, XXREAL_0:2;
p1 to_power (- (2 / e)) > 0 by A3, POWER:39;
then n to_power e > (p to_power (- (2 / e))) to_power e by A16, POWER:42;
then n to_power e > p1 to_power ((- (2 / e)) * e) by A3, POWER:38;
then n to_power e > p to_power (- ((2 / e) * e)) ;
then n to_power e > p to_power (- 2) by XCMPLX_1:88;
then (p to_power 2) * (n to_power e) > (p to_power 2) * (p to_power (- 2)) by A14, XREAL_1:70;
then (p1 to_power 2) * (n to_power e) > p1 to_power (2 + (- 2)) by A3, POWER:32;
then (p1 to_power 2) * (n to_power e) > 1 by POWER:29;
then (p1 ^2 ) * (n to_power e) > 1 by POWER:53;
then A17: 1 / (p * (p1 * (n to_power e))) < 1 / 1 by XREAL_1:90;
2 to_power (p1 * (n to_power e)) > 0 by POWER:39;
then (2 to_power (p1 * (n to_power e))) * (1 / ((p1 * (n to_power e)) * p)) < (2 to_power (p1 * (n to_power e))) * (1 / 1) by A17, XREAL_1:70;
then (2 to_power (p1 * (n to_power e))) / ((p1 * (n to_power e)) * p) < (2 to_power (p1 * (n to_power e))) * 1 ;
then n to_power e < 2 to_power (p1 * (n to_power e)) by A13, XXREAL_0:2;
then log 2,(n to_power e) < log 2,(2 to_power (p1 * (n to_power e))) by A11, POWER:65;
then log 2,(n to_power e) < (p1 * (n to_power e)) * (log 2,2) by POWER:63;
then log 2,(n to_power e) < (p1 * (n to_power e)) * 1 by POWER:60;
then A18: (log 2,(n to_power e)) / (n to_power e) < p by A11, XREAL_1:85;
n > 1 by A8, XXREAL_0:2;
then n to_power e > n to_power 0 by POWER:44;
then n to_power e > 1 by POWER:29;
then log 2,(n to_power e) > log 2,1 by POWER:65;
then log 2,(n to_power e) > 0 by POWER:59;
then (log 2,(n to_power e)) * ((n to_power e) " ) > 0 * ((n to_power e) " ) by A12, XREAL_1:70;
then A19: (log 2,(n to_power e)) / (n to_power e) > 0 ;
(f /" (seq_n^ e)) . n = (f . n) / ((seq_n^ e) . n) by Lm4
.= (log 2,(n to_power e)) / ((seq_n^ e) . n) by A1, A4, A7
.= (log 2,(n to_power e)) / (n to_power e) by A4, A7, Def3 ;
hence abs (((f /" (seq_n^ e)) . n) - 0 ) < p by A18, A19, ABSVALUE:def 1; :: thesis: verum

end;

hence f /" (seq_n^ e) is convergent by SEQ_2:def 6; :: thesis: lim (f /" (seq_n^ e)) = 0
hence lim (f /" (seq_n^ e)) = 0 by A2, SEQ_2:def 7; :: thesis: verum