defpred S₁[ 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 S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[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: 0 <= Product F
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 A6, FINSEQ_1:def 3;
then A8: F . (n + 1) = F2 . 1 by A5, A7, FINSEQ_1:def 7;
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 A3, A7, FINSEQ_2:15;
hence 0 <= F1 . k by A7, A9, FINSEQ_1:def 7; :: thesis: verum

end;

then A10: 0 <= Product F1 by A2, A5;
set x = F2 . 1;
Seg (n + 1) = dom F by A4, FINSEQ_1:def 3;
then A11: 0 <= F2 . 1 by A3, A8, FINSEQ_1:3;
Product F = Product (F1 ^ <*(F2 . 1)*>) by A6, A7, FINSEQ_1:40
.= (Product F1) * (F2 . 1) by RVSUM_1:96 ;
hence 0 <= Product F by A10, A11; :: thesis: verum

end;

hence S₁[n + 1] ; :: thesis: verum

end;

A12: S₁[ 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: 0 <= Product F
then F = <*> REAL ;
hence 0 <= Product F by RVSUM_1:94; :: thesis: verum

end;

A13: for n being Nat holds S₁[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: 0 <= Product F
hence 0 <= Product F by A13, A14; :: thesis: verum