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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[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 b₁ = 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 b₁ = 0 )
then A4: len (f | k) = k by FINSEQ_1:59, NAT_1:11;
reconsider f1 = f | k as complex-valued FinSequence ;
f = f1 ^ <*(f . (k + 1))*> by A3, FINSEQ_3:55;
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: Product b₁ = 0

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 A5; :: thesis: verum

end;

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

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 A8, FINSEQ_1:def 3;
then j <= k + 1 by A3, FINSEQ_1:1;
then j < k + 1 by A7, A9, XXREAL_0:1;
then A11: j <= k by NAT_1:13;
1 <= j by A10, FINSEQ_1:1;
then j in Seg k by A11;
then A12: j in dom f1 by A4, FINSEQ_1:def 3;
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 S₁[k + 1] ; :: thesis: verum

end;

A13: S₁[ 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 S₁[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: Product m = 0
hence Product m = 0 by A14, A15; :: thesis: verum