set h = f + g;
A3: for n being Nat holds |.(f + g).| . n <= (|.f.| . n) + (|.g.| . n)

proof

let n be Nat; :: thesis: |.(f + g).| . n <= (|.f.| . n) + (|.g.| . n)
S1: n in NAT by ORDINAL1:def 12;
A30: |.(f + g).| . n = |.((f + g) . n).| by VALUED_1:18
.= |.((f . n) + (g . n)).| by S1, VALUED_1:1 ;
|.(f . n).| + |.(g . n).| = (|.f.| . n) + |.(g . n).| by VALUED_1:18
.= (|.f.| . n) + (|.g.| . n) by VALUED_1:18 ;
hence |.(f + g).| . n <= (|.f.| . n) + (|.g.| . n) by COMPLEX1:56, A30; :: thesis: verum

end;

consider k1 being Nat such that
A4: |.f.| in Big_Oh (seq_n^ k1) by defabs;
consider k2 being Nat such that
A5: |.g.| in Big_Oh (seq_n^ k2) by defabs;
consider t1 being Element of Funcs (NAT,REAL) such that
A6: ( |.f.| = t1 & ex c1 being Real ex N1 being Element of NAT st
( c1 > 0 & ( for n being Element of NAT st n >= N1 holds
( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) ) ) ) by A4;
consider t2 being Element of Funcs (NAT,REAL) such that
A7: ( |.g.| = t2 & ex c2 being Real ex N2 being Element of NAT st
( c2 > 0 & ( for n being Element of NAT st n >= N2 holds
( t2 . n <= c2 * ((seq_n^ k2) . n) & t2 . n >= 0 ) ) ) ) by A5;
consider c1 being Real, N1 being Element of NAT such that
A8: ( c1 > 0 & ( for n being Element of NAT st n >= N1 holds
( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) ) ) by A6;
consider c2 being Real, N2 being Element of NAT such that
A9: ( c2 > 0 & ( for n being Element of NAT st n >= N2 holds
( t2 . n <= c2 * ((seq_n^ k2) . n) & t2 . n >= 0 ) ) ) by A7;
set c = c1 + c2;
set N = N1 + N2;
set k = k1 + k2;
reconsider t = |.(f + g).| as Element of Funcs (NAT,REAL) by FUNCT_2:8;

now :: thesis: for n being Element of NAT st n >= (N1 + N2) + 2 holds
( t . n <= (c1 + c2) * ((seq_n^ (k1 + k2)) . n) & 0 <= t . n )

let n be Element of NAT ; :: thesis: ( n >= (N1 + N2) + 2 implies ( t . n <= (c1 + c2) * ((seq_n^ (k1 + k2)) . n) & 0 <= t . n ) )
assume B11: n >= (N1 + N2) + 2 ; :: thesis: ( t . n <= (c1 + c2) * ((seq_n^ (k1 + k2)) . n) & 0 <= t . n )
( N1 + N2 <= (N1 + N2) + 2 & 2 <= (N1 + N2) + 2 ) by NAT_1:12;
then A11: ( N1 + N2 <= n & 2 <= n ) by B11, XXREAL_0:2;
( N1 <= N1 + N2 & N2 <= N1 + N2 ) by NAT_1:12;
then A12: ( N1 <= n & N2 <= n ) by A11, XXREAL_0:2;
then A13: ( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) by A8;
A14: ( t2 . n <= c2 * ((seq_n^ k2) . n) & t2 . n >= 0 ) by A12, A9;
B15: 1 < n by A11, XXREAL_0:2;
B14: ( k1 <= k1 + k2 & k2 <= k1 + k2 ) by NAT_1:12;
S1: (seq_n^ k1) . n = n to_power k1 by B11, ASYMPT_1:def 3;
S2: (seq_n^ k2) . n = n to_power k2 by B11, ASYMPT_1:def 3;
S3: (seq_n^ (k1 + k2)) . n = n to_power (k1 + k2) by B11, ASYMPT_1:def 3;
( k1 < k1 + k2 or k1 = k1 + k2 ) by XXREAL_0:1, B14;
then (seq_n^ k1) . n <= (seq_n^ (k1 + k2)) . n by S1, S3, B15, POWER:39;
then S4: c1 * ((seq_n^ k1) . n) <= c1 * ((seq_n^ (k1 + k2)) . n) by XREAL_1:64, A8;
( k2 < k1 + k2 or k2 = k1 + k2 ) by XXREAL_0:1, B14;
then (seq_n^ k2) . n <= (seq_n^ (k1 + k2)) . n by S2, S3, B15, POWER:39;
then c2 * ((seq_n^ k2) . n) <= c2 * ((seq_n^ (k1 + k2)) . n) by XREAL_1:64, A9;
then S6: (c1 * ((seq_n^ k1) . n)) + (c2 * ((seq_n^ k2) . n)) <= (c1 * ((seq_n^ (k1 + k2)) . n)) + (c2 * ((seq_n^ (k1 + k2)) . n)) by S4, XREAL_1:7;
(t1 . n) + (t2 . n) <= (c1 * ((seq_n^ k1) . n)) + (c2 * ((seq_n^ k2) . n)) by XREAL_1:7, A13, A14;
then A15: (t1 . n) + (t2 . n) <= (c1 + c2) * ((seq_n^ (k1 + k2)) . n) by S6, XXREAL_0:2;
t . n <= (t1 . n) + (t2 . n) by A3, A6, A7;
hence t . n <= (c1 + c2) * ((seq_n^ (k1 + k2)) . n) by A15, XXREAL_0:2; :: thesis: 0 <= t . n
|.(f + g).| . n = |.((f + g) . n).| by VALUED_1:18;
hence 0 <= t . n ; :: thesis: verum

end;

then |.(f + g).| in Big_Oh (seq_n^ (k1 + k2)) by A8, A9;
hence for b₁ being Function of NAT,REAL st b₁ = f + g holds
b₁ is polynomially-abs-bounded ; :: thesis: verum