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

now :: thesis: for i being object st i in dom ((a * p) *' q) holds
((a * p) *' q) . i = (a * (p *' q)) . i

let i be object ; :: thesis: ( i in dom ((a * p) *' q) implies ((a * p) *' q) . i = (a * (p *' q)) . i )
assume i in dom ((a * p) *' q) ; :: thesis: ((a * p) *' q) . i = (a * (p *' q)) . i
then reconsider n = i as Element of NAT ;
consider fr being FinSequence of the carrier of L such that
A2: ( len fr = n + 1 & ((a * p) *' q) . i = Sum fr & ( for k being Element of NAT st k in dom fr holds
fr . k = ((a * p) . (k -' 1)) * (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: for k being Element of NAT st k in dom fa holds
fr /. k = a * (fa /. k)

let k be Element of NAT ; :: thesis: ( k in dom fa implies fr /. k = a * (fa /. k) )
assume A6: k in dom fa ; :: thesis: fr /. k = a * (fa /. k)
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
.= ((a * p) . (k -' 1)) * (q . ((n + 1) -' k)) by A4, A6, A2
.= (a * (p . (k -' 1))) * (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: verum

end;

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

end;

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