let f, g, h be Function of NAT,REAL; :: thesis: ( f negligibleEQ g & g negligibleEQ h implies f negligibleEQ h )
given v being Function of NAT,REAL such that B1: ( v is negligible & ( for x being Nat holds |.((f . x) - (g . x)).| <= |.(v . x).| ) ) ; :: according to ASYMPT_3:def 6 :: thesis: ( not g negligibleEQ h or f negligibleEQ h )
given w being Function of NAT,REAL such that B2: ( w is negligible & ( for x being Nat holds |.((g . x) - (h . x)).| <= |.(w . x).| ) ) ; :: according to ASYMPT_3:def 6 :: thesis: f negligibleEQ h
take u = |.v.| + |.w.|; :: according to ASYMPT_3:def 6 :: thesis: ( u is negligible & ( for x being Nat holds |.((f . x) - (h . x)).| <= |.(u . x).| ) )
thus u is negligible by B1, B2; :: thesis: for x being Nat holds |.((f . x) - (h . x)).| <= |.(u . x).|
let x be Nat; :: thesis: |.((f . x) - (h . x)).| <= |.(u . x).|
B4: |.((f . x) - (g . x)).| <= |.(v . x).| by B1;
B5: |.((g . x) - (h . x)).| <= |.(w . x).| by B2;
|.((f . x) - (h . x)).| = |.(((f . x) - (g . x)) + ((g . x) - (h . x))).| ;
then B6: |.((f . x) - (h . x)).| <= |.((f . x) - (g . x)).| + |.((g . x) - (h . x)).| by COMPLEX1:56;
|.((f . x) - (g . x)).| + |.((g . x) - (h . x)).| <= |.(v . x).| + |.(w . x).| by B4, B5, XREAL_1:7;
then B7: |.((f . x) - (h . x)).| <= |.(v . x).| + |.(w . x).| by B6, XXREAL_0:2;
x in NAT by ORDINAL1:def 12;
then consider y being Element of NAT such that
LXY: x = y ;
|.(v . x).| + |.(w . x).| = (|.v.| . x) + |.(w . x).| by SEQ_1:12
.= (|.v.| . x) + (|.w.| . x) by SEQ_1:12
.= (|.v.| + |.w.|) . x by LXY, VALUED_1:1 ;
hence |.((f . x) - (h . x)).| <= |.(u . x).| by B7, ABSVALUE:def 1; :: thesis: verum