defpred S₁[ Nat] means for F being complex-valued FinSequence st len F = $1 holds
( ex k being Nat st
( k in Seg $1 & F . k = 0 ) iff Product F = 0 );
let F be complex-valued FinSequence; :: thesis: ( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )
A1: Seg (len F) = dom F by FINSEQ_1:def 3;
A2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A3: for F being complex-valued FinSequence st len F = i holds
( ex k being Nat st
( k in Seg i & F . k = 0 ) iff Product F = 0 ) ; :: thesis: S₁[i + 1]
let F be complex-valued FinSequence; :: thesis: ( len F = i + 1 implies ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 ) )
assume A4: len F = i + 1 ; :: thesis: ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) iff Product F = 0 )
then consider F9 being complex-valued FinSequence, x being Complex such that
A5: F = F9 ^ <*x*> by Lm4;
A6: len F = (len F9) + 1 by A5, FINSEQ_2:16;
A7: Product F = (Product F9) * x by A5, Th96;
thus ( ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) implies Product F = 0 ) :: thesis: ( Product F = 0 implies ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) )

proof

given k being Nat such that A8: k in Seg (i + 1) and
A9: F . k = 0 ; :: thesis: Product F = 0

now :: thesis: Product F = 0

per cases ( k in Seg i or k = i + 1 ) by A8, FINSEQ_2:7;

suppose A10: k in Seg i ; :: thesis: Product F = 0

Seg (len F9) = dom F9 by FINSEQ_1:def 3;
then F9 . k = F . k by A4, A5, A6, A10, FINSEQ_1:def 7;
then Product F9 = 0 by A3, A4, A6, A9, A10;
hence Product F = 0 by A7; :: thesis: verum

end;

suppose k = i + 1 ; :: thesis: Product F = 0

then x = 0 by A4, A5, A6, A9, FINSEQ_1:42;
hence Product F = 0 by A7; :: thesis: verum

end;

end;

end;

hence Product F = 0 ; :: thesis: verum

end;

assume A11: Product F = 0 ; :: thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )

per cases ( Product F9 = 0 or x = 0 ) by A7, A11;

suppose Product F9 = 0 ; :: thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )

then consider k being Nat such that
A12: k in Seg i and
A13: F9 . k = 0 by A3, A4, A6;
Seg (len F9) = dom F9 by FINSEQ_1:def 3;
then F . k = 0 by A4, A5, A6, A12, A13, FINSEQ_1:def 7;
hence ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) by A12, FINSEQ_2:8; :: thesis: verum

end;

suppose x = 0 ; :: thesis: ex k being Nat st
( k in Seg (i + 1) & F . k = 0 )

then F . (i + 1) = 0 by A4, A5, A6, FINSEQ_1:42;
hence ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) by FINSEQ_1:4; :: thesis: verum

end;

end;

end;

A14: S₁[ 0 ]

proof

let F be complex-valued FinSequence; :: thesis: ( len F = 0 implies ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) )
assume len F = 0 ; :: thesis: ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 )
then F = <*> COMPLEX ;
hence ( ex k being Nat st
( k in Seg 0 & F . k = 0 ) iff Product F = 0 ) by Th94; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A14, A2);
hence ( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 ) by A1; :: thesis: verum