let f, g be Function of NAT,REAL; :: thesis: ( ex h being Function of NAT,REAL st
( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) implies ex h being Function of NAT,REAL st
( h is negligible & ( for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).| ) ) )
given h being Function of NAT,REAL such that P1: ( h is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(h . x).| ) ) ; :: thesis: ex h being Function of NAT,REAL st
( h is negligible & ( for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).| ) )
take h ; :: thesis: ( h is negligible & ( for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).| ) )
thus h is negligible by P1; :: thesis: for x being Nat holds |.((g . x) - (f . x)).| <= |.(h . x).|
let x be Nat; :: thesis: |.((g . x) - (f . x)).| <= |.(h . x).|
|.((f . x) - (g . x)).| <= |.(h . x).| by P1;
hence |.((g . x) - (f . x)).| <= |.(h . x).| by COMPLEX1:60; :: thesis: verum