let c, s be non empty positive-yielding XFinSequence of REAL ; :: thesis: ex d being non empty positive-yielding XFinSequence of REAL ex N being Nat st
for x being Nat st N <= x holds
((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x
consider a1 being Real, k1, N1 being Nat such that
P1: ( 0 < a1 & 0 < k1 & ( for x being Nat st N1 <= x holds
(polynom c) . x <= a1 * (x to_power k1) ) ) by LRNG1;
consider a2 being Real, k2, N2 being Nat such that
P2: ( 0 < a2 & 0 < k2 & ( for x being Nat st N2 <= x holds
(polynom s) . x <= a2 * (x to_power k2) ) ) by LRNG1;
consider d being non empty positive-yielding XFinSequence of REAL such that
P3: for x being Nat holds (a1 * a2) * (x to_power (k1 + k2)) <= (polynom d) . x by LRNG2;
set N = N1 + N2;
take d ; :: thesis: ex N being Nat st
for x being Nat st N <= x holds
((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x
take N1 + N2 ; :: thesis: for x being Nat st N1 + N2 <= x holds
((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x
let x be Nat; :: thesis: ( N1 + N2 <= x implies ((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x )
assume P4: N1 + N2 <= x ; :: thesis: ((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x
N1 <= N1 + N2 by NAT_1:12;
then N1 <= x by XXREAL_0:2, P4;
then P5: (polynom c) . x <= a1 * (x to_power k1) by P1;
N2 <= N1 + N2 by NAT_1:12;
then N2 <= x by XXREAL_0:2, P4;
then P6: (polynom s) . x <= a2 * (x to_power k2) by P2;
P7: 0 < (polynom c) . x by NLM3;
P8: 0 < (polynom s) . x by NLM3;
P9: ((polynom c) . x) * ((polynom s) . x) <= (a1 * (x to_power k1)) * (a2 * (x to_power k2)) by XREAL_1:66, P5, P6, P7, P8;
P10: (a1 * (x to_power k1)) * (a2 * (x to_power k2)) = (a1 * a2) * (x to_power (k1 + k2))

proof

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

suppose P11: x = 0 ; :: thesis: (a1 * (x to_power k1)) * (a2 * (x to_power k2)) = (a1 * a2) * (x to_power (k1 + k2))

P12: x to_power k1 = 0 by P1, P11, POWER:def 2;
x to_power (k1 + k2) = 0 by P2, P11, POWER:def 2;
hence (a1 * (x to_power k1)) * (a2 * (x to_power k2)) = (a1 * a2) * (x to_power (k1 + k2)) by P12; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: (a1 * (x to_power k1)) * (a2 * (x to_power k2)) = (a1 * a2) * (x to_power (k1 + k2))

then (x to_power k1) * (x to_power k2) = x to_power (k1 + k2) by POWER:27;
hence (a1 * (x to_power k1)) * (a2 * (x to_power k2)) = (a1 * a2) * (x to_power (k1 + k2)) ; :: thesis: verum

end;

end;

end;

(a1 * a2) * (x to_power (k1 + k2)) <= (polynom d) . x by P3;
hence ((polynom c) . x) * ((polynom s) . x) <= (polynom d) . x by P9, P10, XXREAL_0:2; :: thesis: verum