let m be Nat; :: thesis: ( 1 < m implies Liouville_seq ((seq_const 1),m) is negligible )
assume AS: 1 < m ; :: thesis: Liouville_seq ((seq_const 1),m) is negligible
ex f being Function of NAT,REAL st
for x being Nat holds f . x = 1 / (2 to_power x)

proof

deffunc H₁( Nat) -> set = 1 / (2 to_power $1);
( ex f being Real_Sequence st
for n being Nat holds f . n = H₁(n) & ( for f1, f2 being Real_Sequence st ( for n being Nat holds f1 . n = H₁(n) ) & ( for n being Nat holds f2 . n = H₁(n) ) holds
f1 = f2 ) ) from IRRAT_1:sch 1();
hence ex f being Function of NAT,REAL st
for x being Nat holds f . x = 1 / (2 to_power x) ; :: thesis: verum

end;

then consider f being Function of NAT,REAL such that
ACF: for x being Nat holds f . x = 1 / (2 to_power x) ;
set g = Liouville_seq ((seq_const 1),m);
for x being Nat holds |.((Liouville_seq ((seq_const 1),m)) . x).| <= |.(f . x).|

proof

let x be Nat; :: thesis: |.((Liouville_seq ((seq_const 1),m)) . x).| <= |.(f . x).|
m1: f . x = 1 / (2 to_power x) by ACF;
then M1: (Liouville_seq ((seq_const 1),m)) . x <= f . x by TLLC, AS;
0 <= (Liouville_seq ((seq_const 1),m)) . x

proof

per cases ( x = 0 or not x is zero ) ;

suppose x = 0 ; :: thesis: 0 <= (Liouville_seq ((seq_const 1),m)) . x

hence 0 <= (Liouville_seq ((seq_const 1),m)) . x by DefLio; :: thesis: verum

end;

suppose not x is zero ; :: thesis: 0 <= (Liouville_seq ((seq_const 1),m)) . x

then (Liouville_seq ((seq_const 1),m)) . x = ((seq_const 1) . x) / (m to_power (x !)) by DefLio;
hence 0 <= (Liouville_seq ((seq_const 1),m)) . x ; :: thesis: verum

end;

end;

end;

then - (f . x) <= (Liouville_seq ((seq_const 1),m)) . x by m1;
then M3: |.((Liouville_seq ((seq_const 1),m)) . x).| <= f . x by M1, ABSVALUE:5;
f . x <= |.(f . x).| by ABSVALUE:4;
hence |.((Liouville_seq ((seq_const 1),m)) . x).| <= |.(f . x).| by XXREAL_0:2, M3; :: thesis: verum

end;

hence Liouville_seq ((seq_const 1),m) is negligible by ACF, ASYMPT_3:25, ASYMPT_3:26; :: thesis: verum