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 |^ ()

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 |^ ()

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 |^ () )

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 |^ ()

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 |^ () )

assume A2: for i being object st i in dom x holds
|.(x . i).| <= r ; :: thesis: |.(eval (b,x)).| <= r |^ ()
reconsider FR = F_Real as Field ;
reconsider X = x as Function of n, the carrier of F_Real ;
set sgm = SgmX ((),());
set B = b * (SgmX ((),()));
A3: ( rng (SgmX ((),())) c= n & n = dom b ) by ;
then A4: dom (b * (SgmX ((),()))) = dom (SgmX ((),())) by RELAT_1:27;
then A5: len (b * (SgmX ((),()))) = len (SgmX ((),())) by FINSEQ_3:29;
dom x = n by FUNCT_2:def 1;
then A6: dom (x * (SgmX ((),()))) = dom (SgmX ((),())) by ;
consider y being FinSequence of FR such that
A7: ( len y = len (SgmX ((),())) & eval (b,x) = Product y ) and
A8: for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = () . (((x * (SgmX ((),()))) /. i),((b * (SgmX ((),()))) /. i)) by POLYNOM2:def 2;
rng (b * (SgmX ((),()))) c= NAT by VALUED_0:def 6;
then reconsider B = b * (SgmX ((),())) as FinSequence of NAT by FINSEQ_1:def 4;
reconsider Y = y as FinSequence of F_Real ;
defpred S1[ 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: S1[ 0 ] by ;
A10: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
set i1 = i + 1;
assume that
A11: S1[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 ;
i + 1 in dom y by ;
then ( y | (i + 1) = (y | i) ^ <*(y . (i + 1))*> & y . (i + 1) = y /. (i + 1) ) by ;
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 ;
i + 1 in dom B by ;
then A17: ( B | (i + 1) = (B | i) ^ <*(B . (i + 1))*> & B . (i + 1) = B /. (i + 1) & B . (i + 1) = b . ((SgmX ((),())) . (i + 1)) ) by ;
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
y /. (i + 1) = () . (((x * (SgmX ((),()))) /. (i + 1)),(B /. (i + 1))) by
.= ((x * (SgmX ((),()))) /. (i + 1)) |^ (B /. (i + 1)) by NIVEN:7 ;
then A20: |.yi1.| = |.((x * (SgmX ((),()))) /. (i + 1)).| |^ (B /. (i + 1)) by TAYLOR_2:1;
i + 1 in dom (x * (SgmX ((),()))) by ;
then A21: ( (x * (SgmX ((),()))) /. (i + 1) = (x * (SgmX ((),()))) . (i + 1) & (x * (SgmX ((),()))) . (i + 1) = x . ((SgmX ((),())) . (i + 1)) & (SgmX ((),())) . (i + 1) in dom x & i + 1 in dom (SgmX ((),())) ) by ;
RelIncl n linearly_orders support b by PRE_POLY:82;
then ( (SgmX ((),())) . (i + 1) in rng (SgmX ((),())) & rng (SgmX ((),())) = support b ) by ;
then B /. (i + 1) <> 0 by ;
then A22: B /. (i + 1) >= 1 + 0 by NAT_1:13;
per cases ( |.((x * (SgmX ((),()))) /. (i + 1)).| > 0 or |.((x * (SgmX ((),()))) /. (i + 1)).| = 0 ) by COMPLEX1:46;
suppose |.((x * (SgmX ((),()))) /. (i + 1)).| > 0 ; :: thesis: |.yi1.| <= r |^ (B /. (i + 1))
hence |.yi1.| <= r |^ (B /. (i + 1)) by ; :: thesis: verum
end;
suppose |.((x * (SgmX ((),()))) /. (i + 1)).| = 0 ; :: thesis: |.yi1.| <= r |^ (B /. (i + 1))
then |.((x * (SgmX ((),()))) /. (i + 1)).| |^ (B /. (i + 1)) = 0 by ;
hence |.yi1.| <= r |^ (B /. (i + 1)) by ; :: thesis: verum
end;
end;
end;
A23: |.Pi.| >= 0 by COMPLEX1:46;
|.yi1.| >= 0 by COMPLEX1:46;
hence |.P.| <= r |^ (Sum (B | (i + 1))) by ; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A9, A10);
then S1[ len y] ;
then |.(eval (b,x)).| <= r |^ (Sum (B | (len B))) by A5, A7;
hence |.(eval (b,x)).| <= r |^ () by Th4; :: thesis: verum