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)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))
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)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))
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)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p)) )
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)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))
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)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p)) )
assume A2: for i being object st i in dom x holds
|.(x . i).| <= r ; :: thesis: |.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p))
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 ((BagOrder n),(Support p));
set SgmF = SgmX ((BagOrder n),(Support pF));
reconsider H = ApF * (SgmX ((BagOrder n),(Support pF))) as FinSequence of the carrier of F_Real ;
A3: sum_of_coefficients |.p.| = Sum (ApF * (SgmX ((BagOrder n),(Support pF)))) by Th3;
consider y being FinSequence of the carrier of FR such that
A4: ( len y = len (SgmX ((BagOrder n),(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 ((BagOrder n),(Support pF)))) /. i) * (eval (((SgmX ((BagOrder n),(Support pF))) /. i),xF)) by POLYNOM2:def 4;
reconsider Y = y as FinSequence of REAL ;
defpred S₁[ Nat] means ( $1 <= len y implies |.(Sum (Y | $1)).| <= (Sum (H | $1)) * (r |^ (degree p)) );
A6: S₁[ 0 ] ;
A7: len (ApF * (SgmX ((BagOrder n),(Support pF)))) = len (SgmX ((BagOrder n),(Support pF))) by CARD_1:def 7;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

A9: BagOrder n linearly_orders Support p by POLYNOM2:18;
A10: rng (SgmX ((BagOrder n),(Support p))) = Support p by A9, PRE_POLY:def 2;
A11: len (p * (SgmX ((BagOrder n),(Support p)))) = len (SgmX ((BagOrder n),(Support p))) by CARD_1:def 7;
let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A12: S₁[i] ; :: thesis: S₁[i + 1]
set i1 = i + 1;
assume A13: i + 1 <= len y ; :: thesis: |.(Sum (Y | (i + 1))).| <= (Sum (H | (i + 1))) * (r |^ (degree p))
then i + 1 in dom y by NAT_1:11, FINSEQ_3:25;
then A14: ( y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> & y . (i + 1) = y /. (i + 1) & Y . (i + 1) = Y /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;
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 A14, RLVECT_1:41
.= addreal . ((Sum (y | i)),(y /. (i + 1))) by RLVECT_1:44
.= (Sum (Y | i)) + (Y /. (i + 1)) by A15, BINOP_2:def 9 ;
i + 1 in dom (ApF * (SgmX ((BagOrder n),(Support pF)))) by A4, A13, A7, NAT_1:11, FINSEQ_3:25;
then A17: ( H | (i + 1) = (H | i) ^ <*(H . (i + 1))*> & H /. (i + 1) = H . (i + 1) & (ApF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1) = (ApF * (SgmX ((BagOrder n),(Support pF)))) . (i + 1) & (ApF * (SgmX ((BagOrder n),(Support pF)))) . (i + 1) = ApF . ((SgmX ((BagOrder n),(Support pF))) . (i + 1)) ) by FINSEQ_5:10, PARTFUN1:def 6, FUNCT_1:12;
A18: Sum (H | (i + 1)) = Sum ((ApF * (SgmX ((BagOrder n),(Support pF)))) | (i + 1)) by MATRPROB:36
.= (Sum ((ApF * (SgmX ((BagOrder n),(Support pF)))) | i)) + (Sum <*((ApF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1))*>) by A17, RLVECT_1:41
.= the addF of FR . ((Sum ((ApF * (SgmX ((BagOrder n),(Support pF)))) | i)),((ApF * (SgmX ((BagOrder n),(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 ((BagOrder n),(Support p)))) /. (i + 1)).| >= 0 & |.(eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x)).| >= 0 ) by COMPLEX1:46;
A20: ((pF * (SgmX ((BagOrder n),(Support pF)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support pF))) /. (i + 1)),xF)) = ((p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x)) by BINOP_2:def 11;
i + 1 in dom (p * (SgmX ((BagOrder n),(Support p)))) by A4, A13, A11, NAT_1:11, FINSEQ_3:25;
then A21: ( (p * (SgmX ((BagOrder n),(Support p)))) . (i + 1) = (p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1) & (p * (SgmX ((BagOrder n),(Support p)))) . (i + 1) = p . ((SgmX ((BagOrder n),(Support p))) . (i + 1)) & i + 1 in dom (SgmX ((BagOrder n),(Support p))) ) by PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;
then A22: ( (SgmX ((BagOrder n),(Support p))) . (i + 1) in rng (SgmX ((BagOrder n),(Support p))) & (SgmX ((BagOrder n),(Support p))) . (i + 1) = (SgmX ((BagOrder n),(Support p))) /. (i + 1) ) by FUNCT_1:def 3, PARTFUN1:def 6;
A23: H /. (i + 1) = |.p.| . ((SgmX ((BagOrder n),(Support p))) /. (i + 1)) by A17, A21, PARTFUN1:def 6
.= |.(p . ((SgmX ((BagOrder n),(Support p))) /. (i + 1))).| by Def1 ;
A24: |.((p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1)).| <= H /. (i + 1) by PARTFUN1:def 6, A21, A23;
A25: r |^ (degree ((SgmX ((BagOrder n),(Support p))) /. (i + 1))) <= r |^ (degree p) by A1, PREPOWER:93, Th6, A22, A10;
|.(eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x)).| <= r |^ (degree ((SgmX ((BagOrder n),(Support p))) /. (i + 1))) by A1, A2, Th9;
then |.(eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x)).| <= r |^ (degree p) by A25, XXREAL_0:2;
then |.((p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1)).| * |.(eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x)).| <= (H /. (i + 1)) * (r |^ (degree p)) by A24, A19, XREAL_1:66;
then A26: |.(((p * (SgmX ((BagOrder n),(Support p)))) /. (i + 1)) * (eval (((SgmX ((BagOrder n),(Support p))) /. (i + 1)),x))).| <= (H /. (i + 1)) * (r |^ (degree p)) by COMPLEX1:65;
A27: |.(Y /. (i + 1)).| <= (H /. (i + 1)) * (r |^ (degree p)) by A20, A26, A5, A13, NAT_1:11;
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 |^ (degree p))) + ((H /. (i + 1)) * (r |^ (degree p))) by A27, XREAL_1:7, A13, A12, NAT_1:13;
hence |.(Sum (Y | (i + 1))).| <= (Sum (H | (i + 1))) * (r |^ (degree p)) by A16, A18, A28, XXREAL_0:2; :: thesis: verum

end;

A29: eval (p,x) = Sum (Y | (len y)) by A4, MATRPROB:36;
A30: Sum (H | (len H)) = sum_of_coefficients |.p.| by A3, MATRPROB:36;
for i being Nat holds S₁[i] from NAT_1:sch 2(A6, A8);
hence |.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p)) by A30, A7, A4, A29; :: thesis: verum