let m be complex-valued FinSequence; :: thesis: ( ex i being natural number st
( i in dom m & m . i = 0 ) implies Product m = 0 )
assume AS: ex i being natural number st
( i in dom m & m . i = 0 ) ; :: thesis: Product m = 0
defpred S₁[ Nat] means for f being complex-valued FinSequence st len f = $1 & ex i being natural number st
( i in dom f & f . i = 0 ) holds
Product f = 0 ;
A: S₁[ 0 ] by FINSEQ_1:4, FINSEQ_1:def 3;
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 complex-valued FinSequence; :: thesis: ( len f = k + 1 & ex i being natural number st
( i in dom f & f . i = 0 ) implies Product b₁ = 0 )
assume B: len f = k + 1 ; :: thesis: ( ex i being natural number st
( i in dom f & f . i = 0 ) implies Product b₁ = 0 )
assume C: ex i being natural number st
( i in dom f & f . i = 0 ) ; :: thesis: Product b₁ = 0
set f1 = f | k;
Y: len (f | k) = k by B, FINSEQ_1:80, NAT_1:11;
reconsider f1 = f | k as complex-valued FinSequence ;
f = f1 ^ <*(f . (k + 1))*> by B, FINSEQ_3:61;
then G: Product f = (Product f1) * (f . (k + 1)) by RVSUM_1:126;

per cases ( f . (k + 1) = 0 or f . (k + 1) <> 0 ) ;

suppose f . (k + 1) = 0 ; :: thesis: Product b₁ = 0

hence Product f = 0 by G; :: thesis: verum

end;

suppose H1: f . (k + 1) <> 0 ; :: thesis: Product b₁ = 0

consider j being natural number such that
GG: ( j in dom f & f . j = 0 ) by C;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
j in Seg (len f) by GG, FINSEQ_1:def 3;
then H4: ( 1 <= j & j <= k + 1 ) by B, FINSEQ_1:3;
then j < k + 1 by GG, H1, XXREAL_0:1;
then j <= k by NAT_1:13;
then j in Seg k by H4;
then H2: j in dom f1 by Y, FINSEQ_1:def 3;
then f1 . j = f . j by FUNCT_1:70;
then Product f1 = 0 by AS, Y, GG, H2;
hence Product f = 0 by G; :: 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 AS, I, H; :: thesis: verum