let L be non empty right_complementable right-distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis:
let p, q be Polynomial of L; :: thesis:
let a be Element of L; :: thesis:
set f = p *' (a * q);
set g = a * (p *' q);
A1: dom (p *' (a * q)) = NAT by FUNCT_2:def 1
.= dom (a * (p *' q)) by FUNCT_2:def 1 ;

now :: thesis:

let i be object ; :: thesis:
assume i in dom (p *' (a * q)) ; :: thesis:
then reconsider n = i as Element of NAT ;
consider fr being FinSequence of the carrier of L such that
A2: ( len fr = n + 1 & (p *' (a * q)) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds
fr . k = (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) ) ) by POLYNOM3:def 9;
consider fa being FinSequence of the carrier of L such that
A3: ( len fa = n + 1 & (p *' q) . i = Sum fa & ( for k being Element of NAT st k in dom fa holds
fa . k = (p . (k -' 1)) * (q . ((n + 1) -' k)) ) ) by POLYNOM3:def 9;
Seg (len fa) = dom fr by A2, A3, FINSEQ_1:def 3;
then A4: dom fa = dom fr by FINSEQ_1:def 3;

A5: now :: thesis:

let k be Element of NAT ; :: thesis:
assume A6: k in dom fa ; :: thesis:
then fa . k = fa /. k by PARTFUN1:def 6;
then reconsider x = fa . k as Element of L ;
thus fr /. k = fr . k by A6, A4, PARTFUN1:def 6
.= (p . (k -' 1)) * ((a * q) . ((n + 1) -' k)) by A4, A6, A2
.= (p . (k -' 1)) * (a * (q . ((n + 1) -' k))) by POLYNOM5:def 4
.= a * ((p . (k -' 1)) * (q . ((n + 1) -' k))) by GROUP_1:def 3
.= a * x by A6, A3
.= a * (fa /. k) by A6, PARTFUN1:def 6 ; :: thesis:

end;

(a * (p *' q)) . n = a * (Sum fa) by A3, POLYNOM5:def 4
.= (p *' (a * q)) . n by A5, Th1, A3, A2 ;
hence (p *' (a * q)) . i = (a * (p *' q)) . i ; :: thesis:

end;

hence p *' (a * q) = a * (p *' q) by A1, FUNCT_1:2; :: thesis: