let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; 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; ( 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
; Product p = 0. L
defpred S1[ 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 S1[j] holds
S1[j + 1]
proof
let j be
Nat;
( S1[j] implies S1[j + 1] )
assume A4:
S1[
j]
;
S1[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;
( 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 )
;
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
j <> 0
;
Product p = 0. Lthen 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 A19:
p /. (len p) <> 0. L
;
Product p = 0. Lconsider 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 15;
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
;
verum end; end;
end;
hence
S1[
j + 1]
;
verum
end;
A27:
ex l being Element of NAT st l = len p
;
A28:
S1[ 0 ]
for j being Nat holds S1[j]
from NAT_1:sch 2(A28, A3);
hence
Product p = 0. L
by A1, A2, A27; verum