let L be non empty right_complementable distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L
for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
let p1, p2 be Polynomial of L; :: thesis: for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
let x be Element of L; :: thesis: p1 *' (x * p2) = x * (p1 *' p2)
set f = p1 *' (x * p2);
set g = x * (p1 *' p2);

A1: now :: thesis: for i9 being object st i9 in dom (p1 *' (x * p2)) holds
(p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9

let i9 be object ; :: thesis: ( i9 in dom (p1 *' (x * p2)) implies (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 )
assume i9 in dom (p1 *' (x * p2)) ; :: thesis: (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9
then reconsider i = i9 as Element of NAT ;
consider rf being FinSequence of L such that
A2: len rf = i + 1 and
A3: (p1 *' (x * p2)) . i = Sum rf and
A4: for k being Element of NAT st k in dom rf holds
rf . k = (p1 . (k -' 1)) * ((x * p2) . ((i + 1) -' k)) by POLYNOM3:def 9;
consider rp being FinSequence of L such that
A5: len rp = i + 1 and
A6: (p1 *' p2) . i = Sum rp and
A7: for k being Element of NAT st k in dom rp holds
rp . k = (p1 . (k -' 1)) * (p2 . ((i + 1) -' k)) by POLYNOM3:def 9;
A8: Seg (len (x * rp)) = dom (x * rp) by FINSEQ_1:def 3
.= dom rp by POLYNOM1:def 1
.= Seg (len rp) by FINSEQ_1:def 3 ;
then A9: dom (x * rp) = Seg (len rf) by A2, A5, FINSEQ_1:def 3
.= dom rf by FINSEQ_1:def 3 ;
A10: dom (x * rp) = dom rp by POLYNOM1:def 1;

A11: now :: thesis: for j being Nat st 1 <= j & j <= len rf holds
(x * rp) . j = rf . j

let j be Nat; :: thesis: ( 1 <= j & j <= len rf implies (x * rp) . j = rf . j )
assume that
A12: 1 <= j and
A13: j <= len rf ; :: thesis: (x * rp) . j = rf . j
A14: j in dom rf by A12, A13, FINSEQ_3:25;
then A15: rp /. j = rp . j by A9, A10, PARTFUN1:def 6;
thus (x * rp) . j = (x * rp) /. j by A9, A14, PARTFUN1:def 6
.= x * (rp /. j) by A9, A10, A14, POLYNOM1:def 1
.= x * ((p1 . (j -' 1)) * (p2 . ((i + 1) -' j))) by A7, A9, A10, A14, A15
.= (p1 . (j -' 1)) * (x * (p2 . ((i + 1) -' j))) by GROUP_1:def 3
.= (p1 . (j -' 1)) * ((x * p2) . ((i + 1) -' j)) by POLYNOM5:def 4
.= rf . j by A4, A14 ; :: thesis: verum

end;

(x * (p1 *' p2)) . i = x * (Sum rp) by A6, POLYNOM5:def 4
.= Sum (x * rp) by Th8
.= (p1 *' (x * p2)) . i by A2, A3, A5, A8, A11, FINSEQ_1:6, FINSEQ_1:14 ;
hence (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 ; :: thesis: verum

end;

dom (p1 *' (x * p2)) = NAT by FUNCT_2:def 1
.= dom (x * (p1 *' p2)) by FUNCT_2:def 1 ;
hence p1 *' (x * p2) = x * (p1 *' p2) by A1, FUNCT_1:2; :: thesis: verum