let M be Element of F_Real; :: thesis: for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) holds
|.(Product F).| <= M |^ (len F)
defpred S₁[ Nat] means for F being FinSequence of F_Real st len F = $1 & ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) holds
|.(Product F).| <= M |^ (len F);
A1: S₁[ 0 ]

proof

let F be FinSequence of F_Real; :: thesis: ( len F = 0 & ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) implies |.(Product F).| <= M |^ (len F) )
assume A2: ( len F = 0 & ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) ) ; :: thesis: |.(Product F).| <= M |^ (len F)
A3: F is Element of the carrier of F_Real * by FINSEQ_1:def 11;
F in 0 -tuples_on the carrier of F_Real by A2, A3;
then A4: Product F = 1. F_Real by FVSUM_1:80
.= 1 ;
M |^ (len F) = 1_ F_Real by A2, BINOM:8
.= 1 ;
hence |.(Product F).| <= M |^ (len F) by A4, ABSVALUE:def 1; :: thesis: verum

end;

A5: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A6: S₁[n] ; :: thesis: S₁[n + 1]
let F1 be FinSequence of F_Real; :: thesis: ( len F1 = n + 1 & ( for i being Nat st i in dom F1 holds
|.(F1 . i).| <= M ) implies |.(Product F1).| <= M |^ (len F1) )
assume A7: ( len F1 = n + 1 & ( for i being Nat st i in dom F1 holds
|.(F1 . i).| <= M ) ) ; :: thesis: |.(Product F1).| <= M |^ (len F1)
A8: dom F1 = Seg (n + 1) by A7, FINSEQ_1:def 3;
F1 <> {} by A7;
then A9: F1 = <*(F1 /. 1)*> ^ (F1 /^ 1) by FINSEQ_5:29;
A10: len F1 >= 1 by A7, NAT_1:11;
then A11: len (F1 /^ 1) = (len F1) - 1 by RFINSEQ:def 1
.= n by A7 ;
for i being Nat st i in dom (F1 /^ 1) holds
|.((F1 /^ 1) . i).| <= M

proof

let i be Nat; :: thesis: ( i in dom (F1 /^ 1) implies |.((F1 /^ 1) . i).| <= M )
assume A12: i in dom (F1 /^ 1) ; :: thesis: |.((F1 /^ 1) . i).| <= M
then i in Seg n by A11, FINSEQ_1:def 3;
then A14: ( 1 <= i & i <= n ) by FINSEQ_1:1;
A15: 1 <= i + 1 by NAT_1:11;
i + 1 <= n + 1 by A14, XREAL_1:6;
then A17: i + 1 in dom F1 by A8, A15;
(F1 /^ 1) . i = F1 . (i + 1) by A12, A10, RFINSEQ:def 1;
hence |.((F1 /^ 1) . i).| <= M by A7, A17; :: thesis: verum

end;

then A19: |.(Product (F1 /^ 1)).| <= M |^ (len (F1 /^ 1)) by A6, A11;
( 1 <= 1 & 1 <= n + 1 ) by NAT_1:11;
then A21: 1 in dom F1 by A8;
then F1 /. 1 = F1 . 1 by PARTFUN1:def 6;
then A22: |.(F1 /. 1).| <= M by A7, A21;
Product F1 = (F1 /. 1) * (Product (F1 /^ 1)) by A9, FVSUM_1:78;
then A23: |.(Product F1).| = |.(F1 /. 1).| * |.(Product (F1 /^ 1)).| by COMPLEX1:65;
M * (M |^ n) = (M |^ 1) * (M |^ n) by BINOM:8
.= M |^ (len F1) by A7, BINOM:10 ;
hence |.(Product F1).| <= M |^ (len F1) by A23, A11, A22, A19, XREAL_1:66; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A5);
hence for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
|.(F . i).| <= M ) holds
|.(Product F).| <= M |^ (len F) ; :: thesis: verum