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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

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

let f be CR_Sequence; :: thesis: ( len f = k + 1 implies Product b₁ > 0 )
assume A4: len f = k + 1 ; :: thesis: Product b₁ > 0
set f1 = f | k;

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

suppose k > 0 ; :: thesis: Product b₁ > 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;

suppose k = 0 ; :: thesis: Product b₁ > 0

then A7: f = <*(f . 1)*> by A4, FINSEQ_1:40;
then dom f = Seg 1 by FINSEQ_1:38;
then 1 in dom f ;
then f . 1 in rng f by FUNCT_1:3;
then f . 1 > 0 by PARTFUN3:def 1;
hence Product f > 0 by A7; :: thesis: verum

end;

end;

end;

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

end;

A8: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A2);
hence Product m > 0 by A1; :: thesis: verum