let R be non empty right_complementable add-associative right_zeroed right_unital distributive associative commutative doubleLoopStr ; :: thesis: for p, q being sequence of R
for a being Element of R holds a * (p *' q) = p *' (a * q)
let p, q be sequence of R; :: thesis: for a being Element of R holds a * (p *' q) = p *' (a * q)
let a be Element of R; :: thesis: a * (p *' q) = p *' (a * q)
set t = a * (p *' q);

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

let x be object ; :: thesis: ( x in NAT implies (a * (p *' q)) . x = (p *' (a * q)) . x )
assume x in NAT ; :: thesis: (a * (p *' q)) . x = (p *' (a * q)) . x
then reconsider i = x as Element of NAT ;
consider F being FinSequence of the carrier of R such that
H1: ( len F = i + 1 & (p *' q) . i = Sum F & ( for k being Element of NAT st k in dom F holds
F . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
consider G being FinSequence of the carrier of R such that
H2: ( len G = i + 1 & (p *' (a * q)) . i = Sum G & ( for k being Element of NAT st k in dom G holds
G . k = (p . (k -' 1)) * ((a * q) . ((i + 1) -' k)) ) ) by POLYNOM3:def 9;
H3: dom F = Seg (i + 1) by H1, FINSEQ_1:def 3
.= dom G by H2, FINSEQ_1:def 3 ;

now :: thesis: for x being object st x in dom F holds
G /. x = a * (F /. x)

let x be object ; :: thesis: ( x in dom F implies G /. x = a * (F /. x) )
assume H4: x in dom F ; :: thesis: G /. x = a * (F /. x)
then reconsider j = x as Element of NAT ;
H5: F . j = (p . (j -' 1)) * (q . ((i + 1) -' j)) by H4, H1;
G /. j = G . j by H3, H4, PARTFUN1:def 6
.= (p . (j -' 1)) * ((a * q) . ((i + 1) -' j)) by H2, H4, H3
.= (p . (j -' 1)) * (a * (q . ((i + 1) -' j))) by POLYNOM5:def 4
.= ((p . (j -' 1)) * (q . ((i + 1) -' j))) * a by GROUP_1:def 3
.= a * (F /. j) by PARTFUN1:def 6, H5, H4 ;
hence G /. x = a * (F /. x) ; :: thesis: verum

end;

then G = a * F by H3, POLYNOM1:def 1;
then Sum G = a * (Sum F) by POLYNOM1:12;
hence (a * (p *' q)) . x = (p *' (a * q)) . x by H1, POLYNOM5:def 4, H2; :: thesis: verum

end;

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