defpred S_{1}[ 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_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[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

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

S

proof

A12:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
; :: thesis: verum

end;assume A2: S

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

hence
S
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

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;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

then A10:
0 <= Product F1
by A2, A5;
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;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

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

proof

A13:
for n being Nat holds S
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;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

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