let f, g be Function of NAT,REAL; :: thesis: ( f negligibleEQ g iff f - g is negligible )

hereby :: thesis: ( f - g is negligible implies f negligibleEQ g )

assume A1: f negligibleEQ g ; :: thesis: f - g is negligible
consider v being Function of NAT,REAL such that
B1: ( v is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(v . x).| ) ) by A1;
for x being Nat holds |.((f - g) . x).| <= |.(v . x).|

proof

let x be Nat; :: thesis: |.((f - g) . x).| <= |.(v . x).|
x in NAT by ORDINAL1:def 12;
then consider y being Element of NAT such that
LXY: x = y ;
|.((f - g) . y).| = |.((f . y) - (g . y)).| by VALUED_1:15;
hence |.((f - g) . x).| <= |.(v . x).| by B1, LXY; :: thesis: verum

end;

hence f - g is negligible by B1, TH4; :: thesis: verum

end;

set v = f - g;
for x being Nat holds |.((f . x) - (g . x)).| <= |.((f - g) . x).|

proof

let x be Nat; :: thesis: |.((f . x) - (g . x)).| <= |.((f - g) . x).|
x in NAT by ORDINAL1:def 12;
hence |.((f . x) - (g . x)).| <= |.((f - g) . x).| by VALUED_1:15; :: thesis: verum

end;

hence ( f - g is negligible implies f negligibleEQ g ) ; :: thesis: verum