let f be Function of NAT,REAL; :: thesis: ex h being Function of NAT,REAL st
( h is negligible & ( for x being Nat holds |.((f . x) - (f . x)).| <= |.(h . x).| ) )
deffunc H₁( Nat) -> set = 1 / (2 to_power $1);
consider h being Real_Sequence such that
P1: for x being Nat holds h . x = H₁(x) from SEQ_1:sch 1();
take h ; :: thesis: ( h is negligible & ( for x being Nat holds |.((f . x) - (f . x)).| <= |.(h . x).| ) )
thus h is negligible by TH3, P1; :: thesis: for x being Nat holds |.((f . x) - (f . x)).| <= |.(h . x).|
let x be Nat; :: thesis: |.((f . x) - (f . x)).| <= |.(h . x).|
|.((f . x) - (f . x)).| = 0 ;
hence |.((f . x) - (f . x)).| <= |.(h . x).| ; :: thesis: verum