let R be non degenerated right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for F being FinSequence of R holds
( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) )
let F be FinSequence of R; :: thesis: ( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) )

now :: thesis: ( Product F = 0. R implies ex i being Nat st
( i in dom F & F . i = 0. R ) )

assume AS: Product F = 0. R ; :: thesis: ex i being Nat st
( i in dom F & F . i = 0. R )
defpred S₁[ Nat] means for f being FinSequence of R st len f = $1 & Product f = 0. R holds
ex i being Nat st
( i in dom f & f . i = 0. R );
A0: S₁[ 0 ]

proof

let F be FinSequence of R; :: thesis: ( len F = 0 & Product F = 0. R implies ex i being Nat st
( i in dom F & F . i = 0. R ) )
assume len F = 0 ; :: thesis: ( not Product F = 0. R or ex i being Nat st
( i in dom F & F . i = 0. R ) )
then F = <*> the carrier of R ;
then Product F = 1_ R by GROUP_4:8
.= 1. R ;
hence ( not Product F = 0. R or ex i being Nat st
( i in dom F & F . i = 0. R ) ) ; :: thesis: verum

end;

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 IV: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being FinSequence of R st len F = k + 1 & Product F = 0. R holds
ex i being Nat st
( i in dom F & F . i = 0. R )

let F be FinSequence of R; :: thesis: ( len F = k + 1 & Product F = 0. R implies ex i being Nat st
( b₂ in dom i & i . b₂ = 0. R ) )
assume A3: len F = k + 1 ; :: thesis: ( Product F = 0. R implies ex i being Nat st
( b₂ in dom i & i . b₂ = 0. R ) )
then F <> {} ;
then consider q being FinSequence, x being object such that
B2: F = q ^ <*x*> by FINSEQ_1:46;
B2a: rng q c= rng F by B2, FINSEQ_1:29;
rng F c= the carrier of R ;
then rng q c= the carrier of R by B2a;
then reconsider q = q as FinSequence of R by FINSEQ_1:def 4;
rng <*x*> = {x} by FINSEQ_1:39;
then B5: x in rng <*x*> by TARSKI:def 1;
rng <*x*> c= rng F by B2, FINSEQ_1:30;
then x in rng F by B5;
then reconsider x = x as Element of R ;
A4: len F = (len q) + (len <*x*>) by B2, FINSEQ_1:22
.= (len q) + 1 by FINSEQ_1:39 ;
A5: Product F = (Product q) * x by GROUP_4:6, B2;
assume A6: Product F = 0. R ; :: thesis: ex i being Nat st
( b₂ in dom i & i . b₂ = 0. R )

per cases ( Product q = 0. R or x = 0. R ) by A6, A5, VECTSP_2:def 1;

suppose Product q = 0. R ; :: thesis: ex i being Nat st
( b₂ in dom i & i . b₂ = 0. R )

then consider j being Nat such that
C1: ( j in dom q & q . j = 0. R ) by A3, A4, IV;
C2: F . j = q . j by B2, C1, FINSEQ_1:def 7;
dom q c= dom F by B2, FINSEQ_1:26;
hence ex i being Nat st
( i in dom F & F . i = 0. R ) by C1, C2; :: thesis: verum

end;

suppose C0: x = 0. R ; :: thesis: ex i being Nat st
( b₂ in dom i & i . b₂ = 0. R )

dom <*x*> = {1} by FINSEQ_1:2, FINSEQ_1:def 8;
then 1 in dom <*x*> by TARSKI:def 1;
then C1: F . (k + 1) = <*x*> . 1 by B2, A4, A3, FINSEQ_1:def 7
.= x ;
dom F = Seg (k + 1) by A3, FINSEQ_1:def 3;
hence ex i being Nat st
( i in dom F & F . i = 0. R ) by C1, C0, FINSEQ_1:4; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

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

end;

hence ( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) ) by prod4; :: thesis: verum