let n be Ordinal; :: thesis: for p being Polynomial of n,F_Real
for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (p,x)).| <= * (r |^ ())

let p be Polynomial of n,F_Real; :: thesis: for r being Real st r >= 1 holds
for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (p,x)).| <= * (r |^ ())

let r be Real; :: thesis: ( r >= 1 implies for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (p,x)).| <= * (r |^ ()) )

assume A1: r >= 1 ; :: thesis: for x being Function of n, the carrier of F_Real st ( for i being object st i in dom x holds
|.(x . i).| <= r ) holds
|.(eval (p,x)).| <= * (r |^ ())

let x be Function of n, the carrier of F_Real; :: thesis: ( ( for i being object st i in dom x holds
|.(x . i).| <= r ) implies |.(eval (p,x)).| <= * (r |^ ()) )

assume A2: for i being object st i in dom x holds
|.(x . i).| <= r ; :: thesis: |.(eval (p,x)).| <= * (r |^ ())
reconsider FR = F_Real as Field ;
reconsider pF = p, ApF = |.p.| as Polynomial of n,FR ;
reconsider xF = x as Function of n, the carrier of FR ;
set sgm = SgmX ((),());
set SgmF = SgmX ((),(Support pF));
reconsider H = ApF * (SgmX ((),(Support pF))) as FinSequence of the carrier of F_Real ;
A3: sum_of_coefficients |.p.| = Sum (ApF * (SgmX ((),(Support pF)))) by Th3;
consider y being FinSequence of the carrier of FR such that
A4: ( len y = len (SgmX ((),(Support pF))) & eval (p,x) = Sum y ) and
A5: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((pF * (SgmX ((),(Support pF)))) /. i) * (eval (((SgmX ((),(Support pF))) /. i),xF)) by POLYNOM2:def 4;
reconsider Y = y as FinSequence of REAL ;
defpred S1[ Nat] means ( \$1 <= len y implies |.(Sum (Y | \$1)).| <= (Sum (H | \$1)) * (r |^ ()) );
A6: S1[ 0 ] ;
A7: len (ApF * (SgmX ((),(Support pF)))) = len (SgmX ((),(Support pF))) by CARD_1:def 7;
A8: for i being Nat st S1[i] holds
S1[i + 1]
proof
A9: BagOrder n linearly_orders Support p by POLYNOM2:18;
A10: rng (SgmX ((),())) = Support p by ;
A11: len (p * (SgmX ((),()))) = len (SgmX ((),())) by CARD_1:def 7;
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A12: S1[i] ; :: thesis: S1[i + 1]
set i1 = i + 1;
assume A13: i + 1 <= len y ; :: thesis: |.(Sum (Y | (i + 1))).| <= (Sum (H | (i + 1))) * (r |^ ())
then i + 1 in dom y by ;
then A14: ( y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> & y . (i + 1) = y /. (i + 1) & Y . (i + 1) = Y /. (i + 1) ) by ;
A15: Sum (y | i) = Sum (Y | i) by MATRPROB:36;
A16: Sum (Y | (i + 1)) = Sum (y | (i + 1)) by MATRPROB:36
.= (Sum (y | i)) + (Sum <*(y /. (i + 1))*>) by
.= addreal . ((Sum (y | i)),(y /. (i + 1))) by RLVECT_1:44
.= (Sum (Y | i)) + (Y /. (i + 1)) by ;
i + 1 in dom (ApF * (SgmX ((),(Support pF)))) by ;
then A17: ( H | (i + 1) = (H | i) ^ <*(H . (i + 1))*> & H /. (i + 1) = H . (i + 1) & (ApF * (SgmX ((),(Support pF)))) /. (i + 1) = (ApF * (SgmX ((),(Support pF)))) . (i + 1) & (ApF * (SgmX ((),(Support pF)))) . (i + 1) = ApF . ((SgmX ((),(Support pF))) . (i + 1)) ) by ;
A18: Sum (H | (i + 1)) = Sum ((ApF * (SgmX ((),(Support pF)))) | (i + 1)) by MATRPROB:36
.= (Sum ((ApF * (SgmX ((),(Support pF)))) | i)) + (Sum <*((ApF * (SgmX ((),(Support pF)))) /. (i + 1))*>) by
.= the addF of FR . ((Sum ((ApF * (SgmX ((),(Support pF)))) | i)),((ApF * (SgmX ((),(Support pF)))) /. (i + 1))) by RLVECT_1:44
.= addreal . ((Sum (H | i)),(H /. (i + 1))) by MATRPROB:36
.= (Sum (H | i)) + (H /. (i + 1)) by BINOP_2:def 9 ;
A19: ( |.((p * (SgmX ((),()))) /. (i + 1)).| >= 0 & |.(eval (((SgmX ((),())) /. (i + 1)),x)).| >= 0 ) by COMPLEX1:46;
A20: ((pF * (SgmX ((),(Support pF)))) /. (i + 1)) * (eval (((SgmX ((),(Support pF))) /. (i + 1)),xF)) = ((p * (SgmX ((),()))) /. (i + 1)) * (eval (((SgmX ((),())) /. (i + 1)),x)) by BINOP_2:def 11;
i + 1 in dom (p * (SgmX ((),()))) by ;
then A21: ( (p * (SgmX ((),()))) . (i + 1) = (p * (SgmX ((),()))) /. (i + 1) & (p * (SgmX ((),()))) . (i + 1) = p . ((SgmX ((),())) . (i + 1)) & i + 1 in dom (SgmX ((),())) ) by ;
then A22: ( (SgmX ((),())) . (i + 1) in rng (SgmX ((),())) & (SgmX ((),())) . (i + 1) = (SgmX ((),())) /. (i + 1) ) by ;
A23: H /. (i + 1) = |.p.| . ((SgmX ((),())) /. (i + 1)) by
.= |.(p . ((SgmX ((),())) /. (i + 1))).| by Def1 ;
A24: |.((p * (SgmX ((),()))) /. (i + 1)).| <= H /. (i + 1) by ;
A25: r |^ (degree ((SgmX ((),())) /. (i + 1))) <= r |^ () by ;
|.(eval (((SgmX ((),())) /. (i + 1)),x)).| <= r |^ (degree ((SgmX ((),())) /. (i + 1))) by A1, A2, Th9;
then |.(eval (((SgmX ((),())) /. (i + 1)),x)).| <= r |^ () by ;
then |.((p * (SgmX ((),()))) /. (i + 1)).| * |.(eval (((SgmX ((),())) /. (i + 1)),x)).| <= (H /. (i + 1)) * (r |^ ()) by ;
then A26: |.(((p * (SgmX ((),()))) /. (i + 1)) * (eval (((SgmX ((),())) /. (i + 1)),x))).| <= (H /. (i + 1)) * (r |^ ()) by COMPLEX1:65;
A27: |.(Y /. (i + 1)).| <= (H /. (i + 1)) * (r |^ ()) by ;
A28: |.(Sum (Y | i)).| + |.(Y /. (i + 1)).| >= |.((Sum (Y | i)) + (Y /. (i + 1))).| by COMPLEX1:56;
|.(Sum (Y | i)).| + |.(Y /. (i + 1)).| <= ((Sum (H | i)) * (r |^ ())) + ((H /. (i + 1)) * (r |^ ())) by ;
hence |.(Sum (Y | (i + 1))).| <= (Sum (H | (i + 1))) * (r |^ ()) by ; :: thesis: verum
end;
A29: eval (p,x) = Sum (Y | (len y)) by ;
A30: Sum (H | (len H)) = sum_of_coefficients |.p.| by ;
for i being Nat holds S1[i] from NAT_1:sch 2(A6, A8);
hence |.(eval (p,x)).| <= * (r |^ ()) by A30, A7, A4, A29; :: thesis: verum