let L be non empty associative commutative doubleLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: 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 len p = 0 ; :: thesis: Product q = a * (Product p)

then p = {} ;
hence Product q = a * (Product p) by A3; :: thesis: verum

end;

suppose A8: len p <> 0 ; :: thesis: 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 S₁[ 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 & S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < len p & S₁[j] implies S₁[j + 1] )
assume that
A24: 1 <= j and
A25: j < len p ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A26: S₁[j] ; :: thesis: S₁[j + 1]

per cases ( j < i or i <= j ) ;

suppose A27: j < i ; :: thesis: S₁[j + 1]

per cases ( j + 1 = i or j + 1 <> i ) ;

suppose A28: j + 1 = i ; :: thesis: S₁[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 S₁[j + 1] by A28; :: thesis: verum

end;

suppose A30: j + 1 <> i ; :: thesis: S₁[j + 1]

A31: j + 1 < i

proof

assume i <= j + 1 ; :: thesis: contradiction
then i < j + 1 by A30, XXREAL_0:1;
hence contradiction by A27, NAT_1:13; :: thesis: verum

end;

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 S₁[j + 1] by A31; :: thesis: verum

end;

end;

end;

suppose A35: i <= j ; :: thesis: S₁[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 S₁[j + 1] by A35, NAT_1:13; :: thesis: verum

end;

end;

end;

A40: 1 in dom q by A10, A22, A20, FINSEQ_1:1;

now :: thesis: ( ( 1 < i & fp . 1 = fq . 1 ) or ( i <= 1 & fq . 1 = a * (fp . 1) ) )

per cases ( 1 < i or i <= 1 ) ;

case A41: 1 < i ; :: thesis: fp . 1 = fq . 1

thus fp . 1 = p /. 1 by A11, A21, PARTFUN1:def 6
.= q /. 1 by A5, A21, A41
.= fq . 1 by A14, A40, PARTFUN1:def 6 ; :: thesis: verum

end;

case i <= 1 ; :: thesis: fq . 1 = a * (fp . 1)

then i = 1 by A18, XXREAL_0:1;
hence fq . 1 = a * (p /. 1) by A3, A4, A14, A17, A10, A22, PARTFUN1:def 6
.= a * (fp . 1) by A11, A21, PARTFUN1:def 6 ;
:: thesis: verum

end;

end;

end;

then A42: S₁[1] ;
for j being Element of NAT st 1 <= j & j <= len p holds
S₁[j] from INT_1:sch 7(A42, A23);
hence Product q = a * (Product p) by A9, A13, A16, A18, A19; :: thesis: verum

end;

end;