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)
thus |.(f (#) g).| . n = |.((f (#) g) . n).| by VALUED_1:18
.= |.((f . n) * (g . n)).| by VALUED_1:5
.= |.(f . n).| * |.(g . n).| by COMPLEX1:65
.= (|.f.| . n) * |.(g . n).| by VALUED_1:18
.= (|.f.| . n) * (|.g.| . n) by VALUED_1:18 ; :: 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 A11n: ( 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 A11n, 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;
A15: (t1 . n) * (t2 . n) <= (c1 * ((seq_n^ k1) . n)) * (c2 * ((seq_n^ k2) . n)) by XREAL_1:66, A13, A14;
(c1 * ((seq_n^ k1) . n)) * (c2 * ((seq_n^ k2) . n)) = (c1 * c2) * (((seq_n^ k1) . n) * ((seq_n^ k2) . n))
.= (c1 * c2) * ((n to_power k1) * ((seq_n^ k2) . n)) by B11, ASYMPT_1:def 3
.= (c1 * c2) * ((n to_power k1) * (n to_power k2)) by B11, ASYMPT_1:def 3
.= (c1 * c2) * (n to_power (k1 + k2)) by B11, POWER:27
.= (c1 * c2) * ((seq_n^ (k1 + k2)) . n) by B11, ASYMPT_1:def 3 ;
hence t . n <= (c1 * c2) * ((seq_n^ (k1 + k2)) . n) by A15, A3, A6, A7; :: thesis: 0 <= t . n
0 <= (t1 . n) * (t2 . n) by A13, A14;
hence 0 <= t . n by A3, A6, A7; :: 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