let F be complex-yielding FinSequence; :: thesis: ( ex k being Nat st
( k in dom F & F . k = 0 ) iff Product F = 0 )
defpred S₁[ Nat] means for F being complex-yielding FinSequence st len F = $1 holds
( ex k being Nat st
( k in Seg $1 & F . k = 0 ) iff Product F = 0 );
A1: S₁[ 0 ] by Th124, FINSEQ_1:32;
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-yielding 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-yielding 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 F' being complex-yielding FinSequence, x being complex number such that
A5: F = F' ^ <*x*> by Lm6;
A6: len F = (len F') + 1 by A5, FINSEQ_2:19;
A7: Product F = (Product F') * x by A5, Th126;
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

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

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

Seg (len F') = dom F' by FINSEQ_1:def 3;
then F' . k = F . k by A4, A5, A6, A10, FINSEQ_1:def 7;
then Product F' = 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:59;
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 F' = 0 or x = 0 ) by A7, A11;

suppose Product F' = 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 & F' . k = 0 ) by A3, A4, A6;
Seg (len F') = dom F' by FINSEQ_1:def 3;
then ( k in Seg (i + 1) & F . k = 0 ) by A4, A5, A6, A12, FINSEQ_1:def 7, FINSEQ_2:9;
hence ex k being Nat st
( k in Seg (i + 1) & F . k = 0 ) ; :: thesis: verum

end;

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

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

end;

end;

end;

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