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

proof

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

end;

A4: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: for p being FinSequence of the carrier of K st len p = i holds
( ex k being Element of 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 Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K ) )
assume A6: len p = i + 1 ; :: thesis: ( ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) iff Product p = 0. K )
then consider p' being FinSequence of the carrier of K, a being Element of K such that
A7: p = p' ^ <*a*> by FINSEQ_2:22;
A8: i + 1 = (len p') + 1 by A6, A7, FINSEQ_2:19;
then A9: i = len p' by XCMPLX_1:2;
A10: Product p = (Product p') * a by A7, GROUP_4:9;
thus ( ex k being Element of 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 Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) )

proof

given k being Element of NAT such that A11: k in Seg (i + 1) and
A12: p . k = 0. K ; :: thesis: Product p = 0. K

now

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

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

then k in dom p' by A9, FINSEQ_1:def 3;
then p' . k = p . k by A7, FINSEQ_1:def 7;
then Product p' = 0. K by A5, A9, A12, A13;
hence Product p = 0. K by A10, VECTSP_1:39; :: thesis: verum

end;

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

then a = 0. K by A7, A8, A12, FINSEQ_1:59;
hence Product p = 0. K by A10, VECTSP_1:39; :: thesis: verum

end;

end;

end;

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

end;

assume A14: Product p = 0. K ; :: thesis: ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K )

per cases ( Product p' = 0. K or a = 0. K ) by A10, A14, VECTSP_1:44;

suppose Product p' = 0. K ; :: thesis: ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K )

then consider k being Element of NAT such that
A15: ( k in Seg i & p' . k = 0. K ) by A5, A9;
k in dom p' by A9, A15, FINSEQ_1:def 3;
then ( k in Seg (i + 1) & p . k = 0. K ) by A7, A15, FINSEQ_1:def 7, FINSEQ_2:9;
hence ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) ; :: thesis: verum

end;

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

then ( i + 1 in Seg (i + 1) & p . (i + 1) = 0. K ) by A7, A8, FINSEQ_1:6, FINSEQ_1:59;
hence ex k being Element of NAT st
( k in Seg (i + 1) & p . k = 0. K ) ; :: thesis: verum

end;

end;

end;

A16: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A1, A4);
Seg (len p) = dom p by FINSEQ_1:def 3;
hence ( ex k being Element of NAT st
( k in dom p & p . k = 0. K ) iff Product p = 0. K ) by A16; :: thesis: verum