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 )
assume A1:
for k being Element of NAT st k in dom F holds
F . k > 0
; :: thesis: Product F > 0
defpred S1[ Element of 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 ;
A2:
S1[ 0 ]
by FINSEQ_1:32, RVSUM_1:124;
A3:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
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
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 A5:
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 A6:
len F = n + 1
;
:: thesis: Product F > 0
then consider F1,
F2 being
FinSequence of
REAL such that A7:
len F1 = n
and A8:
len F2 = 1
and A9:
F = F1 ^ F2
by FINSEQ_2:26;
set x =
F2 . 1;
for
k being
Element of
NAT st
k in dom F1 holds
F1 . k > 0
then A11:
Product F1 > 0
by A4, A7;
1
in Seg 1
by FINSEQ_1:5;
then
1
in dom F2
by A8, FINSEQ_1:def 3;
then A12:
F . (n + 1) = F2 . 1
by A7, A9, FINSEQ_1:def 7;
Seg (n + 1) = dom F
by A6, FINSEQ_1:def 3;
then A13:
F2 . 1
> 0
by A5, A12, FINSEQ_1:5;
Product F =
Product (F1 ^ <*(F2 . 1)*>)
by A8, A9, FINSEQ_1:57
.=
(Product F1) * (F2 . 1)
by RVSUM_1:126
;
hence
Product F > 0
by A11, A13;
:: thesis: verum
end;
hence
S1[
n + 1]
;
:: thesis: verum
end;
A14:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A2, A3);
ex n being Element of NAT st n = len F
;
hence
Product F > 0
by A1, A14; :: thesis: verum