defpred S₁[ Nat] means for F being FinSequence of REAL st ( for k being Element of NAT st k in dom F holds
F . k > 0 ) & len F = $1 holds
Product F > 0 ;
let F be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom F holds
F . k > 0 ) implies Product F > 0 )
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
F . k > 0 ) & len F = n + 1 holds
Product F > 0

proof

let F be FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom F holds
F . k > 0 ) & len F = n + 1 implies Product F > 0 )
assume A3: for k being Element of NAT st k in dom F holds
F . k > 0 ; :: thesis: ( not len F = n + 1 or Product F > 0 )
assume A4: len F = n + 1 ; :: thesis: Product F > 0
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 by FINSEQ_1:3;
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
F1 . k > 0

proof

let k be Element of NAT ; :: thesis: ( k in dom F1 implies F1 . k > 0 )
assume A9: k in dom F1 ; :: thesis: F1 . k > 0
then F . k > 0 by A3, A7, FINSEQ_2:15;
hence F1 . k > 0 by A7, A9, FINSEQ_1:def 7; :: thesis: verum

end;

then A10: Product F1 > 0 by A2, A5;
set x = F2 . 1;
Seg (n + 1) = dom F by A4, FINSEQ_1:def 3;
then A11: F2 . 1 > 0 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 Product F > 0 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
F . k > 0 ) & len F = 0 implies Product F > 0 )
assume for k being Element of NAT st k in dom F holds
F . k > 0 ; :: thesis: ( not len F = 0 or Product F > 0 )
assume len F = 0 ; :: thesis: Product F > 0
then F = <*> REAL ;
hence Product F > 0 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
F . k > 0 ; :: thesis: Product F > 0
hence Product F > 0 by A13, A14; :: thesis: verum