let m be CR_Sequence; :: thesis: Product m > 0
defpred S₁[ Nat] means for f being CR_Sequence st len f = $1 holds
Product f > 0 ;
A: S₁[ 0 ] by FINSEQ_1:32, RVSUM_1:124;
B: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume AS: S₁[k] ; :: thesis: S₁[k + 1]

now

let f be CR_Sequence; :: thesis: ( len f = k + 1 implies Product b₁ > 0 )
assume B: 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 B, CRsub, NAT_1:11;
len f1 = k by B, FINSEQ_1:80, NAT_1:11;
then D: Product f1 > 0 by AS;
F: f = f1 ^ <*(f . (k + 1))*> by B, FINSEQ_3:61;
( 1 <= k + 1 & k + 1 <= k + 1 ) by NAT_1:11;
then k + 1 in Seg (k + 1) ;
then H: k + 1 in dom f by B, FINSEQ_1:def 3;
f . (k + 1) in rng f by H, FUNCT_1:12;
then f . (k + 1) > 0 by PARTFUN3:def 1;
then 0 * (f . (k + 1)) < (Product f1) * (f . (k + 1)) by D, XREAL_1:70;
hence Product f > 0 by F, RVSUM_1:126; :: thesis: verum

end;

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

then C1: f = <*(f . 1)*> by B, FINSEQ_1:57;
then dom f = Seg 1 by FINSEQ_1:55;
then 1 in dom f ;
then f . 1 in rng f by FUNCT_1:12;
then f . 1 > 0 by PARTFUN3:def 1;
hence Product f > 0 by C1, RVSUM_1:125; :: thesis: verum

end;

end;

end;

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

end;

I: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A, B);
consider j being Nat such that
H: len m = j ;
thus Product m > 0 by I, H; :: thesis: verum