let K be non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being FinSequence of the carrier of K holds
( ex k being Nat st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
let p be FinSequence of the carrier of K; :: thesis: ( ex k being Nat st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )
defpred S₁[ Nat] means for p being FinSequence of the carrier of K st len p = $1 holds
( ex k being Nat st
( k in Seg $1 & p . k = 0. K ) iff Product p = 0. K );
A1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A2: for p being FinSequence of the carrier of K st len p = i holds
( ex k being Nat st
( k in Seg i & p . k = 0. K ) iff Product p = 0. K ) ; :: thesis: S₁[i + 1]
let p be FinSequence of the carrier of K; :: thesis: ( len p = i + 1 implies ( ex k being Nat st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K ) )
assume A3: len p = i + 1 ; :: thesis: ( ex k being Nat st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K )
then consider p9 being FinSequence of the carrier of K, a being Element of K such that
A4: p = p9 ^ <*a*> by FINSEQ_2:19;
A5: i + 1 = (len p9) + 1 by A3, A4, FINSEQ_2:16;
then A6: i = len p9 by XCMPLX_1:2;
A7: Product p = (Product p9) * a by A4, GROUP_4:6;
thus ( ex k being Nat st
( k in Seg (i + 1) & p . k = 0. K ) implies Product p = 0. K ) :: thesis: ( Product p = 0. K implies ex k being Nat st
( k in Seg (i + 1) & p . k = 0. K ) )

proof

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

now :: thesis: Product p = 0. K

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

suppose A10: k in Seg i ; :: thesis: Product p = 0. K

then k in dom p9 by A6, FINSEQ_1:def 3;
then p9 . k = p . k by A4, FINSEQ_1:def 7;
then Product p9 = 0. K by A2, A6, A9, A10;
hence Product p = 0. K by A7; :: thesis: verum

end;

suppose k = i + 1 ; :: thesis: Product p = 0. K

then a = 0. K by A4, A5, A9, FINSEQ_1:42;
hence Product p = 0. K by A7; :: thesis: verum

end;

end;

end;

hence Product p = 0. K ; :: thesis: verum

end;

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

per cases ( Product p9 = 0. K or a = 0. K ) by A7, A11, VECTSP_1:12;

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

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

end;

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

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

end;

end;

end;

A14: Seg (len p) = dom p by FINSEQ_1:def 3;
A15: S₁[ 0 ]

proof

let p be FinSequence of the carrier of K; :: thesis: ( len p = 0 implies ( ex k being Nat st
( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K ) )
assume len p = 0 ; :: thesis: ( ex k being Nat st
( k in Seg 0 & p . k = 0. K ) iff Product p = 0. K )
then p = <*> the carrier of K ;
then A16: Product p = 1. K by Lm6;
thus ( ex k being Nat st
( k in Seg 0 & p . k = 0. K ) implies Product p = 0. K ) ; :: thesis: ( Product p = 0. K implies ex k being Nat st
( k in Seg 0 & p . k = 0. K ) )
assume Product p = 0. K ; :: thesis: ex k being Nat st
( k in Seg 0 & p . k = 0. K )
hence ex k being Nat st
( k in Seg 0 & p . k = 0. K ) by A16; :: thesis: verum

end;

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