defpred S1[ Nat] means for F being FinSequence of REAL st ( for k being Element of NAT st k in dom F holds
0 <= F . k ) & len F = \$1 holds
0 <= Product F;
let F be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom F holds
0 <= F . k ) implies 0 <= Product F )

A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
for F being FinSequence of REAL st ( for k being Element of NAT st k in dom F holds
0 <= F . k ) & len F = n + 1 holds
0 <= Product F
proof
let F be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom F holds
0 <= F . k ) & len F = n + 1 implies 0 <= Product F )

assume A3: for k being Element of NAT st k in dom F holds
0 <= F . k ; :: thesis: ( not len F = n + 1 or 0 <= Product F )
assume A4: len F = n + 1 ; :: thesis:
then consider F1, F2 being FinSequence of REAL such that
A5: len F1 = n and
A6: len F2 = 1 and
A7: F = F1 ^ F2 by FINSEQ_2:23;
1 in Seg 1 ;
then 1 in dom F2 by ;
then A8: F . (n + 1) = F2 . 1 by ;
for k being Element of NAT st k in dom F1 holds
0 <= F1 . k
proof
let k be Element of NAT ; :: thesis: ( k in dom F1 implies 0 <= F1 . k )
assume A9: k in dom F1 ; :: thesis: 0 <= F1 . k
then 0 <= F . k by ;
hence 0 <= F1 . k by ; :: thesis: verum
end;
then A10: 0 <= Product F1 by A2, A5;
set x = F2 . 1;
Seg (n + 1) = dom F by ;
then A11: 0 <= F2 . 1 by ;
Product F = Product (F1 ^ <*(F2 . 1)*>) by
.= (Product F1) * (F2 . 1) by RVSUM_1:96 ;
hence 0 <= Product F by ; :: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
A12: S1[ 0 ]
proof
let F be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom F holds
0 <= F . k ) & len F = 0 implies 0 <= Product F )

assume for k being Element of NAT st k in dom F holds
0 <= F . k ; :: thesis: ( not len F = 0 or 0 <= Product F )
assume len F = 0 ; :: thesis:
then F = <*> REAL ;
hence 0 <= Product F by RVSUM_1:94; :: thesis: verum
end;
A13: for n being Nat holds S1[n] from NAT_1:sch 2(A12, A1);
A14: ex n being Element of NAT st n = len F ;
assume for k being Element of NAT st k in dom F holds
0 <= F . k ; :: thesis:
hence 0 <= Product F by ; :: thesis: verum