let n be Ordinal; :: thesis: for b being bag of n

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 (b,x)).| <= r |^ (degree b)

let b be bag of n; :: 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 (b,x)).| <= r |^ (degree b)

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 (b,x)).| <= r |^ (degree b) )

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 (b,x)).| <= r |^ (degree b)

let x be Function of n,F_Real; :: thesis: ( ( for i being object st i in dom x holds

|.(x . i).| <= r ) implies |.(eval (b,x)).| <= r |^ (degree b) )

assume A2: for i being object st i in dom x holds

|.(x . i).| <= r ; :: thesis: |.(eval (b,x)).| <= r |^ (degree b)

reconsider FR = F_Real as Field ;

reconsider X = x as Function of n, the carrier of F_Real ;

set sgm = SgmX ((RelIncl n),(support b));

set B = b * (SgmX ((RelIncl n),(support b)));

A3: ( rng (SgmX ((RelIncl n),(support b))) c= n & n = dom b ) by PARTFUN1:def 2, RELAT_1:def 19;

then A4: dom (b * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) by RELAT_1:27;

then A5: len (b * (SgmX ((RelIncl n),(support b)))) = len (SgmX ((RelIncl n),(support b))) by FINSEQ_3:29;

dom x = n by FUNCT_2:def 1;

then A6: dom (x * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) by A3, RELAT_1:27;

consider y being FinSequence of FR such that

A7: ( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product y ) and

A8: for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power F_Real) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;

rng (b * (SgmX ((RelIncl n),(support b)))) c= NAT by VALUED_0:def 6;

then reconsider B = b * (SgmX ((RelIncl n),(support b))) as FinSequence of NAT by FINSEQ_1:def 4;

reconsider Y = y as FinSequence of F_Real ;

defpred S_{1}[ Nat] means ( $1 <= len y implies ( Product (y | $1) is Real & ( for P being Real st P = Product (y | $1) holds

|.P.| <= r |^ (Sum (B | $1)) ) ) );

reconsider ZERO = 0 as Nat ;

y | ZERO = <*> the carrier of F_Real ;

then Product (y | ZERO) = 1_ F_Real by GROUP_4:8;

then A9: S_{1}[ 0 ]
by NEWTON:4, RVSUM_1:72;

A10: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A9, A10);

then S_{1}[ len y]
;

then |.(eval (b,x)).| <= r |^ (Sum (B | (len B))) by A5, A7;

hence |.(eval (b,x)).| <= r |^ (degree b) by Th4; :: 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 (b,x)).| <= r |^ (degree b)

let b be bag of n; :: 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 (b,x)).| <= r |^ (degree b)

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 (b,x)).| <= r |^ (degree b) )

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 (b,x)).| <= r |^ (degree b)

let x be Function of n,F_Real; :: thesis: ( ( for i being object st i in dom x holds

|.(x . i).| <= r ) implies |.(eval (b,x)).| <= r |^ (degree b) )

assume A2: for i being object st i in dom x holds

|.(x . i).| <= r ; :: thesis: |.(eval (b,x)).| <= r |^ (degree b)

reconsider FR = F_Real as Field ;

reconsider X = x as Function of n, the carrier of F_Real ;

set sgm = SgmX ((RelIncl n),(support b));

set B = b * (SgmX ((RelIncl n),(support b)));

A3: ( rng (SgmX ((RelIncl n),(support b))) c= n & n = dom b ) by PARTFUN1:def 2, RELAT_1:def 19;

then A4: dom (b * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) by RELAT_1:27;

then A5: len (b * (SgmX ((RelIncl n),(support b)))) = len (SgmX ((RelIncl n),(support b))) by FINSEQ_3:29;

dom x = n by FUNCT_2:def 1;

then A6: dom (x * (SgmX ((RelIncl n),(support b)))) = dom (SgmX ((RelIncl n),(support b))) by A3, RELAT_1:27;

consider y being FinSequence of FR such that

A7: ( len y = len (SgmX ((RelIncl n),(support b))) & eval (b,x) = Product y ) and

A8: for i being Element of NAT st 1 <= i & i <= len y holds

y /. i = (power F_Real) . (((x * (SgmX ((RelIncl n),(support b)))) /. i),((b * (SgmX ((RelIncl n),(support b)))) /. i)) by POLYNOM2:def 2;

rng (b * (SgmX ((RelIncl n),(support b)))) c= NAT by VALUED_0:def 6;

then reconsider B = b * (SgmX ((RelIncl n),(support b))) as FinSequence of NAT by FINSEQ_1:def 4;

reconsider Y = y as FinSequence of F_Real ;

defpred S

|.P.| <= r |^ (Sum (B | $1)) ) ) );

reconsider ZERO = 0 as Nat ;

y | ZERO = <*> the carrier of F_Real ;

then Product (y | ZERO) = 1_ F_Real by GROUP_4:8;

then A9: S

A10: for i being Nat st S

S

proof

for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

set i1 = i + 1;

assume that

A11: S_{1}[i]
and

A12: i + 1 <= len y ; :: thesis: ( Product (y | (i + 1)) is Real & ( for P being Real st P = Product (y | (i + 1)) holds

|.P.| <= r |^ (Sum (B | (i + 1))) ) )

reconsider yi1 = y /. (i + 1), Pi = Product (y | i) as Real ;

A13: |.Pi.| <= r |^ (Sum (B | i)) by A12, A11, NAT_1:13;

i + 1 in dom y by A12, NAT_1:11, FINSEQ_3:25;

then ( y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> & y . (i + 1) = y /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;

then A14: Product (y | (i + 1)) = (Product (y | i)) * (y /. (i + 1)) by GROUP_4:6

.= Pi * yi1 by BINOP_2:def 11 ;

thus Product (y | (i + 1)) is Real ; :: thesis: for P being Real st P = Product (y | (i + 1)) holds

|.P.| <= r |^ (Sum (B | (i + 1)))

let P be Real; :: thesis: ( P = Product (y | (i + 1)) implies |.P.| <= r |^ (Sum (B | (i + 1))) )

assume A15: P = Product (y | (i + 1)) ; :: thesis: |.P.| <= r |^ (Sum (B | (i + 1)))

A16: |.P.| = |.Pi.| * |.yi1.| by A15, A14, COMPLEX1:65;

i + 1 in dom B by A7, A12, A4, NAT_1:11, FINSEQ_3:25;

then A17: ( B | (i + 1) = (B | i) ^ <*(B . (i + 1))*> & B . (i + 1) = B /. (i + 1) & B . (i + 1) = b . ((SgmX ((RelIncl n),(support b))) . (i + 1)) ) by FINSEQ_5:10, PARTFUN1:def 6, FUNCT_1:12;

then Sum (B | (i + 1)) = (Sum (B | i)) + (B /. (i + 1)) by RVSUM_1:74;

then A18: r |^ (Sum (B | (i + 1))) = (r |^ (Sum (B | i))) * (r |^ (B /. (i + 1))) by NEWTON:8;

A19: |.yi1.| <= r |^ (B /. (i + 1))

|.yi1.| >= 0 by COMPLEX1:46;

hence |.P.| <= r |^ (Sum (B | (i + 1))) by A13, A18, A23, A16, A19, XREAL_1:66; :: thesis: verum

end;set i1 = i + 1;

assume that

A11: S

A12: i + 1 <= len y ; :: thesis: ( Product (y | (i + 1)) is Real & ( for P being Real st P = Product (y | (i + 1)) holds

|.P.| <= r |^ (Sum (B | (i + 1))) ) )

reconsider yi1 = y /. (i + 1), Pi = Product (y | i) as Real ;

A13: |.Pi.| <= r |^ (Sum (B | i)) by A12, A11, NAT_1:13;

i + 1 in dom y by A12, NAT_1:11, FINSEQ_3:25;

then ( y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> & y . (i + 1) = y /. (i + 1) ) by FINSEQ_5:10, PARTFUN1:def 6;

then A14: Product (y | (i + 1)) = (Product (y | i)) * (y /. (i + 1)) by GROUP_4:6

.= Pi * yi1 by BINOP_2:def 11 ;

thus Product (y | (i + 1)) is Real ; :: thesis: for P being Real st P = Product (y | (i + 1)) holds

|.P.| <= r |^ (Sum (B | (i + 1)))

let P be Real; :: thesis: ( P = Product (y | (i + 1)) implies |.P.| <= r |^ (Sum (B | (i + 1))) )

assume A15: P = Product (y | (i + 1)) ; :: thesis: |.P.| <= r |^ (Sum (B | (i + 1)))

A16: |.P.| = |.Pi.| * |.yi1.| by A15, A14, COMPLEX1:65;

i + 1 in dom B by A7, A12, A4, NAT_1:11, FINSEQ_3:25;

then A17: ( B | (i + 1) = (B | i) ^ <*(B . (i + 1))*> & B . (i + 1) = B /. (i + 1) & B . (i + 1) = b . ((SgmX ((RelIncl n),(support b))) . (i + 1)) ) by FINSEQ_5:10, PARTFUN1:def 6, FUNCT_1:12;

then Sum (B | (i + 1)) = (Sum (B | i)) + (B /. (i + 1)) by RVSUM_1:74;

then A18: r |^ (Sum (B | (i + 1))) = (r |^ (Sum (B | i))) * (r |^ (B /. (i + 1))) by NEWTON:8;

A19: |.yi1.| <= r |^ (B /. (i + 1))

proof

A23:
|.Pi.| >= 0
by COMPLEX1:46;
y /. (i + 1) =
(power F_Real) . (((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)),(B /. (i + 1)))
by A8, A12, NAT_1:11

.= ((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)) |^ (B /. (i + 1)) by NIVEN:7 ;

then A20: |.yi1.| = |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| |^ (B /. (i + 1)) by TAYLOR_2:1;

i + 1 in dom (x * (SgmX ((RelIncl n),(support b)))) by A6, A7, A12, NAT_1:11, FINSEQ_3:25;

then A21: ( (x * (SgmX ((RelIncl n),(support b)))) /. (i + 1) = (x * (SgmX ((RelIncl n),(support b)))) . (i + 1) & (x * (SgmX ((RelIncl n),(support b)))) . (i + 1) = x . ((SgmX ((RelIncl n),(support b))) . (i + 1)) & (SgmX ((RelIncl n),(support b))) . (i + 1) in dom x & i + 1 in dom (SgmX ((RelIncl n),(support b))) ) by PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;

RelIncl n linearly_orders support b by PRE_POLY:82;

then ( (SgmX ((RelIncl n),(support b))) . (i + 1) in rng (SgmX ((RelIncl n),(support b))) & rng (SgmX ((RelIncl n),(support b))) = support b ) by A21, FUNCT_1:def 3, PRE_POLY:def 2;

then B /. (i + 1) <> 0 by A17, PRE_POLY:def 7;

then A22: B /. (i + 1) >= 1 + 0 by NAT_1:13;

end;.= ((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)) |^ (B /. (i + 1)) by NIVEN:7 ;

then A20: |.yi1.| = |.((x * (SgmX ((RelIncl n),(support b)))) /. (i + 1)).| |^ (B /. (i + 1)) by TAYLOR_2:1;

i + 1 in dom (x * (SgmX ((RelIncl n),(support b)))) by A6, A7, A12, NAT_1:11, FINSEQ_3:25;

then A21: ( (x * (SgmX ((RelIncl n),(support b)))) /. (i + 1) = (x * (SgmX ((RelIncl n),(support b)))) . (i + 1) & (x * (SgmX ((RelIncl n),(support b)))) . (i + 1) = x . ((SgmX ((RelIncl n),(support b))) . (i + 1)) & (SgmX ((RelIncl n),(support b))) . (i + 1) in dom x & i + 1 in dom (SgmX ((RelIncl n),(support b))) ) by PARTFUN1:def 6, FUNCT_1:11, FUNCT_1:12;

RelIncl n linearly_orders support b by PRE_POLY:82;

then ( (SgmX ((RelIncl n),(support b))) . (i + 1) in rng (SgmX ((RelIncl n),(support b))) & rng (SgmX ((RelIncl n),(support b))) = support b ) by A21, FUNCT_1:def 3, PRE_POLY:def 2;

then B /. (i + 1) <> 0 by A17, PRE_POLY:def 7;

then A22: B /. (i + 1) >= 1 + 0 by NAT_1:13;

|.yi1.| >= 0 by COMPLEX1:46;

hence |.P.| <= r |^ (Sum (B | (i + 1))) by A13, A18, A23, A16, A19, XREAL_1:66; :: thesis: verum

then S

then |.(eval (b,x)).| <= r |^ (Sum (B | (len B))) by A5, A7;

hence |.(eval (b,x)).| <= r |^ (degree b) by Th4; :: thesis: verum