let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being FinSequence of the carrier of L st ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) holds
Product p = 0. L
let p be FinSequence of the carrier of L; :: thesis: ( ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) implies Product p = 0. L )
given i being Element of NAT such that A1: i in dom p and
A2: p /. i = 0. L ; :: thesis: Product p = 0. L
defpred S₁[ Nat] means for p being FinSequence of the carrier of L st len p = $1 & ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) holds
Product p = 0. L;
A3: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A4: S₁[j] ; :: thesis: S₁[j + 1]
for p being FinSequence of the carrier of L st len p = j + 1 & ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) holds
Product p = 0. L

proof

let p be FinSequence of the carrier of L; :: thesis: ( len p = j + 1 & ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) implies Product p = 0. L )
assume that
A5: len p = j + 1 and
A6: ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) ; :: thesis: Product p = 0. L
A7: ex fp being sequence of the carrier of L st
( fp . 1 = p . 1 & ( for i being Nat st 0 <> i & i < len p holds
fp . (i + 1) = the multF of L . ((fp . i),(p . (i + 1))) ) & the multF of L "**" p = fp . (len p) ) by A5, FINSOP_1:1, NAT_1:14;
A8: len p >= 1 by A5, NAT_1:14;
then A9: 1 in dom p by FINSEQ_3:25;
A10: dom p = Seg (len p) by FINSEQ_1:def 3;
then A11: j + 1 in dom p by A5, A8, FINSEQ_1:1;

per cases ( j = 0 or j <> 0 ) ;

suppose A12: j = 0 ; :: thesis: Product p = 0. L

then A13: dom p = {1} by A5, FINSEQ_1:2, FINSEQ_1:def 3;
Product p = p . 1 by A5, A7, A12, GROUP_4:def 2
.= p /. 1 by A9, PARTFUN1:def 6 ;
hence Product p = 0. L by A6, A13, TARSKI:def 1; :: thesis: verum

end;

suppose j <> 0 ; :: thesis: Product p = 0. L

then A14: 1 <= j by NAT_1:14;
reconsider p9 = p | (Seg j) as FinSequence of the carrier of L by FINSEQ_1:18;
A15: j <= j + 1 by XREAL_1:29;
then A16: dom p9 = Seg j by A5, FINSEQ_1:17;
p = p9 ^ <*(p . (len p))*> by A5, FINSEQ_3:55;
then A17: p = p9 ^ <*(p /. (len p))*> by A5, A11, PARTFUN1:def 6;
A18: len p9 = j by A5, A15, FINSEQ_1:17;

per cases ( p /. (len p) = 0. L or p /. (len p) <> 0. L ) ;

suppose p /. (len p) = 0. L ; :: thesis: Product p = 0. L

hence Product p = (Product p9) * (0. L) by A17, GROUP_4:6
.= 0. L ;
:: thesis: verum

end;

suppose A19: p /. (len p) <> 0. L ; :: thesis: Product p = 0. L

consider i being Element of NAT such that
A20: i in dom p and
A21: p /. i = 0. L by A6;
i <= len p by A10, A20, FINSEQ_1:1;
then i < len p by A19, A21, XXREAL_0:1;
then A22: i <= j by A5, NAT_1:13;
A23: 1 <= i by A10, A20, FINSEQ_1:1;
then A24: i in dom p9 by A16, A22, FINSEQ_1:1;
A25: j in dom p by A5, A10, A14, A15, FINSEQ_1:1;
i in Seg j by A23, A22, FINSEQ_1:1;
then (p | j) . i = p . i by A25, RFINSEQ:6;
then p9 . i = p . i by FINSEQ_1:def 16;
then p9 /. i = p . i by A24, PARTFUN1:def 6;
then A26: p9 /. i = 0. L by A20, A21, PARTFUN1:def 6;
thus Product p = (Product p9) * (p /. (len p)) by A17, GROUP_4:6
.= (0. L) * (p /. (len p)) by A4, A18, A24, A26
.= 0. L ; :: thesis: verum

end;

end;

end;

end;

end;

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

end;

A27: ex l being Element of NAT st l = len p ;
A28: S₁[ 0 ]

proof

let p be FinSequence of L; :: thesis: ( len p = 0 & ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) implies Product p = 0. L )
assume len p = 0 ; :: thesis: ( for i being Element of NAT holds
( not i in dom p or not p /. i = 0. L ) or Product p = 0. L )
then p = {} ;
hence ( for i being Element of NAT holds
( not i in dom p or not p /. i = 0. L ) or Product p = 0. L ) ; :: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A28, A3);
hence Product p = 0. L by A1, A2, A27; :: thesis: verum