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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) 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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) 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 i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) implies Product q = a * (Product p) )
assume A1: ( len p = len q & ex i being Element of NAT st
( i in dom p & q /. i = a * (p /. i) & ( for i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) ) ; :: thesis: Product q = a * (Product p)
then consider i being Element of NAT such that
A2: ( i in dom p & q /. i = a * (p /. i) & ( for i' being Element of NAT st i' in dom p & i' <> i holds
q /. i' = p /. i' ) ) ;
A3: ( Product p = the multF of L "**" p & Product q = the multF of L "**" q ) by GROUP_4:def 3;

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 A2, RELAT_1:60; :: thesis: verum

end;

suppose len p <> 0 ; :: thesis: Product q = a * (Product p)

then A4: len p >= 1 by NAT_1:14;
then consider fp being Function of NAT ,the carrier of L such that
A5: ( fp . 1 = p . 1 & ( for i being Element of NAT st 0 <> i & i < len p holds
fp . (i + 1) = the multF of L . (fp . i),(p . (i + 1)) ) & Product p = fp . (len p) ) by A3, FINSOP_1:2;
consider fq being Function of NAT ,the carrier of L such that
A6: ( fq . 1 = q . 1 & ( for i being Element of NAT st 0 <> i & i < len q holds
fq . (i + 1) = the multF of L . (fq . i),(q . (i + 1)) ) & Product q = fq . (len p) ) by A1, A3, A4, FINSOP_1:2;
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
A7: dom p = Seg l by FINSEQ_1:def 2;
i in { z where z is Element of NAT : ( 1 <= z & z <= l ) } by A2, A7, FINSEQ_1:def 1;
then consider i' being Element of NAT such that
A8: ( i' = i & 1 <= i' & i' <= l ) ;
consider l' being Nat such that
A9: dom q = Seg l' by FINSEQ_1:def 2;
reconsider l = l, l' = l' as Element of NAT by ORDINAL1:def 13;
A10: l = len p by A7, FINSEQ_1:def 3
.= l' by A1, A9, FINSEQ_1:def 3 ;
1 <= l by A8, XXREAL_0:2;
then A11: ( 1 in dom p & 1 in dom q ) by A7, A9, A10, FINSEQ_1:3;

now

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

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

thus fp . 1 = p /. 1 by A5, A11, PARTFUN1:def 8
.= q /. 1 by A2, A11, A12
.= fq . 1 by A6, A11, PARTFUN1:def 8 ; :: thesis: verum

end;

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

then i = 1 by A8, XXREAL_0:1;
hence fq . 1 = a * (p /. 1) by A2, A6, A7, A9, A10, PARTFUN1:def 8
.= a * (fp . 1) by A5, A11, PARTFUN1:def 8 ;
:: thesis: verum

end;

end;

end;

then A13: S₁[1] ;
A14: 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 A15: ( 1 <= j & j < len p ) ; :: thesis: ( not S₁[j] or S₁[j + 1] )
assume A16: S₁[j] ; :: thesis: S₁[j + 1]

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

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

now

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

case A18: j + 1 = i ; :: thesis: S₁[j + 1]

then A19: p . (j + 1) = p /. (j + 1) by A2, PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A2, A7, A9, A10, A18, PARTFUN1:def 8;
then fq . (j + 1) = (fp . j) * (a * (p /. (j + 1))) by A1, A2, A6, A15, A16, A17, A18
.= ((fp . j) * (p /. (j + 1))) * a by GROUP_1:def 4
.= (fp . (j + 1)) * a by A5, A15, A19 ;
hence S₁[j + 1] by A18; :: thesis: verum

end;

case A20: j + 1 <> i ; :: thesis: S₁[j + 1]

j + 1 <= i by A17, NAT_1:13;
then A21: j + 1 <= l by A8, XXREAL_0:2;
0 + 1 <= j + 1 by XREAL_1:8;
then A22: j + 1 in Seg l by A21, FINSEQ_1:3;
then A23: p . (j + 1) = p /. (j + 1) by A7, PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A9, A10, A22, PARTFUN1:def 8;
then A24: fq . (j + 1) = (fq . j) * (q /. (j + 1)) by A1, A6, A15
.= the multF of L . (fq . j),(p . (j + 1)) by A2, A7, A20, A22, A23
.= fp . (j + 1) by A5, A15, A16, A17 ;
j + 1 < i

proof

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

end;

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

end;

end;

end;

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

end;

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

then A26: i < j + 1 by NAT_1:13;
j < l by A7, A15, FINSEQ_1:def 3;
then A27: j + 1 <= l by NAT_1:13;
0 + 1 <= j + 1 by XREAL_1:8;
then A28: j + 1 in dom p by A7, A27, FINSEQ_1:3;
then A29: p . (j + 1) = p /. (j + 1) by PARTFUN1:def 8;
q . (j + 1) = q /. (j + 1) by A7, A9, A10, A28, PARTFUN1:def 8;
then fq . (j + 1) = (fq . j) * (q /. (j + 1)) by A1, A6, A15
.= (a * (fp . j)) * (p /. (j + 1)) by A2, A16, A25, A26, A28
.= a * ((fp . j) * (p /. (j + 1))) by GROUP_1:def 4
.= a * (fp . (j + 1)) by A5, A15, A29 ;
hence S₁[j + 1] by A25, NAT_1:13; :: thesis: verum

end;

end;

end;

A30: for j being Element of NAT st 1 <= j & j <= len p holds
S₁[j] from POLYNOM2:sch 4(A13, A14);
len p = l by A7, FINSEQ_1:def 3;
hence Product q = a * (Product p) by A4, A5, A6, A8, A30; :: thesis: verum

end;

end;