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_{1}[ Nat] means ( $1 <= len y implies |.(Sum (Y | $1)).| <= (Sum (H | $1)) * (r |^ (degree p)) );

A6: S_{1}[ 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_{1}[i] holds

S_{1}[i + 1]

A30: Sum (H | (len H)) = sum_of_coefficients |.p.| by A3, MATRPROB:36;

for i being Nat holds S_{1}[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

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

A6: S

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

S

proof

A29:
eval (p,x) = Sum (Y | (len y))
by A4, MATRPROB:36;
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_{1}[i] implies S_{1}[i + 1] )

assume A12: S_{1}[i]
; :: thesis: S_{1}[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;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

assume A12: S

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

A30: Sum (H | (len H)) = sum_of_coefficients |.p.| by A3, MATRPROB:36;

for i being Nat holds S

hence |.(eval (p,x)).| <= (sum_of_coefficients |.p.|) * (r |^ (degree p)) by A30, A7, A4, A29; :: thesis: verum