let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L
for p29 being Element of (Polynom-Ring L) st p29 = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
let p1, p2 be Polynomial of L; :: thesis: for p29 being Element of (Polynom-Ring L) st p29 = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
let p29 be Element of (Polynom-Ring L); :: thesis: ( p29 = p2 implies for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F) )
assume A1: p29 = p2 ; :: thesis: for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p29 * F)
reconsider p19 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
let F be FinSequence of (Polynom-Ring L); :: thesis: ( p1 = Sum F implies p2 *' p1 = Sum (p29 * F) )
assume p1 = Sum F ; :: thesis: p2 *' p1 = Sum (p29 * F)
then p29 * p19 = Sum (p29 * F) by Th8;
hence p2 *' p1 = Sum (p29 * F) by A1, POLYNOM3:def 10; :: thesis: verum