defpred S1[ Nat] means for f being complex-valued FinSequence st len f = \$1 & ex i being Nat st
( i in dom f & f . i = 0 ) holds
Product f = 0 ;
let m be complex-valued FinSequence; :: thesis: ( ex i being Nat st
( i in dom m & m . i = 0 ) implies Product m = 0 )

A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: for f being complex-valued FinSequence st len f = k + 1 & ex i being Nat st
( i in dom f & f . i = 0 ) holds
Product f = 0
let f be complex-valued FinSequence; :: thesis: ( len f = k + 1 & ex i being Nat st
( i in dom f & f . i = 0 ) implies Product b1 = 0 )

set f1 = f | k;
assume A3: len f = k + 1 ; :: thesis: ( ex i being Nat st
( i in dom f & f . i = 0 ) implies Product b1 = 0 )

then A4: len (f | k) = k by ;
reconsider f1 = f | k as complex-valued FinSequence ;
f = f1 ^ <*(f . (k + 1))*> by ;
then A5: Product f = (Product f1) * (f . (k + 1)) by RVSUM_1:96;
assume A6: ex i being Nat st
( i in dom f & f . i = 0 ) ; :: thesis:
per cases ( f . (k + 1) = 0 or f . (k + 1) <> 0 ) ;
suppose f . (k + 1) = 0 ; :: thesis:
hence Product f = 0 by A5; :: thesis: verum
end;
suppose A7: f . (k + 1) <> 0 ; :: thesis:
consider j being Nat such that
A8: j in dom f and
A9: f . j = 0 by A6;
reconsider j = j as Element of NAT by ORDINAL1:def 12;
A10: j in Seg (len f) by ;
then j <= k + 1 by ;
then j < k + 1 by ;
then A11: j <= k by NAT_1:13;
1 <= j by ;
then j in Seg k by A11;
then A12: j in dom f1 by ;
then f1 . j = f . j by FUNCT_1:47;
then Product f1 = 0 by A2, A4, A9, A12;
hence Product f = 0 by A5; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A13: S1[ 0 ]
proof
let f be complex-valued FinSequence; :: thesis: ( len f = 0 & ex i being Nat st
( i in dom f & f . i = 0 ) implies Product f = 0 )

assume len f = 0 ; :: thesis: ( for i being Nat holds
( not i in dom f or not f . i = 0 ) or Product f = 0 )

then Seg (len f) = {} ;
hence ( for i being Nat holds
( not i in dom f or not f . i = 0 ) or Product f = 0 ) by FINSEQ_1:def 3; :: thesis: verum
end;
A14: for k being Nat holds S1[k] from NAT_1:sch 2(A13, A1);
A15: ex j being Nat st len m = j ;
assume ex i being Nat st
( i in dom m & m . i = 0 ) ; :: thesis:
hence Product m = 0 by ; :: thesis: verum