defpred S_{1}[ Nat] means for f being CR_Sequence st len f = $1 holds

Product f > 0 ;

let m be CR_Sequence; :: thesis: Product m > 0

A1: ex j being Nat st len m = j ;

A2: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A8, A2);

hence Product m > 0 by A1; :: thesis: verum

Product f > 0 ;

let m be CR_Sequence; :: thesis: Product m > 0

A1: ex j being Nat st len m = j ;

A2: for k being Nat st S

S

proof

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

assume A3: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A3: S

now :: thesis: for f being CR_Sequence st len f = k + 1 holds

Product f > 0

hence
SProduct f > 0

let f be CR_Sequence; :: thesis: ( len f = k + 1 implies Product b_{1} > 0 )

assume A4: len f = k + 1 ; :: thesis: Product b_{1} > 0

set f1 = f | k;

end;assume A4: len f = k + 1 ; :: thesis: Product b

set f1 = f | k;

per cases
( k > 0 or k = 0 )
;

end;

suppose
k > 0
; :: thesis: Product b_{1} > 0

then reconsider f1 = f | k as CR_Sequence by A4, Th24, NAT_1:11;

A5: f = f1 ^ <*(f . (k + 1))*> by A4, FINSEQ_3:55;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (k + 1) ;

then k + 1 in dom f by A4, FINSEQ_1:def 3;

then f . (k + 1) in rng f by FUNCT_1:3;

then A6: f . (k + 1) > 0 by PARTFUN3:def 1;

len f1 = k by A4, FINSEQ_1:59, NAT_1:11;

then Product f1 > 0 by A3;

then 0 * (f . (k + 1)) < (Product f1) * (f . (k + 1)) by A6, XREAL_1:68;

hence Product f > 0 by A5, RVSUM_1:96; :: thesis: verum

end;A5: f = f1 ^ <*(f . (k + 1))*> by A4, FINSEQ_3:55;

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (k + 1) ;

then k + 1 in dom f by A4, FINSEQ_1:def 3;

then f . (k + 1) in rng f by FUNCT_1:3;

then A6: f . (k + 1) > 0 by PARTFUN3:def 1;

len f1 = k by A4, FINSEQ_1:59, NAT_1:11;

then Product f1 > 0 by A3;

then 0 * (f . (k + 1)) < (Product f1) * (f . (k + 1)) by A6, XREAL_1:68;

hence Product f > 0 by A5, RVSUM_1:96; :: thesis: verum

for k being Nat holds S

hence Product m > 0 by A1; :: thesis: verum