let p be prime odd Nat; :: thesis: for m being positive Nat
for x being Element of F_Real st 0 < x & x <= m holds
|.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m)
let m be positive Nat; :: thesis: for x being Element of F_Real st 0 < x & x <= m holds
|.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m)
let x be Element of F_Real; :: thesis: ( 0 < x & x <= m implies |.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m) )
assume A1: ( 0 < x & x <= m ) ; :: thesis: |.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m)
A2: len (x. (m,p)) = m by Def2;
A3: dom (x. (m,p)) = Seg (len (x. (m,p))) by FINSEQ_1:def 3
.= Seg m by Def2 ;
then A4: dom (^ (x. (m,p))) = Seg m by E_TRANS1:def 6;
Seg (len (eval ((^ (x. (m,p))),x))) = dom (eval ((^ (x. (m,p))),x)) by FINSEQ_1:def 3
.= Seg m by A4, E_TRANS1:def 7 ;
then A5: len (eval ((^ (x. (m,p))),x)) = m by FINSEQ_1:6;
not x. (m,p) is empty by A2;
then A6: eval ((~ (^ (Product (x. (m,p))))),x) = Product (eval ((^ (x. (m,p))),x)) by E_TRANS1:38;
reconsider m0 = m as Element of F_Real by NUMBERS:15, INT_1:def 2;
set M = m0 |^ p;
A7: m0 |^ p = m |^ p by Lm16;
A8: (m0 |^ p) |^ m = m0 |^ (p * m) by BINOM:11
.= m |^ (p * m) by Lm16 ;
for i being Nat st i in dom (eval ((^ (x. (m,p))),x)) holds
|.((eval ((^ (x. (m,p))),x)) . i).| <= m |^ p

proof

let i be Nat; :: thesis: ( i in dom (eval ((^ (x. (m,p))),x)) implies |.((eval ((^ (x. (m,p))),x)) . i).| <= m |^ p )
assume A10: i in dom (eval ((^ (x. (m,p))),x)) ; :: thesis: |.((eval ((^ (x. (m,p))),x)) . i).| <= m |^ p
then A11: i in dom (^ (x. (m,p))) by E_TRANS1:def 7;
A12: i in Seg m by A4, A10, E_TRANS1:def 7;
set F = x. (m,p);
A13: i in dom (x. (m,p)) by A3, A4, A10, E_TRANS1:def 7;
A14: (^ (x. (m,p))) /. i = (^ (x. (m,p))) . i by A11, PARTFUN1:def 6
.= ^ ((x. (m,p)) /. i) by A13, E_TRANS1:def 6 ;
(eval ((^ (x. (m,p))),x)) . i = eval ((~ (^ ((x. (m,p)) /. i))),x) by A14, A11, E_TRANS1:def 7;
hence |.((eval ((^ (x. (m,p))),x)) . i).| <= m |^ p by A12, Th39, A1; :: thesis: verum

end;

hence |.(eval ((~ (^ (Product (x. (m,p))))),x)).| <= m |^ (p * m) by A8, A5, A6, A7, Th41; :: thesis: verum