let L be non empty associative commutative doubleLoopStr ; for a being Element of L
for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Product q = a * (Product p)
let a be Element of L; for p, q being FinSequence of the carrier of L st len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) holds
Product q = a * (Product p)
let p, q be FinSequence of the carrier of L; ( len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) ) implies Product q = a * (Product p) )
assume that
A1:
len p = len q
and
A2:
ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9 ) )
; Product q = a * (Product p)
consider i being Element of NAT such that
A3:
i in dom p
and
A4:
q /. i = a * (p /. i)
and
A5:
for i9 being Element of NAT st i9 in dom p & i9 <> i holds
q /. i9 = p /. i9
by A2;
A6:
Product p = the multF of L "**" p
by GROUP_4:def 2;
A7:
Product q = the multF of L "**" q
by GROUP_4:def 2;
per cases
( len p = 0 or len p <> 0 )
;
suppose A8:
len p <> 0
;
Product q = a * (Product p)then A9:
len p >= 1
by NAT_1:14;
consider l9 being
Nat such that A10:
dom q = Seg l9
by FINSEQ_1:def 2;
consider fp being
sequence of the
carrier of
L such that A11:
fp . 1
= p . 1
and A12:
for
i being
Nat st
0 <> i &
i < len p holds
fp . (i + 1) = the
multF of
L . (
(fp . i),
(p . (i + 1)))
and A13:
Product p = fp . (len p)
by A6, A8, FINSOP_1:1, NAT_1:14;
consider fq being
sequence of the
carrier of
L such that A14:
fq . 1
= q . 1
and A15:
for
i being
Nat st
0 <> i &
i < len q holds
fq . (i + 1) = the
multF of
L . (
(fq . i),
(q . (i + 1)))
and A16:
Product q = fq . (len p)
by A1, A7, A8, FINSOP_1:1, NAT_1:14;
defpred S1[
Element of
NAT ]
means ( ( $1
< i &
fp . $1
= fq . $1 ) or (
i <= $1 &
fq . $1
= a * (fp . $1) ) );
consider l being
Nat such that A17:
dom p = Seg l
by FINSEQ_1:def 2;
i in { z where z is Nat : ( 1 <= z & z <= l ) }
by A3, A17, FINSEQ_1:def 1;
then A18:
ex
i9 being
Nat st
(
i9 = i & 1
<= i9 &
i9 <= l )
;
reconsider l =
l,
l9 =
l9 as
Element of
NAT by ORDINAL1:def 12;
A19:
len p = l
by A17, FINSEQ_1:def 3;
A20:
1
<= l
by A18, XXREAL_0:2;
then A21:
1
in dom p
by A17, FINSEQ_1:1;
A22:
l =
len p
by A17, FINSEQ_1:def 3
.=
l9
by A1, A10, FINSEQ_1:def 3
;
A23:
for
j being
Element of
NAT st 1
<= j &
j < len p &
S1[
j] holds
S1[
j + 1]
proof
let j be
Element of
NAT ;
( 1 <= j & j < len p & S1[j] implies S1[j + 1] )
assume that A24:
1
<= j
and A25:
j < len p
;
( not S1[j] or S1[j + 1] )
assume A26:
S1[
j]
;
S1[j + 1]
per cases
( j < i or i <= j )
;
suppose A27:
j < i
;
S1[j + 1]per cases
( j + 1 = i or j + 1 <> i )
;
suppose A28:
j + 1
= i
;
S1[j + 1]then A29:
p . (j + 1) = p /. (j + 1)
by A3, PARTFUN1:def 6;
q . (j + 1) = q /. (j + 1)
by A3, A17, A10, A22, A28, PARTFUN1:def 6;
then fq . (j + 1) =
(fp . j) * (a * (p /. (j + 1)))
by A1, A4, A15, A24, A25, A26, A27, A28
.=
((fp . j) * (p /. (j + 1))) * a
by GROUP_1:def 3
.=
(fp . (j + 1)) * a
by A12, A24, A25, A29
;
hence
S1[
j + 1]
by A28;
verum end; suppose A30:
j + 1
<> i
;
S1[j + 1]A31:
j + 1
< i
j + 1
<= i
by A27, NAT_1:13;
then A32:
j + 1
<= l
by A18, XXREAL_0:2;
0 + 1
<= j + 1
by XREAL_1:6;
then A33:
j + 1
in Seg l
by A32, FINSEQ_1:1;
then A34:
p . (j + 1) = p /. (j + 1)
by A17, PARTFUN1:def 6;
q . (j + 1) = q /. (j + 1)
by A10, A22, A33, PARTFUN1:def 6;
then fq . (j + 1) =
(fq . j) * (q /. (j + 1))
by A1, A15, A24, A25
.=
the
multF of
L . (
(fq . j),
(p . (j + 1)))
by A5, A17, A30, A33, A34
.=
fp . (j + 1)
by A12, A24, A25, A26, A27
;
hence
S1[
j + 1]
by A31;
verum end; end; end; suppose A35:
i <= j
;
S1[j + 1]
j < l
by A17, A25, FINSEQ_1:def 3;
then A36:
j + 1
<= l
by NAT_1:13;
0 + 1
<= j + 1
by XREAL_1:6;
then A37:
j + 1
in dom p
by A17, A36, FINSEQ_1:1;
then A38:
p . (j + 1) = p /. (j + 1)
by PARTFUN1:def 6;
A39:
i < j + 1
by A35, NAT_1:13;
q . (j + 1) = q /. (j + 1)
by A17, A10, A22, A37, PARTFUN1:def 6;
then fq . (j + 1) =
(fq . j) * (q /. (j + 1))
by A1, A15, A24, A25
.=
(a * (fp . j)) * (p /. (j + 1))
by A5, A26, A35, A39, A37
.=
a * ((fp . j) * (p /. (j + 1)))
by GROUP_1:def 3
.=
a * (fp . (j + 1))
by A12, A24, A25, A38
;
hence
S1[
j + 1]
by A35, NAT_1:13;
verum end; end;
end; A40:
1
in dom q
by A10, A22, A20, FINSEQ_1:1;
now ( ( 1 < i & fp . 1 = fq . 1 ) or ( i <= 1 & fq . 1 = a * (fp . 1) ) )end; then A42:
S1[1]
;
for
j being
Element of
NAT st 1
<= j &
j <= len p holds
S1[
j]
from INT_1:sch 7(A42, A23);
hence
Product q = a * (Product p)
by A9, A13, A16, A18, A19;
verum end; end;