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 ;
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 ;
then A11: (p . (k -' 1)) * (q . ((i + 1) -' k)) = f1 . k by A3
.= f1 /. k by ;
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
.= (a * f1) /. k by
.= (a * f1) . k by ; :: thesis: verum
end;
thus (a * (p *' q)) . i = a * (Sum f1) by
.= Sum (a * f1) by BINOM:4
.= ((a * p) *' q) . i by ; :: thesis: verum
end;
hence a * (p *' q) = (a * p) *' q by FUNCT_2:63; :: thesis: verum