let L be non empty right_complementable left_zeroed distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for a being Element of L
for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
let a be Element of L; :: thesis: for p, q being sequence of L holds a * (p *' q) = (a * p) *' q
let p, q be sequence of L; :: thesis: a * (p *' q) = (a * p) *' q
for x being Element of NAT holds (a * (p *' q)) . x = ((a * p) *' q) . x

proof

let i be Element of NAT ; :: thesis: (a * (p *' q)) . i = ((a * p) *' q) . i
consider f1 being FinSequence of the carrier of L such that
A1: len f1 = i + 1 and
A2: (p *' q) . i = Sum f1 and
A3: for k being Element of NAT st k in dom f1 holds
f1 . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;
consider f2 being FinSequence of the carrier of L such that
A4: len f2 = i + 1 and
A5: ((a * p) *' q) . i = Sum f2 and
A6: for k being Element of NAT st k in dom f2 holds
f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;
A7: dom (a * f1) = dom f1 by POLYNOM1:def 1
.= dom f2 by A1, A4, FINSEQ_3:29 ;
A8: for k being Nat st k in dom f2 holds
f2 . k = (a * f1) . k

proof

let k be Nat; :: thesis: ( k in dom f2 implies f2 . k = (a * f1) . k )
assume A9: k in dom f2 ; :: thesis: f2 . k = (a * f1) . k
A10: k in dom f1 by A1, A4, A9, FINSEQ_3:29;
then A11: (p . (k -' 1)) * (q . ((i + 1) -' k)) = f1 . k by A3
.= f1 /. k by A10, PARTFUN1:def 6 ;
thus f2 . k = ((a * p) . (k -' 1)) * (q . ((i + 1) -' k)) by A6, A9
.= (a * (p . (k -' 1))) * (q . ((i + 1) -' k)) by POLYNOM5:def 4
.= a * (f1 /. k) by A11, GROUP_1:def 3
.= (a * f1) /. k by A10, POLYNOM1:def 1
.= (a * f1) . k by A7, A9, PARTFUN1:def 6 ; :: thesis: verum

end;

thus (a * (p *' q)) . i = a * (Sum f1) by A2, POLYNOM5:def 4
.= Sum (a * f1) by BINOM:4
.= ((a * p) *' q) . i by A5, A7, A8, FINSEQ_1:13 ; :: thesis: verum

end;

hence a * (p *' q) = (a * p) *' q by FUNCT_2:63; :: thesis: verum