set h = a (#) f;

per cases ( a = 0 or a <> 0 ) ;

suppose CS1: a = 0 ; :: thesis: for b₁ being Function of NAT,REAL st b₁ = a (#) f holds
b₁ is polynomially-abs-bounded

X0: dom (a (#) f) = NAT by FUNCT_2:def 1;

now :: thesis: for z being object st z in dom (a (#) f) holds
(a (#) f) . z = 0

let z be object ; :: thesis: ( z in dom (a (#) f) implies (a (#) f) . z = 0 )
assume z in dom (a (#) f) ; :: thesis: (a (#) f) . z = 0
then reconsider n = z as Element of NAT ;
thus (a (#) f) . z = 0 * (f . n) by CS1, VALUED_1:6
.= 0 ; :: thesis: verum

end;

then a (#) f = NAT --> 0 by FUNCOP_1:11, X0;
hence for b₁ being Function of NAT,REAL st b₁ = a (#) f holds
b₁ is polynomially-abs-bounded by LM1; :: thesis: verum

end;

suppose A0: a <> 0 ; :: thesis: for b₁ being Function of NAT,REAL st b₁ = a (#) f holds
b₁ is polynomially-abs-bounded

A3: for n being Nat holds |.(a (#) f).| . n = |.a.| * (|.f.| . n)

proof

let n be Nat; :: thesis: |.(a (#) f).| . n = |.a.| * (|.f.| . n)
thus |.(a (#) f).| . n = |.((a (#) f) . n).| by VALUED_1:18
.= |.(a * (f . n)).| by VALUED_1:6
.= |.a.| * |.(f . n).| by COMPLEX1:65
.= |.a.| * (|.f.| . 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 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 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;
set c = |.a.| * c1;
reconsider t = |.(a (#) f).| as Element of Funcs (NAT,REAL) by FUNCT_2:8;

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

let n be Element of NAT ; :: thesis: ( n >= N1 + 2 implies ( t . n <= (|.a.| * c1) * ((seq_n^ k1) . n) & 0 <= t . n ) )
assume B11: n >= N1 + 2 ; :: thesis: ( t . n <= (|.a.| * c1) * ((seq_n^ k1) . n) & 0 <= t . n )
( N1 <= N1 + 2 & 2 <= N1 + 2 ) by NAT_1:12;
then ( N1 <= n & 2 <= n ) by B11, XXREAL_0:2;
then A13: ( t1 . n <= c1 * ((seq_n^ k1) . n) & t1 . n >= 0 ) by A8;
then A15: |.a.| * (t1 . n) <= |.a.| * (c1 * ((seq_n^ k1) . n)) by XREAL_1:66;
thus t . n <= (|.a.| * c1) * ((seq_n^ k1) . n) by A15, A3, A6; :: thesis: 0 <= t . n
0 <= |.a.| * (t1 . n) by A13;
hence 0 <= t . n by A3, A6; :: thesis: verum

end;

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

end;

end;